!4#4761 universe issues

Stream: mathlib4

[Kevin Buzzard]

I'm trying to solve the universe issues in !4#4761 . This should work on master:

import Mathlib.Algebra.Category.ModuleCat.Abelian

universe u

variable (k : Type u) [Ring k]

open CategoryTheory Limits

set_option pp.universes true in
#synth HasLimitsOfSize.{u, u, u, u+1} (ModuleCat.{u, u} k)
-- ModuleCat.instHasLimitsOfSizeModuleCatMaxModuleCategory.{?u.54, u, u}

This is an issue in the PR because even though I'm specifying all universes in the input, I still have a universe variable in the output. This leads to the usual problematic

stuck at solving universe constraint
  u =?= max u ?u.84829

later on, which I am not entirely sure how to fix. I am not entirely clear how to solve this issue.

[Mario Carneiro]

What is docs4#ModuleCat.instHasLimitsOfSizeModuleCatMaxModuleCategory ?

[Mario Carneiro]

that's a bad instance

[Mario Carneiro]

Actually it seems it would work to use

#synth HasLimitsOfSize.{u, u, u, u+1} (ModuleCatMax.{u, u} k)

[Mario Carneiro]

This issue is what the TypeMax stuff was about

[Kevin Buzzard]

That instance is already defined using ModuleCatMax!

I can't get typeclass inference to do the first (currently failing) example in the PR. I think it's a universe issue and the hints above aren't enough for me to solve it. Here's the issue on master:

import Mathlib.Algebra.Category.ModuleCat.Abelian
import Mathlib.RepresentationTheory.Action

universe v₁ v₂ u

variable (k : Type u) [Ring k]

open CategoryTheory Limits Action

variable (V : Type (u + 1)) [LargeCategory V] (M : MonCat.{u})

-- naming an instance
noncomputable instance foo [HasLimits V] : PreservesLimits (forget V M) :=
inferInstance

abbrev Rep (k G : Type u) [Ring k] [Monoid G] :=
  Action (ModuleCat.{u} k) (MonCat.of G)

variable (k G : Type u) [Ring k] [Monoid G]

noncomputable example : PreservesLimits (forget₂ (Rep k G) (ModuleCat.ModuleCatMax.{u, u} k)) :=
-- inferInstance -- fails
-- foo (ModuleCat.ModuleCatMax k) (MonCat.of G) -- stuck at solving universe constraint
foo (ModuleCat.ModuleCatMax.{u, u} k) (MonCat.of G) -- works

The idea is that we want typeclass inference to do it. The universe constraint errors are:

1)
stuck at solving universe constraint
  u =?= max ?u.25910 ?u.25911
while trying to unify
  Category ((Category (ModuleCat.ModuleCatMax k)) k inst✝¹)
with
  (Category (ModuleCat k)) ((Category (ModuleCat k)) k inst✝¹)

2)
stuck at solving universe constraint
  max ?u.25910 ?u.25911 =?= max u ?u.25910
while trying to unify
  HasLimitsOfSize ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)
with
  (HasLimitsOfSize (ModuleCat.ModuleCatMax k)) ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)
    ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)

3)
stuck at solving universe constraint
  u =?= max u ?u.25910
while trying to unify
  HasLimitsOfSize ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)
with
  (HasLimitsOfSize (ModuleCat.ModuleCatMax k)) ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)
    ((HasLimitsOfSize (ModuleCat.ModuleCatMax k)) k inst✝¹)

4)
stuck at solving universe constraint
  u+1 =?= max (max u (?u.25910+1)) (?u.25911+1)
while trying to unify
  Type (u + 1) : Type (u + 2)
with
  Type (max u ((max ?u.25911 ?u.25910) + 1)) : Type (max (u + 1) ((max ?u.25911 ?u.25910) + 2))