unfold theorem generation produces declaration with left-over universe metavariables

[lovely-error]

def iscoh_wmap {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
  fun f => @Subtype (B -> A) fun r => ∀ a , a = r (f a)
def wmap : Type _ -> Type _ -> Type _ :=
  fun A B => @Sigma (A -> B) fun f => iscoh_wmap f

def hgroup : Nat -> Type _ -> Type _
| .zero , T => wmap T T
| .succ a, T => wmap (hgroup a T) (hgroup a T)

example : hgroup 0 Unit := by 
  -- unfold hgroup -- uncomment here
  admit

The error is this

(kernel) declaration has metavariables 'hgroup.eq_def'

This shouldn't happen right?

[nomeata]

Nope, clearly a bug in the unfold theorem generation code.

Here is a way to see the term with the universe meta variables left:

import Lean

def iscoh_wmap {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
  fun f => @Subtype (B -> A) fun r => ∀ a , a = r (f a)
def wmap : Type _ -> Type _ -> Type _ :=
  fun A B => @Sigma (A -> B) fun f => iscoh_wmap f

def hgroup : Nat -> Type _ -> Type _
| .zero , T => wmap T T
| .succ a, T => wmap (hgroup a T) (hgroup a T)

theorem foo : hgroup.eq_1 = hgroup.eq_1 := rfl

open Lean Meta
namespace Lean.Elab.Eqns
def mkUnfoldEq' (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
  withOptions (tactic.hygienic.set · false) do
    let baseName := declName
    lambdaTelescope info.value fun xs body => do
      let us := info.levelParams.map mkLevelParam
      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
      let goal ← mkFreshExprSyntheticOpaqueMVar type
      mkUnfoldProof declName goal.mvarId!
      let type ← mkForallFVars xs type
      let value ← mkLambdaFVars xs (← instantiateMVars goal)
      let name := Name.str baseName unfoldThmSuffix
      logInfo m!"value := {value}"
      addDecl <| Declaration.thmDecl {
        name, type, value
        levelParams := info.levelParams
      }
      return name

set_option pp.universes true

run_meta
  let env ← getEnv
  let .some eic := Structural.eqnInfoExt.find? env ``hgroup |>.map (·.toEqnInfoCore) | throwError "bad"
  let _ ← mkUnfoldEq' ``hgroup  eic

produces

value := fun x x_1 =>
  hgroup.match_1.splitter.{u_1, u_2, 0}
    (fun x_2 x_1_1 =>
      Eq.{1} x x_2 →
        Eq.{(max u_1 u_2) + 2} x_1 x_1_1 →
          Eq.{(max u_1 u_2) + 2} (hgroup.{u_1, u_2} x x_1)
            (match x, x_1 with
            | Nat.zero, T => wmap.{max u_1 u_2, max u_1 u_2} T T
            | Nat.succ a, T => wmap.{max u_1 u_2, max u_1 u_2} (hgroup.{u_1, u_2} a T) (hgroup.{u_1, u_2} a T)))
    x x_1
    (fun T h =>
      Eq.ndrec.{0, 1} (motive := fun x =>
        Eq.{(max u_1 u_2) + 2} x_1 T →
          Eq.{(max u_1 u_2) + 2} (hgroup.{u_1, u_2} x x_1)
            (match x, x_1 with
            | Nat.zero, T => wmap.{max u_1 u_2, max u_1 u_2} T T
            | Nat.succ a, T => wmap.{max u_1 u_2, max u_1 u_2} (hgroup.{u_1, u_2} a T) (hgroup.{u_1, u_2} a T)))
        (fun h => id.{0} (hgroup.eq_1.{u_1, u_2} x_1)) (Eq.symm.{1} h))
    (fun a T h =>
      Eq.ndrec.{0, 1} (motive := fun x =>
        Eq.{(max u_1 u_2) + 2} x_1 T →
          Eq.{(max u_1 u_2) + 2} (hgroup.{u_1, u_2} x x_1)
            (match x, x_1 with
            | Nat.zero, T => wmap.{max u_1 u_2, max u_1 u_2} T T
            | Nat.succ a, T => wmap.{max u_1 u_2, max u_1 u_2} (hgroup.{u_1, u_2} a T) (hgroup.{u_1, u_2} a T)))
        (fun h => id.{0} (hgroup.eq_1.{?u.2617, ?u.2616} (hgroup.{u_1, u_2} a x_1))) (Eq.symm.{1} h))
    (Eq.refl.{1} x) (Eq.refl.{(max u_1 u_2) + 2} x_1)

note the hgroup.eq_1.{?u.2617, ?u.2616}

[nomeata]

The type of hgroup is inferred as

hgroup.{u_1, u_2} : Nat → Type (max u_1 u_2) → Type (max u_1 u_2)

The problem goes away if the universes of hgroup are given explicitly:

def hgroup : Nat -> Type u -> Type u

It’s not quite surprising that applying

theorem hgroup.eq_1.{u_1, u_2} : ∀ (x : Type (max u_1 u_2)), hgroup Nat.zero x = wmap x x :=
fun x => Eq.refl (hgroup Nat.zero x)

will not solve for u_1 and u_2, so maybe the problem can be avoided earlier?

So far my initial debugging.