universe weirdness

Stream: general

[Kevin Buzzard]

I define a function twice using two different methods and the resulting definitions have slightly different types.

def with_zero (α) := option α

instance : monad with_zero := option.monad

def with_zero.map {α β : Type*} (f : α → β) : with_zero α → with_zero β := functor.map f
def with_zero.map' {α β : Type*} (f : α → β) : with_zero α → with_zero β := option.map f

#check @with_zero.map
-- with_zero.map : Π {α β : Type u_1}, (α → β) → with_zero α → with_zero β
#check @with_zero.map'
-- with_zero.map' : Π {α : Type u_1} {β : Type u_2}, (α → β) → with_zero α → with_zero β

In the map version, the universes of alpha and beta have magically become the same.

[Mario Carneiro]

When you use Type*, that's basically a universe metavariable Type ?u. It gets unified in the definition

[Kevin Buzzard]

I had never understood that before.

[Mario Carneiro]

if you use Type u and Type v you will get an error on the first one

[Mario Carneiro]

this is why Type* is not used in core, in favor of explicit universes

[Mario Carneiro]

It's a bit more explicit but I think being able to almost completely forget about universes is more worthwhile