Zulip Chat Archive

Stream: lean4

Topic: Implicit arguments and pattern matching


view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Mar 30 2021 at 14:36):

This works out of the box on current master

view this post on Zulip Notification Bot (Mar 30 2021 at 14:36):

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

view this post on Zulip 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).

view this post on Zulip 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