Infer the most general type

Stream: new members

[Patrick Johnson]

Is there a way to tell Lean to infer the most general type for a definition?

universes u v w
variable {α : Sort u}
variable {β : Sort v}
variable {γ : Sort w}
def K (a : α) (b : β) := a
def S (a : α → β → γ) (b : α → β) (c : α) := a c (b c)
def I := S K K -- error

It works if I write types explicitly: def I : α → α := S K (@K _ Type), but how can I make it implicit?

[Eric Wieser]

Are you sure you want Type and not (Type u) or (Type v) or ...

[Patrick Johnson]

It doesn't affect the final type of I. The second argument of the last K is ignored.

def I : α → α := S K (@K _ Type)
#check @I -- I : Π {α : Sort u_1}, α → α

[Reid Barton]

You can also put any random type like int there, yeah.

[Reid Barton]

A priori they could all define different functions I, so you should say which one you mean

[Reid Barton]

Haskell has some defaulting rule for situations like this because it can assume that all your definitions are parametric

[Reid Barton]

here is maybe a more familiar example:

def z : ℕ := list.length []  -- error: don't know how to synthesize placeholder

[Kyle Miller]

For

def I := S (@K α _) (@K _ ℕ) -- works
def I := S K (@K _ ℕ) -- doesn't work

a reason it doesn't work is that Lean doesn't do Hindley-Milner type inference. A key step of the algorithm is abstraction of metavariables at binding sites, but Lean instead says "don't know how to synthesize placeholder" in this situation.

[Kyle Miller]

Elaborating on what Reid said about how they could all define different functions I: the types might be the same for the various choices, but the definitions potentially might not be equal. (They are in this case, though.)

[Kyle Miller]

I don't use let expressions enough to have noticed that it checks for metavariables:

example : list ℕ :=
let x := []  -- don't know how to synthesize placeholder
in x

This is a place where Hindley-Milner would abstract the metavariable and make x be polymorphic.

The let tactic allows metavariables, though:

example : list ℕ :=
begin
  let x := [],
  exact x
end