Help with Universe Levels

Stream: mathlib4

[zbatt]

I'm working on porting Data.FinEnum and I'm having some issues with universes. In particular, at the bottom with regard to the Pi.*_enum instances. If I let Lean fill them in on its own, its able to do it with, for example max u u_1 but if I try to do what works in Lean3 i..e Type max u v (where u, v are universes declared at the top of the file) it doesn't accept it. Can someone help me understand why this is? Thanks so much!

[Mario Carneiro]

can you show a #mwe?

[Mario Carneiro]

it's a bit hard to tell from your description what exactly you did and what lean had to say about it

[zbatt]

The translation of Pi.enum into Lean4 currently looks like:

def Pi.enum (β : α → Type _) [FinEnum α] [∀ a, FinEnum (β a)] : List (∀ a, β a) :=
  (Pi (toList α) fun x => toList (β x)).map (fun f x => f x (mem_to_list _))

which is parameterized over universes u which is declared in the file and u_1 which is not. In mathlib3, it is given as :

def pi.enum (β : α → Type (max u v)) [fin_enum α] [∀a, fin_enum (β a)] : list (Π a, β a)

which is parameterized over both u, v which are declared in the file.

Lean4 is filling in the wild card with max u u_1, but if I try to "force" it to be polymorphic over v I get

stuck at solving universe constraint
  max u ?u.109735 =?= max u v
while trying to unify
  (List (β x)) (β x)
with
  List (β x)

I think the relevant declarations are

universe u v
α : Type u
β : α -> Type v

Edit: Let me cook up a better mwe

[zbatt]

import Mathlib.Control.Monad.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.List.ProdSigma

universe u v

open Finset

class FinEnum (α : Sort _) where
  card : ℕ
  Equiv : α ≃ Fin card
  [decEq : DecidableEq α]
#align fin_enum FinEnum

attribute [instance] FinEnum.decEq

namespace FinEnum

variable {α : Type u} {β : α → Type v}


/-- create a `FinEnum` instance from an exhaustive list without duplicates -/
def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' : List.Nodup xs) : FinEnum α
    where
  card := xs.length
  Equiv :=
    ⟨fun x => ⟨xs.indexOf x, by rw [List.indexOf_lt_length] ; apply h⟩, fun ⟨i, h⟩ =>
      xs.nthLe _ h, fun x => by simp [ofNodupList.match_1], fun ⟨i, h⟩ => by
      simp [ofNodupList.match_1, *]⟩
#align fin_enum.of_nodup_list FinEnum.ofNodupList

/-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/
def ofList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) : FinEnum α :=
  ofNodupList xs.dedup (by simp [*]) (List.nodup_dedup _)
#align fin_enum.of_list FinEnum.ofList

/-- create an exhaustive list of the values of a given type -/
def toList (α) [FinEnum α] : List α :=
  (List.finRange (card α)).map (Equiv).symm
#align fin_enum.to_list FinEnum.toList

open Function

@[simp]
theorem mem_to_list [FinEnum α] (x : α) : x ∈ toList α := by
  simp [toList] ; exists Equiv x ; simp
#align fin_enum.mem_to_list FinEnum.mem_to_list


instance (priority := 100) [FinEnum α] : Fintype α
    where
  elems := univ.map (Equiv).symm.toEmbedding
  complete := by intros ; simp

