make binder implicit in CoeFun

Stream: lean4

[Kevin Buzzard]

Is this possible in Lean 4? It worked in Lean 3:

-- lean 4
structure Foo (F G : Type → Type) where
  app : ∀ α : Type, F α → G α -- explicit

variable (F : Type → Type)
variable (G : Type → Type)

-- make α implicit in coercion to fun
instance : CoeFun (Foo F G) fun _ => ∀ {α : Type}, F α → G α := ⟨Foo.app⟩

variable (f : Foo F G) (x : F Nat)

#check f x -- fails
/-
application type mismatch
  Foo.app f x
argument
  x
has type
  F Nat : Type
but is expected to have type
  Type : Type 1
-/

#check f Nat x -- G Nat

[Kevin Buzzard]

-- lean 3
structure foo (F G : Type → Type) :=
(app : ∀ α : Type, F α → G α) -- explicit

variable (F : Type → Type)
variable (G : Type → Type)

-- make α implicit in coercion to fun
instance : has_coe_to_fun (foo F G) (λ _, Π {α}, F α → G α) :=
⟨foo.app⟩

variables (f : foo F G) (x : F ℕ)

#check f x -- works

[Gabriel Ebner]

No this doesn't work, you can't change the type with coercions.

[Gabriel Ebner]

You'd need to an auxiliary definition for that.

[Kevin Buzzard]

When things like this happen during porting (stuff which would work in lean 3 but not in lean 4) I never know whether to ask about them or just work around them.. I'll work around this one!

[Leonardo de Moura]

Recall that coercions are eagerly expanded by Lean 4.

[Kevin Buzzard]

Yeah but in my mental model of elaboration (which is poor) Foo.app is being unified to have type ∀ {α : Type}, F α → G α...I guess what I'm actually saying is that I don't really even understand how binders interact with type theory. My understanding is that ∀ {α : Type}, F α → G α and ∀ (α : Type), F α → G α are syntactically equal as far as type theory goes, and Foo.app is being coerced into having type ∀ {α : Type}, F α → G α but I have no clue about whether that coercion "sticks" when the coercion to function is instantiated; it seemed to stick in Lean 3 but not in Lean 4, is my mental model.

[Adam Topaz]

Is there any issue with making the following modification?

-- lean 4
structure Foo (F G : Type → Type) where
  app : ∀ {α : Type}, F α → G α -- implicit

variable (F : Type → Type)
variable (G : Type → Type)

-- make α implicit in coercion to fun
instance : CoeFun (Foo F G) fun _ => ∀ {α : Type}, F α → G α := ⟨Foo.app⟩

variable (f : Foo F G) (x : F Nat)

#check f x -- works

[Adam Topaz]

Or this

-- lean 4
structure Foo (F G : Type → Type) where
  app : ∀ α : Type, F α → G α -- explicit

variable (F : Type → Type)
variable (G : Type → Type)

-- make α implicit in coercion to fun
instance : CoeFun (Foo F G) fun _ => ∀ {α : Type}, F α → G α := ⟨fun η => η.app _⟩

variable (f : Foo F G) (x : F Nat)

#check f x -- works

[Eric Wieser]

@Adam Topaz , your --explicit comment is now wrong, right?

[Adam Topaz]

yeah ;)

[Adam Topaz]

(fixed)

[Leonardo de Moura]

@Kevin Buzzard If you add a set_option pp.all true in the Lean 4 and Lean 3 files, you will see the difference
Lean 3

set_option pp.all true
#check f x -- works
-- @coe_fn.{2 2} (foo F G) (λ (_x : foo F G), Π {α : Type}, F α → G α) (foo.has_coe_to_fun F G) f nat x : G nat

Lean 4

set_option pp.all true
#check f Nat x -- G Nat
-- @Foo.app F G f Nat x : G Nat

Note that the Lean 3 version contains the coe_fn auxiliary function.

[Kevin Buzzard]

@Adam Topaz the issue with changing the binders is that I think the agreement is that we try to make the port as faithful as possible right now, or else this will just lead to confusion down the line. In Lean 3 the app has an explicit alpha and the coercion has an implicit one, so your second suggestion is what I've gone with.