Universe issue in computable inductive type

Stream: lean4

[Arend Mellendijk]

I'm having universe issues with an inductive type. In short I'm trying to add a type parameter to
docs#Mathlib.Tactic.Ring.ExProd, but the parameter forces the inductive type to live in Type 1
instead of Type. This is a problem because MetaM : Type → Type, so I can't compute with anything in
Type 1.

Here's a (slightly) simplified example of what I'm dealing with:

import Mathlib
open Qq

inductive Ex : ∀ {u : Lean.Level} (α : Q(Type u)), (Q($α) → Type) → (e : Q($α)) → Type 1
| const {u : Lean.Level} {α : Q(Type u)} {type : Q($α) → Type}
    {e : Q($α)} (c : type e) :  Ex α type e
| mul {u : Lean.Level} {α : Q(Type u)} {type : Q($α) → Type} {a t m : Q($α)} {e : Q(ℕ)}
    (base : Ex α type a) (exp : Ex q(ℕ) (fun _ ↦ ℕ) e) (tail : Ex α type t) : Ex α type m

I tried to bump down the universe level by turning the arguments into parameters, but the exp argument of the mul constructor passes a different type, so that doesn't work:

/-
(kernel) arg #8 of 'Mathlib.Tactic.Algebra.Ex'.mul' contains a non valid occurrence of the datatypes being declared
-/
inductive Ex' {u : Lean.Level} (α : Q(Type u)) (type : Q($α) → Type) : (e : Q($α)) → Type
| const {e : Q($α)} (c : type e) : Ex' α type e
| mul {a t m : Q($α)} {e : Q(ℕ)}
    (base : Ex' α type a) (exp : Ex' q(ℕ) (fun _ ↦ ℕ) e) (tail : Ex' α type t) : Ex' α type m

How should I deal with this? Ideally I'd like to just be able to compute with the first definition.

[Aaron Liu]

why do you need a Q($α) → Type

[Arend Mellendijk]

It's not evident from this snippet but I want to define operations on this type that are annotated using Qq, for example:

evalAdd : ∀ {x y : Q($α)}, type x → type y → Ring.Result type q($x + $y)

See docs#Mathlib.Tactic.Ring.Result

[Aaron Liu]

Arend Mellendijk said:

I tried to bump down the universe level by turning the arguments into parameters, but the exp argument of the mul constructor passes a different type, so that doesn't work:

Can you factor out the Ex q(ℕ) (fun _ ↦ ℕ) as a separate inductive?

[Arend Mellendijk]

That could work, but it does seem unsatisfactory. I'm adding this parameter to deduplicate code in an open PR, so special-casing Nat feels like a step backwards. It also adds a bunch of (seemingly) unnecessary casting back and forth.

I'll do this for now, but I'm still very open to other ideas.

[Eric Wieser]

Generally it's a mess to put Qq inside inductive types, because as the user you care about matching expressions in indices up to defeq, but Lean will match them up to exact equality of expression constructors.