/-- For `Pi.cons x xs y f` create a function where every `i ∈ xs` is mapped to `f i` and
`x` is mapped to `y`  -/
def Pi.cons [DecidableEq α] (x : α) (xs : List α) (y : β x) (f : ∀ a, a ∈ xs → β a) :
    ∀ a, a ∈ (x :: xs : List α) → β a
  | b, h => if h' : b = x then cast (by rw [h']) y else f b (List.mem_of_ne_of_mem h' h)
#align fin_enum.pi.cons FinEnum.Pi.cons

/-- Given `f` a function whose domain is `x :: xs`, produce a function whose domain
is restricted to `xs`.  -/
def Pi.tail {x : α} {xs : List α} (f : ∀ a, a ∈ (x :: xs : List α) → β a) : ∀ a, a ∈ xs → β a
  | a, h => f a (List.mem_cons_of_mem _ h)
#align fin_enum.pi.tail FinEnum.Pi.tail

/-- `Pi xs f` creates the list of functions `g` such that, for `x ∈ xs`, `g x ∈ f x` -/
def Pi {β : α → Type max u v} [DecidableEq α] :
    ∀ xs : List α, (∀ a, List (β a)) → List (∀ a, a ∈ xs → β a)
  | [], _ => [fun x h => (List.not_mem_nil x h).elim]
  | x :: xs, fs => FinEnum.Pi.cons x xs <$> fs x <*> Pi xs fs
#align fin_enum.pi FinEnum.Pi

theorem mem_pi {β : α → Type _} [FinEnum α] [∀ a, FinEnum (β a)] (xs : List α)
    (f : ∀ a, a ∈ xs → β a) : f ∈ Pi xs fun x => toList (β x) :=
  by sorry

#align fin_enum.mem_pi FinEnum.mem_pi

/-- enumerate all functions whose domain and range are finitely enumerable -/
def Pi.enum (β : α → Type _) [FinEnum α] [∀ a, FinEnum (β a)] : List (∀ a, β a) :=
  (Pi (toList α) fun x => toList (β x)).map (fun f x => f x (mem_to_list _))
#align fin_enum.pi.enum FinEnum.Pi.enum

theorem Pi.mem_enum {β : α → Type _} [FinEnum α] [∀ a, FinEnum (β a)] (f : ∀ a, β a) :
    f ∈ Pi.enum β := by simp [Pi.enum] ; refine' ⟨fun a _ => f a, mem_pi _ _, rfl⟩
#align fin_enum.pi.mem_enum FinEnum.Pi.mem_enum

instance Pi.finEnum {β : α → Type _} [FinEnum α] [∀ a, FinEnum (β a)] : FinEnum (∀ a, β a) :=
  ofList (Pi.enum _) fun _ => Pi.mem_enum _
#align fin_enum.pi.fin_enum FinEnum.Pi.finEnum

instance pfunFinEnum (p : Prop) [Decidable p] (α : p → Type) [∀ hp, FinEnum (α hp)] :
    FinEnum (∀ hp : p, α hp) :=
  if hp : p then
    ofList ((toList (α hp)).map fun x _ => x) (by intro x ; simp ; exact ⟨x hp, rfl⟩)
  else ofList [fun hp' => (hp hp').elim] (by intro ; simp ; ext hp' ; cases hp hp')
#align fin_enum.pfun_fin_enum FinEnum.pfunFinEnum

end FinEnum

[zbatt]

the piece in question is the last 4 instances which in mathlib3 have an argument β : α → Type <something involving u and v>. A particular example would be Pi.enum haing an argument β : α → Type (max u v) This is as far as I could cut the file without breaking the bit in quesiton, hopefully its ok.

[Mario Carneiro]

It works if you use

def Pi.enum (β : α → Type (max u v)) [FinEnum α] [∀ a, FinEnum (β a)] : List (∀ a, β a) :=
  (Pi.{u, v} (toList α) fun x => toList (β x)).map (fun f x => f x (mem_to_list _))

[Mario Carneiro]

You can't infer the universes purely from the output type being Type (max u v), since Pi.{u, v} and Pi.{u, max u v} have the same type

[Mario Carneiro]

The reason lean 3 behaves differently here is because the type and value of a def are elaborated separately in lean 4

[zbatt]

Ah ok that makes sense. Thank you so much!

[zbatt]

A bit tangential, but are there good places to read more about intricacies of lean such as this so I can attempt to debug similar issues in the future?

[Mario Carneiro]

not really... usually "intricacies" are all very diverse things so it's hard to put them all in one collection

[zbatt]

Makes sense

[zbatt]

Thank you for your help with this!

[Arien Malec]

I think my TProd issue is similar:

import Mathlib.Data.List.Nodup

open List Function

variable {ι : Type _} {α : ι → Type _} {i j : ι} {l : List ι} {f : ∀ i, α i}

namespace List

variable (α)

/-- The product of a family of types over a list. -/
def TProd (l : List ι) : Type _ :=
  l.foldr (fun i β => α i × β) PUnit

variable {α}

namespace TProd

open List

protected def mk : ∀ (l : List ι) (f : ∀ i, α i), TProd α l
  | [] => fun _ => PUnit.unit
  | i :: is => fun f => (f i, TProd.mk is f)

@[simp]
theorem snd_mk (i : ι) (l : List ι) (f : ∀ i, α i) : (TProd.mk (i :: l) f).2 = TProd.mk l f :=
  rfl

gives:

stuck at solving universe constraint
  max ?u.1430 ?u.1507 =?= max ?u.1430 ?u.1458
while trying to unify
  (TProd (fun i => α i) l) ι (fun i => α i) l
with
  (foldr (fun i β => (fun i => α i) i × β) PUnit l) ι (foldr (fun i β => (fun i => α i) i × β) PUnit l)
    (fun i β => (foldr (fun i β => (fun i => α i) i × β) PUnit l) ((fun i => α i) i) β)
    (foldr (fun i β => (fun i => α i) i × β) PUnit l) l

I think the placeholder universes are leading Lean to infer different universe levels here?

[Arien Malec]

But explicitly naming my universes doesn't help...

[Arien Malec]

Uh, so actually it does.

[Arien Malec]

https://en.wikipedia.org/wiki/Rubber_duck_debugging