Universe constraint solving problem

Stream: new members

[Ching-Tsun Chou]

I have some code that looks like the following:

import Mathlib.Data.Set.Card
import Mathlib.Data.Sigma.Basic

class C where
  T : Type*
  s : Set T

def C_sigma {I : Type*} (F : I → C) : C where
  T := Σ i : I, (F i).T
  s := ⋃ i : I, Sigma.mk i '' (F i).s

example (I : Type*) (F : I → C) :
    ∃ G : C, G = G := by
  use (C_sigma F)
  sorry

At the tactic use (C_sigma F), I got the following error message:

failed to solve universe constraint
u_3 =?= max ?u.117 ?u.118
while trying to unify
C : Type (u_3 + 1)
with
C : Type ((max u_2 u_1) + 1)

How do I fix this problem?
[ Needless to say, the real goal I want to prove is not G = G. The only purpose of the above code is to exhibit the problem. ]

[Eric Wieser]

Every time you writeC, Lean is interpreting this as C.{_}. If you fill in these underscores with u and v after universes u v then hopefully the issue will become clear

[Ching-Tsun Chou]

@Eric Wieser Sorry, I don't quite understand what you wrote. Could you elaborate a little?

[Eric Wieser]

import Mathlib.Data.Set.Card
import Mathlib.Data.Sigma.Basic

universe u v w

class C where
  T : Type u
  s : Set T

def C_sigma {I : Type u} (F : I → C.{v}) : C.{max u v} where
  T := Σ i : I, (F i).T
  s := ⋃ i : I, Sigma.mk i '' (F i).s

example (I : Type u) (F : I → C.{v}) :
    ∃ G : C.{w}, G = G := by
  use (C_sigma F) -- still fails, but now you know which is which
  sorry

example (I : Type u) (F : I → C.{v}) :
    ∃ G : C.{max u v}, G = G := by
  use (C_sigma F)  -- succeeds