CoeFun and implicit arguments

[mniip]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Function applications going through CoeFun do not respect the implicitness of the parameters declared in the instance head, rather they take the implicitness information from the instance implementation.

Context

Steps to Reproduce

structure Foo where app : ∀α, (x : α) → α

def foo := Foo.mk fun _ => id

instance : CoeFun Foo fun _ => ∀{α}, α → α where
  coe := Foo.app

/-- info: CoeFun.coe foo Nat : Type -/
#guard_msgs in
#check CoeFun.coe foo Nat
/-- info: foo.app Nat : Nat → Nat -/
#guard_msgs in
#check foo Nat

Expected behavior:

• Both cases desugar as Foo.app foo (α:=Type) (x:=Nat), and infer the type Type

Actual behavior:

• The first one infers the correct type, but the second desugars as Foo.app foo (α:=Nat) and infers the type Nat → Nat.

Versions

4.13.0

Additional Information

The problem can be reversed by making the structure field have implicit ∀{α} and the instance head have the explicit ∀α.
#1891 seems relevant.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

CoeFun Foo fun _ => ∀{α}, α → α tells the elaborator to coerce the former type into the latter. I don't see why it should adjust the second type with any other information, at least without further motivation. Thus I'm closing this as by design.

[mniip]

@Kha I think there's a misunderstanding.

CoeFun Foo fun _ => ∀{α}, α → α tells the elaborator to coerce the former type into the latter.

That's exactly what it fails to do, hence this issue.

Instead of coercing to "the latter" -- whatever is written in the instance head, it coerces to what is actually the type of the instance body.

[Kha]

Oh! I will reopen then. It would still be good to know more about the practical relevance of this issue, is there a specific use case?

[mniip]

I bumped into this by accident more than anything. I had

structure NatTrans (f g : Type u → Type u) [Functor f] [Functor g] where
  app : ∀α, f α → g α
  preserves_map : ∀α β h xs, app β (h <$> xs) = h <$> app α xs

and I decided to define a CoeFun instance like so:

instance [Functor f] [Functor g]
  : CoeFun (NatTrans f g) fun _ => ∀{α}, f α → g α where
    coe := NatTrans.app

which reproduces this bug. The easy work-around of course is to instead define it as

instance [Functor f] [Functor g]
  : CoeFun (NatTrans f g) fun _ => ∀{α}, f α → g α where
    coe η := NatTrans.app η _

but I was nevertheless surprised that the implementation of an instance can affect how its use-sites are typechecked.

[kmill]

I don't see any good way to have it use the type in the CoeFun type, since the way coercions work is that the body of a coercion instance is substituted in for the coe function. There's no place where we can insert the type that appears in CoeFun itself. If we didn't do the substitution, then the type would appear in the coe application itself, but I don't believe substitution is a design that we will backtrack on.

Maybe a solution here is a linter that warns if the types don't have the same implicitness and optParam/autoParam annotations?

(Another practical consequence is when we have a dotParam annotation, people might try inserting it into the CoeFun type rather than the implementation's type, which will have no effect.)