Phantom universe implicit

Stream: lean4

[cognivore]

Dear all, I'm using Foladble defined as follows.

class Foldable (T : Type u → Type v) where
  fold : [HMul M M M] → [One M] → T M → M
  foldr : (A → B → B) → B → T A → B
  foldl : (A → B → A) → A → T B → A

I then define a classic asum function as follows:

def asum {f : Type u → Type v} {t : Type v → Type v}
         [Foldable t] [Alternative f] (fas : t (f α)) : f α :=
  Foldable.foldr (fun a b => a <|> b) Alternative.failure fas

However, when I inspect its implicits, I see:

Megaparsec.Common.asum.{u, v,
  u_1} : {α : Type u} →
  {f : Type u → Type v} → {t : Type v → Type v}
  → [inst : Foldable t] → [inst : Alternative f] → t (f α) → f α

Where did universe u_1 come from? It doesn't seem to be used.

[Mario Carneiro]

if you mouse over foldl and foldr you will see that B is unconstrained in foldr and A is unconstrained in foldl, resulting in two additional universe parameters to Foldable

[Mario Carneiro]

that is,

class Foldable.{a, b, u, v} (T : Type u → Type v) where
  fold {M : Type u} : [HMul M M M] → [One M] → T M → M
  foldr {A : Type u} {B : Type b} : (A → B → B) → B → T A → B
  foldl {A : Type a} {B : Type u} : (A → B → A) → A → T B → A

[pcpthm]

Setting pp.universes true reveals u_1 is used in Foldable as Mario says:

set_option pp.universes true in
#print asum

def asum.{u, v, u_1} : {α : Type u} →
  {f : Type u → Type v} →
    {t : Type v → Type v} → [inst : Foldable.{v, v, v + 1, u_1} t] → [inst : Alternative.{u, v} f] → t (f α) → f α := ...