Universe polymorphic typeclass constraints

Stream: general

[Harry Goldstein]

Some quick background — I'm working with a type G that is Type → Type 1 and I wanted to use it with Traversable, so I had to generalize the typeclass a bit:

class MyTraversable (t : Type u → Type u) : Type (max (u + 1) (v + 1)) extends Functor t where
  -- NOTE: Previously `m` was constrained to have type `Type u → Type u`
  traverse : ∀ {m : Type u → Type v} [Monad m] {α β}, (α → m β) → t α → m (t β)

This works, but the extra parameter v does some weird things to typeclass resolution. In particular, I have a function that needs MyTraversable t at both Type 1 and Type 2, and the only solution I've come up with is to just add the constraint twice.

Here's a full MWE:

class MyTraversable (t : Type u → Type u) : Type (max (u + 1) (v + 1)) extends Functor t where
  -- NOTE: Previously `m` was constrained to have type `Type u → Type u`
  traverse : ∀ {m : Type u → Type v} [Monad m] {α β}, (α → m β) → t α → m (t β)

variable (G : Type → Type 1)
variable [Monad G]
variable (mkG? : ∀ {α}, α → G (Option α))

open MyTraversable in
def foo
    [MyTraversable t]
    [MyTraversable t] -- NOTE: Only works when I constrain this twice, once at Type 1 and once at Type 2
    {α : Type}
    (xs : t α) :
    G (Option (t α)) :=
  let xs' : G (t (Option α)) := traverse mkG? xs -- Needs MyTraversable t : Type 2
  traverse id <$> xs' -- Needs MyTraversable t : Type 1

Is there a better way to do this? Or is this just expected behavior?

[Kyle Miller]

Maybe there's a clever trick somehow, but unfortunately universe polymorphism can occur only at the top level (think "implicit forall" for universes at the very beginning of the declaration's type, and only there). That means everything else has to be specialized to some universe levels.

[Eric Wieser]

[MyTraversable.{_,0} t] [MyTraversable.{_,1} t] is probably more idiomatic

[Eric Wieser]

You could also consider swapping the order of the universe arguments (with class MyTraversible.{v,u}) to avoid the need for the _,, and adding @[pp_with_univ] from mathlib to ensure the infoview shows the universes.

[Harry Goldstein]

These are great suggestions, thanks! The explicit universes at least makes it clear to a reader what's going on, which is probably good enough.