Debugging universe levels for minimal brecOn metatheory

Stream: Type theory

[nrs]

I've been attempting to make a small formalization of brecOn to get a better hang of Lean's metatheory. In the code below, Ctors is implicitly representing an inductive type by exhausting its constructors. Let ctors : Ctors. Then i : ctors.ctor_indexer will provide an index that will allow us to grab a constructor through ctors.ctor_at i, and so term : ctors.ctor_at i is effectively a value of the type given by ctors. This is encoded in the TermOf structure. Ctors is a special case of mathlib'sPFunctor and TermOf is a special case of mathlib's WType, and we encode Lean's rec by giving a way to witness some motive for each constructor.

Everything was going more or less well until the definition of brecOn_aux in the code that follows, which fails to solve universe levels, and I'm not entirely sure I understand why. Before below, it seems to me we don't need more than one universe, but to encode below we need at least two universes: one containing the witness of the motive, and another one containing the witnessing that there is a witness to the motive, which needs to be a single universe level higher (right?), and from this point onwards I think we need to start keeping explicit track of universe levels, because just using Type _ will produce said failure to solve universe level constraints at brecOn_aux.

I am not entirely sure how to progress forwards given this fact. Anyone have hints/suggestions/free associations to share from looking at the code below? Meanwhile I will be reviewing the source code for inductive types, the code for compile_inductive and Mario Carneiro's metatheory code.

structure Ctors where
  ctor_indexer : Type
  ctor_at : ctor_indexer -> Type _

structure TermOf (ctors : Ctors) where
  ctor_choice : ctors.ctor_indexer
  ctor_wness : ctors.ctor_at ctor_choice
  continuation_index : ctors.ctor_indexer
  continuation : ctors.ctor_at continuation_index -> TermOf ctors

structure rec (ctors : Ctors) where
  indexed_motives : (ctor_choice : ctors.ctor_indexer) -> ((ctor_wness : ctors.ctor_at ctor_choice) -> Type _)
  motive_wness_from_term : (term : TermOf ctors) -> indexed_motives term.ctor_choice term.ctor_wness

def below (base_rec : rec ctors) : rec ctors where
  indexed_motives := (fun _ _ => Type _)
  motive_wness_from_term := fun term => PProd
    (base_rec.indexed_motives term.ctor_choice term.ctor_wness)
    (Type _)

-- failure to solve universe levels in the following
def brecOn_aux (base_rec : rec ctors) : rec ctors where
  indexed_motives := fun ctor_choice ctor_wness => PProd
    (base_rec.indexed_motives ctor_choice ctor_wness)
    ((below base_rec).indexed_motives ctor_choice ctor_wness)
  motive_wness_from_term := fun term => .mk
    (base_rec.motive_wness_from_term term)
    ((below base_rec).motive_wness_from_term term)
-- if definition had succeeded, we would have defined brecOn by projecting the left value from the above's `motive_wness_from_term`

[nrs]

was re-reading Lean's below and might have made a mistake in my encoding above. Here's another version that works and doesn't need explicit universe levels. comments or suggestions are still welcome!

structure Ctors where
  ctor_indexer : Type
  ctor_at : ctor_indexer -> Type _

structure TermOf (ctors : Ctors) where
  ctor_choice : ctors.ctor_indexer
  ctor_wness : ctors.ctor_at ctor_choice
  continuation_index : ctors.ctor_indexer
  continuation : ctors.ctor_at continuation_index -> TermOf ctors

structure rec (ctors : Ctors) where
  indexed_motives : (ctor_choice : ctors.ctor_indexer) -> ((ctor_wness : ctors.ctor_at ctor_choice) -> Type _)
  motive_wness_from_term : (term : TermOf ctors) -> indexed_motives term.ctor_choice term.ctor_wness

def below (base_rec : rec ctors) : rec ctors where
  indexed_motives := (fun _ _ => Type _)
  motive_wness_from_term := fun term => @PProd
    (base_rec.indexed_motives term.ctor_choice term.ctor_wness)
    (ctors.ctor_at term.ctor_choice)

def brecOn_aux (base_rec : rec ctors) : rec ctors where
  indexed_motives := fun ctor_choice ctor_wness => Prod
    (base_rec.indexed_motives ctor_choice ctor_wness)
    ((below base_rec).indexed_motives ctor_choice ctor_wness)
  motive_wness_from_term := fun term => .mk
    (base_rec.motive_wness_from_term term)
    ((below base_rec).motive_wness_from_term term)

def brecOn (base_rec : rec ctors) : rec ctors where
  indexed_motives := fun ctor_choice ctor_wness => base_rec.indexed_motives ctor_choice ctor_wness
  motive_wness_from_term := fun term => ((brecOn_aux base_rec).motive_wness_from_term <| term).fst

edit: the above will not work, a working definition needs to stick closer to the definitions for polynomial functors and wtypes