Implicit variables from context

Stream: lean4

[Zygimantas Straznickas]

Is it possible to get Lean to fill in implicit arguments using matching-type terms in the current context? In Coq I would often do this:

Record PointedType := mkPointedType {
  T : Type ;
  mkT : T
}.

Inductive PointedTypeVal {P : PointedType} :=
| mk : P.(T) -> PointedTypeVal.

Definition test {P : PointedType} : PointedTypeVal := mk P.(mkT).

(* or *)

Variable (P : PointedType).
Definition test2 : PointedTypeVal := mk P.(mkT).

In Lean it doesn't seem to work:

structure PointedType where
  T : Type
  mkT : T

inductive PointedTypeVal {P : PointedType} where
  | mk : P.T -> PointedTypeVal

set_option pp.all true

def test {A : PointedType} : PointedTypeVal :=  PointedTypeVal.mk A.mkT
-- error (in the return type specification):
-- @PointedTypeVal : {P : PointedType} → Type
-- don't know how to synthesize implicit argument
--  @PointedTypeVal (@?m.649 A)
-- context:
-- A : PointedType
-- ⊢ PointedType
-- when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

variable {A : PointedType}
def test2 : PointedTypeVal :=  PointedTypeVal.mk A.mkT
-- same error

[Mario Carneiro]

It looks like the behavior has changed from lean 3 here. In general, lean definitely will use unification to fill implicit arguments, and in lean 3, it will do what you are hoping. In lean 4, the type of the declaration is elaborated separately from the body when it is provided, meaning that it will only infer the type if it could also infer the type when the body is sorry. However you can leave the type off completely, in which case it will use the body to infer the type, so you can write this instead:

-- this works
def test {A : PointedType} := PointedTypeVal.mk A.mkT

-- also this
def test2 {A : PointedType} := (PointedTypeVal.mk A.mkT : PointedTypeVal)
def test3 {A : PointedType} := show PointedTypeVal from PointedTypeVal.mk A.mkT

[Mario Carneiro]

@Zygimantas Straznickas

[Zygimantas Straznickas]

Thanks, that works!

[Zygimantas Straznickas]

Actually, is there a similar workaround I can use when providing argument types? E.g. making def test (v : PointedTypeVal) := v work?

[Mario Carneiro]

def test := fun (v : PointedTypeVal) => v

[Mario Carneiro]

not that this will work, because that body won't help to infer the argument anyway