## Stream: new members

### Topic: confusing error message trying to prove 2 fns equal

#### Alok Singh (S1'17) (Nov 26 2023 at 04:18):

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 (Nov 26 2023 at 04:59):

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 (Nov 26 2023 at 09:36):

Oh yikes, autoImplicit uses Type _ not Type*?

#### Ruben Van de Velde (Nov 26 2023 at 10:18):

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

#### David Thrane Christiansen (Nov 27 2023 at 06:06):

@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 (Nov 27 2023 at 06:44):

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 (Nov 27 2023 at 07:14):

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

Right :-)

#### David Thrane Christiansen (Nov 27 2023 at 08:56):

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) (Nov 27 2023 at 16:49):

Thanks all

Last updated: Dec 20 2023 at 11:08 UTC