why doesn't this unify?

Stream: lean4

[Kevin Buzzard]

universe u v w

structure ApplicativeTransformation (F : Type u → Type v) [Applicative F] [LawfulApplicative F]
  (G : Type u → Type w) [Applicative G] [LawfulApplicative G] : Type max (u + 1) v w where
  app : ∀ α : Type u, F α → G α
  preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x
  preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y

variable (F : Type u → Type v) [Applicative F] [LawfulApplicative F]

variable (G : Type u → Type w) [Applicative G] [LawfulApplicative G]

instance : CoeFun (ApplicativeTransformation F G) fun _ => ∀ {α}, F α → G α :=
  ⟨ApplicativeTransformation.app⟩

variable {F G}

@[simp]
theorem coe_mk (f : ∀ α : Type u, F α → G α) (pp ps) :
  (ApplicativeTransformation.mk f pp ps) = f :=
  rfl
/-
type mismatch
  ps
has type
  ?m.1275 : Sort ?u.1274
but is expected to have type
  ∀ (x : F (α✝ → β✝)) (y : F α✝), f β✝ (Seq.seq x fun x => y) = Seq.seq (f (α✝ → β✝) x) fun x => f α✝ y : Prop
-/

In Lean 3 this worked (this is from control.traversable.basic in mathlib). I find these error messages confusing. There is an obvious solution to ?m.1275 : Sort ?u.1274 = <some proposition> : Prop. Changing to (ps : _) and variants didn't seem to fix the problem. What am I missing?

[Kyle Miller]

I think it's because Lean 4 unfolds coercions, so all that's left on the LHS of the = is f. Edit: with the version below, it's (ApplicativeTransformation.mk f pp ps).app on the LHS, so this theory isn't right.

[Kyle Miller]

I'm still a bit confused by what's going on, but giving the full types works:

theorem coe_mk (f : ∀ α : Type u, F α → G α)
  (pp : ∀ {α : Type u} (x : α), f _ (pure x) = pure x)
  (ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f _ (x <*> y) = f _ x <*> f _ y) :
  (ApplicativeTransformation.mk f pp ps) = f :=
  rfl

but there's no point for it being a @[simp] lemma since it's just f = f in the end (at least that's the error the attribute reports. When I #print the lemma I see a more complicated type... Ah, the LHS is (ApplicativeTransformation.mk f pp ps).app, which is something simp will already simplify?)

[Adam Topaz]

It has to do with the implicit variables in preserves_pure' and preservsed_seq' (but I can't say I understand why!)

universe u v w

structure ApplicativeTransformation (F : Type u → Type v) [Applicative F] [LawfulApplicative F]
  (G : Type u → Type w) [Applicative G] [LawfulApplicative G] : Type max (u + 1) v w where
  app : ∀ α : Type u, F α → G α
  preserves_pure' : ∀ (α : Type u) (x : α), app _ (pure x) = pure x
  preserves_seq' : ∀ (α β : Type u) (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y

variable (F : Type u → Type v) [Applicative F] [LawfulApplicative F]

variable (G : Type u → Type w) [Applicative G] [LawfulApplicative G]

instance : CoeFun (ApplicativeTransformation F G) fun _ => ∀ {α}, F α → G α :=
  ⟨ApplicativeTransformation.app⟩

variable {F G}

@[simp]
theorem coe_mk (f : ∀ (α : Type u), F α → G α) (pp ps) :
  (ApplicativeTransformation.mk f pp ps) = f :=
  rfl

^--- that works

[Adam Topaz]

Maybe hygiene has something to do with it?

[Kevin Buzzard]

Oh nice! So this looks like a bug?

[Kevin Buzzard]

def foo1mk (_ : ∀ (α : Type) (a : α), a = a) : Nat := 37
def foo2mk (_ : ∀ {α : Type} (a : α), a = a) : Nat := 37 -- implicit binder

example (x) : foo1mk x = foo1mk x := rfl -- works
example (x : ∀ {α : Type} (a : α), a = a) : foo2mk x = foo2mk x := rfl -- works
example (x) : foo2mk x = foo2mk x := rfl -- fails
/-
type mismatch
  x
has type
  ?m.114 : Sort ?u.113
but is expected to have type
  ∀ (a : α✝), a = a : Prop
-/

Should I open an issue or is this expected behaviour?

[Scott Morrison]

I'm not sure. In lean3 we have:

def foo1mk (_ : ∀ (α : Type) (a : α), a = a) : nat := 37
def foo2mk (_ : ∀ {α : Type} (a : α), a = a) : nat := 37 -- implicit binder

example (x) : foo1mk x = foo1mk x := rfl -- works
example (x : ∀ {α : Type} (a : α), a = a) : foo2mk x = foo2mk x := rfl -- fails
example (x) : foo2mk x = foo2mk x := rfl -- fails

[Kevin Buzzard]

But this works in Lean 3: https://github.com/leanprover-community/mathlib/blob/cb48031ce12812ece794b782299def24bd8daba0/src/control/traversable/basic.lean#L90

[Kevin Buzzard]

-- Lean 3
def foo2mk (_ : ∀ {α : Type} (a : α), a = a) : nat := 37
example (x) : foo2mk x = 37 := rfl -- works
example (x) : foo2mk x = foo2mk x := rfl -- fails on second foo2mk

I am now completely bewildered.

[Gabriel Ebner]

I think this is the implicit lambdas feature in action (lean inserts fun {alpha} => automatically).

[Gabriel Ebner]

It might work if you write foo2mk @x

[Kevin Buzzard]

Thanks! Yes this @ trick fixes it (in both Lean 3 and Lean 4), although I don't really understand why; my mental model of what's going on must be wrong.

[Mario Carneiro]

The @ operator does two things:

1. When applied to an application like @foo x y z (or @(f a) x y z for that matter), it will elaborate the application part foo x y z with all implicit arguments as explicit. So for example if foo or f a here had the type ∀ {x y z : ℕ}, ℕ then x y z would be passed in instead of using _ _ _ for those arguments and giving a type error. This is the normal use of @ from lean 3.
2. When used in a context where the expected type is an implicit lambda like foo @_ where foo : (∀ {x : ℕ}, ℕ) → ℕ, it prevents automatic insertion of fun x =>. That is, foo 0 is interpreted the same as foo @(fun _ => 0). This is a lean 4 original.

Notice that the behavior (1) affects the elaboration of the thing inside the expression, while (2) affects the context around the expression (the expected type). The @ simultaneously affects both but you can get just one or the other behavior by using (@e) or @(e) as appropriate.

[Mario Carneiro]

The present issue has to do with behavior (2). When you use foo2mk @x it will pass x directly to foo2mk rather than doing foo2mk @(fun _ => x) like it normally would. Because the type of x is unknown, this would cause it to get the type x : ∀ (a : ?α), a = a and then the second application will fail.

[Leonardo de Moura]

Pushed a small improvement for the implicit lambda feature. All examples in this thread have been included in the test suite, and are working without the @ annotation.
https://github.com/leanprover/lean4/commit/3e45060dd52c13ee4904da1ccf6279df154f1a8a