Definining a function changes type behavior?

Stream: lean4

[Jeremy Salwen]

Consider the following MWE:

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Tactic.Find
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic
open Mathlib.Tactic

lemma List.toArray_data (a:Array α): (List.toArray a.data) = a := sorry

def lem :=  (fun {α} a =>
  id
    (Eq.mp (congrFun (congrArg Eq (List.toArray_data (Array.pop (α:=α) a))) (List.toArray (List.dropLast a.data)))
      (congrArg List.toArray (Array.data_pop a))))

def bar (β):= funext (α:= Array β) lem
def foo (β):= funext (α:= Array β) (fun {α} a =>
  id
    (Eq.mp (congrFun (congrArg Eq (List.toArray_data (Array.pop (α:=α) a))) (List.toArray (List.dropLast a.data)))
      (congrArg List.toArray (Array.data_pop a))))

bar type checks fine, but foo doesn't despite the fact that lem is just defined as the same expression used in foo.

The error I get is

application type mismatch
  @Array.pop α
argument
  α
has type
  Array β : Type ?u.178
but is expected to have type
  Type ?u.230 : Type (?u.230 + 1)

Which makes me think it is somehow universe related? Is there any way to make the raw fun work here the same as the defined lem?

[Sebastian Ullrich]

The error message should make you suspicious: α should probably not be an Array. When an identifier like lem is of implicit function type, it is eligible for implicit parameter insertion, i.e. the last lem is short for @lem (Array β). This is not the case when directly using a lambda.

[Jeremy Salwen]

Is there a way to fill implicit parameters of a lambda?

[Sebastian Ullrich]

This feels like #xy, but I suppose you can let-bind it

#check List.map (let f := fun {α} (a : α) => a; f)

[Jeremy Salwen]

Thanks Sebastian, I suppose it is a bit #xy, as I really want to do it to an Expr in the MetaM monad, but this gives me enough info to do that.