confusing error message trying to prove 2 fns equal

Stream: new members

[Alok Singh (S1'17)]

the code (from @David Thrane Christiansen 's book):

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  do return ((← lookup xs 0), (← lookup xs 2), (← lookup xs 4), (← lookup xs 6))

def firstThirdFifthSeventh' [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) := do
  let first ← lookup xs 0
  let third ← lookup xs 2
  let fifth ← lookup xs 4
  let seventh ← lookup xs 6
  pure (first, third, fifth, seventh)

theorem firstThirdFifthSeventhEq [Monad m] (lookup : List α → Nat → m α) (xs : List α) :
  firstThirdFifthSeventh lookup xs  = firstThirdFifthSeventh' lookup xs := by sorry

gives the error

stuck at solving universe constraint max (max (max (?u.10163+1) (?u.10164+1)) (?u.10165+1)) (?u.10166+1) =?= max (max (max (?u.10185+1) (?u.10186+1)) (?u.10187+1)) (?u.10188+1) while trying to unify Type (max (max (max ?u.10163 ?u.10164) ?u.10165) ?u.10166) : Type ((max (max (max ?u.10163 ?u.10164) ?u.10165) ?u.10166) + 1) with Type (max (max ?u.10188 (max ?u.10187 ?u.10188) (max (max ?u.10186 ?u.10188) ?u.10187) (max (max ?u.10185 ?u.10188) ?u.10187) ?u.10186) (max ?u.10187 ?u.10188) (max (max ?u.10186 ?u.10188) ?u.10187) (max (max ?u.10185 ?u.10188) ?u.10187) ?u.10186) : Type (max ((max ?u.10188 (max ?u.10187 ?u.10188) (max (max ?u.10186 ?u.10188) ?u.10187) (max (max ?u.10185 ?u.10188) ?u.10187) ?u.10186) + 1) ((max (max ?u.10187 ?u.10188) (max (max ?u.10186 ?u.10188) ?u.10187) (max (max ?u.10185 ?u.10188) ?u.10187) ?u.10186) + 1)), stuck at solving universe constraint max (max (max ?u.10185 ?u.10186) ?u.10187) ?u.10188 =?= max (max (max ?u.10163 ?u.10164) ?u.10165) ?u.10166 while trying to unify (List α → Nat → m α) α → Nat → m α with (List α → Nat → m α) α → Nat → m α

i don't get the failure to unify since these impls are basically the same

[Yongyi Chen]

One way to make the error go away is to make α a type parameter by putting {α : Type*} or something like that in the declaration of each function, instead of letting it be auto-implicit.

[Kevin Buzzard]

Oh yikes, autoImplicit uses Type _ not Type*?

[Ruben Van de Velde]

I'd guess so, since * is a mathlib thing as far as I understand

[David Thrane Christiansen]

@Alok Singh (S1'17) The issue here is that Lean infers a very general type for the two functions behind the scenes, and then when they're used together, they're too general for Lean to realize that they fit together.

The simplest thing that gets you unstuck without using lots of features beyond where you are in the book is to constrain the type of m:

theorem firstThirdFifthSeventhEq {m : Type → Type} [Monad m] (lookup : List α → Nat → m α) (xs : List α) :
  firstThirdFifthSeventh lookup xs  = firstThirdFifthSeventh' lookup xs := by rfl

[David Thrane Christiansen]

After you make it past section 6.5 on universes, then this next bit may make sense. If not, ask me and I'll do my best.

Lean's product type is polymorphic over universes, so it has the type:

Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

In each of those type signatures, it's nested three times, for a total of four universe parameters. The Monad class also has two parameters - one is fixed to be the output universe of the outermost Prod, but the other is left unconstrained. This means that the two function signatures have fully-explicit declarations like:

firstThirdFifthSeventh.{u_1, u_2, u_3, u_4, u_5}
  {m : Type (max u_1 (max u_2 u_1) (max (max u_3 u_1) u_2) (max (max u_4 u_1) u_2) u_3) → Type u_5}
  {α : Type (max u_1 (max u_2 u_1) (max (max u_3 u_1) u_2) (max (max u_4 u_1) u_2) u_3)} [inst : Monad m]
  (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α)

The equality type requires that both of its arguments be in the same universe:

Eq.{u_1} {α : Sort u_1} (a✝ a¹✝ : α) : Prop

Thus, Lean needs to find universe levels that make these two piles of max equal. I'm actually not sure why it doesn't here - I'll go follow up and see what I can figure out.

[Mario Carneiro]

it's because max is not injective and lean is conservative about unifying those expressions

[David Thrane Christiansen]

Right :-)

[David Thrane Christiansen]

So @Alok Singh (S1'17) - to unpack what's going on is that we can't conclude that max a b = max c d implies a = c or b = d. This means that the system needs help.

The error message could certainly do with some work.

[Alok Singh (S1'17)]

Thanks all