Implicit function argument changes type parsing behaviour

Stream: lean4

[Leni Aniva]

Consider this example: (I could not find a smaller example since when I try to shrink the example it somehow does not give the error:

def f { α } (as t bs: List α) (a b: α) (h: (List.concat t a) = (List.concat bs b)) (var: α) (var1: List α) (var2: α) (var3: List α)
  (h1: (List.concat (var :: var1) a) = (List.concat (var2 :: var3) b))
  (_auto0: List.below (motive := (λ _auto0: List α => ∀ (_auto1: List α) (_auto2: α) (_auto3: α) (_auto4: ((List.concat _auto0 _auto2) = (List.concat _auto1 _auto3))),
           And (_auto0 = _auto1) (_auto2 = _auto3)))
    (var :: var1))
  :=
    @PProd.fst
      (@PProd
        ((fun _auto1 : (@List α) =>
            (forall {_auto2 : (@List α)}, (forall {_auto3 : α}, (forall {_auto4 : α},
              (forall (_auto5 : (@Eq (@List α) (@List.concat α _auto1 _auto3) (@List.concat α _auto2 _auto4))),
                (@And (@Eq (@List α) _auto1 _auto2) (@Eq α _auto3 _auto4))))))) var1)
        (@List.rec α (fun (_auto1 : (@List α)) => Type) PUnit (fun (head : α) => (fun (tail : (@List α)) => (fun (tail_ih : Type) => (@PProd (@PProd ((fun _auto3 : (@List α) => (forall {_auto4 : (@List α)}, (forall {_auto5 : α}, (forall {_auto6 : α}, (forall (_auto7 : (@Eq (@List α) (@List.concat α _auto3 _auto5) (@List.concat α _auto4 _auto6))), (@And (@Eq (@List α) _auto3 _auto4) (@Eq α _auto5 _auto6))))))) tail) tail_ih) PUnit)))) var1))
      PUnit
      _auto0

If I put { ... } brackets around _auto1 : (@List α), it somehow doesn't typecheck anymore:

def f { α } (as t bs: List α) (a b: α) (h: (List.concat t a) = (List.concat bs b)) (var: α) (var1: List α) (var2: α) (var3: List α)
  (h1: (List.concat (var :: var1) a) = (List.concat (var2 :: var3) b))
  (_auto0: List.below (motive := (λ _auto0: List α => ∀ (_auto1: List α) (_auto2: α) (_auto3: α) (_auto4: ((List.concat _auto0 _auto2) = (List.concat _auto1 _auto3))),
           And (_auto0 = _auto1) (_auto2 = _auto3)))
    (var :: var1))
  :=
    @PProd.fst
      (@PProd
        ((fun {_auto1 : (@List α)} =>
            (forall {_auto2 : (@List α)}, (forall {_auto3 : α}, (forall {_auto4 : α},
              (forall (_auto5 : (@Eq (@List α) (@List.concat α _auto1 _auto3) (@List.concat α _auto2 _auto4))),
                (@And (@Eq (@List α) _auto1 _auto2) (@Eq α _auto3 _auto4))))))) var1)
        (@List.rec α (fun (_auto1 : (@List α)) => Type) PUnit (fun (head : α) => (fun (tail : (@List α)) => (fun (tail_ih : Type) => (@PProd (@PProd ((fun _auto3 : (@List α) => (forall {_auto4 : (@List α)}, (forall {_auto5 : α}, (forall {_auto6 : α}, (forall (_auto7 : (@Eq (@List α) (@List.concat α _auto3 _auto5) (@List.concat α _auto4 _auto6))), (@And (@Eq (@List α) _auto3 _auto4) (@Eq α _auto5 _auto6))))))) tail) tail_ih) PUnit)))) var1))
      PUnit
      _auto0

gives

function expected at
  (@fun {_auto1 : List.{?u.31} α} =>
      ∀ {_auto2 : List.{?u.31} α} {_auto3 _auto4 : α},
        @Eq.{?u.31 + 1} (List.{?u.31} α) (@List.concat.{?u.31} α _auto1 _auto3) (@List.concat.{?u.31} α _auto2 _auto4) →
          And (@Eq.{?u.31 + 1} (List.{?u.31} α) _auto1 _auto2) (@Eq.{?u.31 + 1} α _auto3 _auto4))
    ?m.169
term has type
  Prop

However, this typechecks with no issue:

def g1 { α } := fun { _auto1 : (List α) } => ∀ (_auto2: (List α)), _auto1 = _auto2
def g2 { α } := fun _auto1 : (List α) => ∀ (_auto2: (List α)), _auto1 = _auto2

why does { ... } change the typecheck behaviour?

[Robert Maxton]

Arguably, that's the whole point of implicit arguments! Implicit arguments are supposed to be uniquely defined by (and therefore redundant with) later arguments; if you have no later arguments then they're supposed to be uniquely defined by the expected type. Thus, a lambda that ends with an implicit binder will participate in typechecking as if it had no last argument, and a lambda that has only implicit binders will typecheck as its output type, in this case Prop.

[Robert Maxton]

If you don't like this behavior, you can use strict implicit binders ⦃...⦄ instead, which will not be filled in unless there actually is a later argument to infer from, so functions will stay functions