type error with a strange error message

Stream: new members

[Nicolas Rolland]

This error message is not very useful, and I don't know why the file below spits an error.
What is the real type error at play ?

-- type mismatch
-- t'
-- has type
-- LimitCone (Functor.empty Cat) : Type (max (max (u + 1) (v + 1)) u v)
-- but is expected to have type
-- LimitCone (Functor.empty Cat) : Type (max (max (u + 1) (v + 1)) u v)

import Mathlib.CategoryTheory.ChosenFiniteProducts

namespace CategoryTheory.Cat

open Limits

def terminal : (LimitCone (Functor.empty Cat)) := {
    cone := asEmptyCone (Cat.of (Discrete PUnit)),
    isLimit := sorry
  }

instance GOOD : ChosenFiniteProducts Cat where
  product (X Y : Cat): _ := sorry
  terminal  := terminal

instance BAD.{v,u} : ChosenFiniteProducts Cat.{v,u} where
  product (X Y : Cat): _ := sorry
  terminal  := by have t :  (_ : Type (max (u + 1) (v + 1)) ):= terminal
                  have t' : (_ : Type (max (max (u + 1) (v + 1)) u v)) := t
                  exact t'
                  -- type mismatch
                  --   t'
                  -- has type
                  --   LimitCone (Functor.empty Cat) : Type (max (max (u + 1) (v + 1)) u v)
                  -- but is expected to have type
                  --   LimitCone (Functor.empty Cat) : Type (max (max (u + 1) (v + 1)) u v)

end CategoryTheory.Cat

[Riccardo Brasca]

You can try convert t' to see the difference between the two terms

[Nicolas Rolland]

where is convert defined ?

using

set_option pp.universes true

I could get more info :

-- type mismatch
--   t'
-- has type
--   LimitCone.{0, 0, max u v, (max u v) + 1}
--     (Functor.empty.{0, max u v, (max u v) + 1} Cat.{max u v, max u v}) : Type (max (max (u + 1) (v + 1)) u v)
-- but is expected to have type
--   LimitCone.{0, 0, max u v, max (u + 1) (v + 1)}
--     (Functor.empty.{0, max u v, max (u + 1) (v + 1)} Cat.{v, u}) : Type (max (max (u + 1) (v + 1)) u v)

(I think the underlying error itself is related to the category instance of Discrete which is a "small category" aka Cat.{u,u})

[Damiano Testa]

Nicolas Rolland said:

where is convert defined ?

These both work:

import Mathlib

-- import Mathlib.Tactic.Convert
#min_imports in (← `(tactic| convert h))

#min_imports in  -- import Mathlib.Tactic.Convert
example (h : 0 = 0) : 0 = 0 := by
  convert h