Implicit arguments and pattern matching

Stream: lean4

[Ryan Scott]

While translating some Coq code over to Lean4, I was surprised to discover that this doesn't typecheck:

inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T

open T

def runT (t : T) {a : Type} (x : a) : a :=
  match t with
  /- Doesn't work -/
  | mkT f => f x
  /-
  Also doesn't work

  | mkT f => @f a x
  | mkT f => f (a := a) x
  -/

T.lean:9:8
type mismatch
  f
has type
  ?m.56
but is expected to have type
  a✝ → a✝

On the other hand, this does typecheck:

inductive T2 : Type 1 :=
| mkT2 : (forall (a : Type), a -> a) -> T2

open T2

def runT2 (t2 : T2) {a : Type} (x : a) : a :=
  match t2 with
  /- Works -/
  | mkT2 f => f a x

The only difference between the two programs is whether the a in the type of mkT is made implicit or not. Is this expected behavior? If so, how can I make the first version of mkT typecheck?

I'm using Lean (version 4.0.0-m2, commit 26dda3f63d88, Release), in case that's important.

[Sebastian Ullrich]

This works out of the box on current master

[Notification Bot]

This topic was moved here from #general > Implicit arguments and pattern matching by Sebastian Ullrich

[Ryan Scott]

Ah, good to know! I suppose I should be using nightly instead of stable, then.

A related question: I'm having trouble figuring out why this discrepancy exists:

inductive T : Type 1 :=
| mkT : (forall {a : Type}, a -> a) -> T

open T

-- Works
def makeT (f : forall {a : Type}, a -> a) : T :=
  mkT f

-- Doesn't work
def makeT' : (forall {a : Type}, a -> a) -> T
| f => mkT f

T.lean:12:11
type mismatch
  f
has type
  ?m.118 x✝ → ?m.118 x✝ : Type
but is expected to have type
  a✝ → a✝ : Type

This is with Lean (version 4.0.0-nightly-2021-03-29, commit 0dfefb7b7845, Release).

[Leonardo de Moura]

@Ryan Scott This is probably an issue with the new implicit lambda feature in Lean4. I will investigate it today.