# Zulip Chat Archive

## Stream: lean4

### Topic: Implicit arguments and pattern matching

#### Ryan Scott (Mar 30 2021 at 14:23):

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 (Mar 30 2021 at 14:36):

This works out of the box on current master

#### Notification Bot (Mar 30 2021 at 14:36):

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

#### Ryan Scott (Mar 30 2021 at 14:45):

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 (Mar 30 2021 at 16:05):

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

Last updated: May 18 2021 at 23:14 UTC