chore: update stage0

2021-02-25 17:09:12 -08:00 · 2021-02-25 17:09:12 -08:00 · 5cfa9504ca
commit 5cfa9504ca
parent 0c1c6c0a73
15 changed files with 2439 additions and 1982 deletions
--- a/stage0/src/Init/Control/Lawful.lean
+++ b/stage0/src/Init/Control/Lawful.lean
@ -10,6 +10,9 @@ import Init.Control.StateRef

 open Function

+@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
+  rfl
+
 class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
  map_const          : (Functor.mapConst : α → f β → f α) = Functor.map ∘ const β
  id_map   (x : f α) : id <$> x = x
@ -27,8 +30,8 @@ class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFu
  seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
  pure_seq    (g : α → β) (x : f α)   : pure g <*> x = g <$> x
  map_pure    (g : α → β) (x : α)     : g <$> (pure x : f α) = pure (g x)
-  seq_pure    (g : f (α → β)) (x : α) : g <*> pure x = (fun h : α → β => h x) <$> g
-  seq_assoc   (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = (@comp α β γ <$> h) <*> g <*> x
+  seq_pure    (g : f (α → β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
+  seq_assoc   (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = ((. ∘ .) <$> h) <*> g <*> x
  comp_map g h x := by
    repeat rw [← pure_seq]
    simp [seq_assoc, map_pure, seq_pure]
@ -65,9 +68,19 @@ attribute [simp] pure_bind bind_assoc
 theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
  rw [← bind_pure_comp]

+theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α) : f <*> x = f >>= (. <$> x) := by
+  rw [← bind_map]
+
 theorem bind_congr [Bind m] {x : m α} {f g : α → m β} (h : ∀ a, f a = g a) : x >>= f = x >>= g := by
  simp [funext h]

+@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x := by
+  have (x >>= fun _ => pure ⟨⟩) = (x >>= pure) by
+    apply bind_congr; intro u
+    cases u; simp
+  rw [bind_pure] at this
+  assumption
+
 theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
  simp [funext h]

@ -75,14 +88,10 @@ theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α →
  rw [bind_map]

 theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
-  rw [seqRight_eq, ← bind_map, ← bind_pure_comp]
-  simp [Function.const]
+  rw [seqRight_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]

 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
-  rw [seqLeft_eq, ← bind_map, ← bind_pure_comp]
-  simp
-  apply bind_congr; intro
-  rw [← bind_pure_comp]
+  rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]

 /- Id -/

@ -106,9 +115,18 @@ theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
  assumption

@[simp] theorem run_pure [Monad m] : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
+
@[simp] theorem run_lift [Monad m] : run (ExceptT.lift x : ExceptT ε m α) = Except.ok <$> x := rfl
+
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
-@[simp] theorem run_bind [Monad m] (x : ExceptT ε m α)
+
+@[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
+  simp[ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont, map_eq_pure_bind]
+
+@[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
+  simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
+
+theorem run_bind [Monad m] (x : ExceptT ε m α)
        : run (x >>= f : ExceptT ε m β)
          =
          run x >>= fun
@ -121,8 +139,7 @@ theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by

@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
    : (f <$> x).run = Except.map f <$> x.run := by
-  rw [← bind_pure_comp (m := m)]
-  simp [Functor.map, ExceptT.map]
+  simp [Functor.map, ExceptT.map, map_eq_pure_bind]
  apply bind_congr
  intro a; cases a <;> simp [Except.map]

@ -136,20 +153,19 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
  show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
  rw [← ExceptT.bind_pure_comp]
  apply ext
-  simp
+  simp [run_bind]
  apply bind_congr
-  intro a
-  cases a with
-  | error => simp
-  | ok =>
-    simp; rw [← bind_pure_comp]; apply bind_congr; intro b;
+  intro
+  | Except.error _ => simp
+  | Except.ok _ =>
+    simp [map_eq_pure_bind]; apply bind_congr; intro b;
    cases b <;> simp [comp, Except.map, const]

 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
  show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
  rw [← ExceptT.bind_pure_comp]
  apply ext
-  simp
+  simp [run_bind]
  apply bind_congr
  intro a; cases a <;> simp

@ -158,11 +174,11 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
  map_const      := by intros; rfl
  seqLeft_eq     := ExceptT.seqLeft_eq
  seqRight_eq    := ExceptT.seqRight_eq
-  pure_seq       := by intros; apply ext; simp [ExceptT.seq_eq]
+  pure_seq       := by intros; apply ext; simp [ExceptT.seq_eq, run_bind]
  bind_pure_comp := ExceptT.bind_pure_comp
  bind_map       := by intros; rfl
-  pure_bind      := by intros; apply ext; simp
-  bind_assoc     := by intros; apply ext; simp; apply bind_congr; intro a; cases a <;> simp
+  pure_bind      := by intros; apply ext; simp [run_bind]
+  bind_assoc     := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp

 end ExceptT

@ -175,19 +191,27 @@ theorem ext [Monad m] {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ct
  exact funext h

@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
+
@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
    : (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
+
@[simp] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
    : (f <$> x).run ctx = f <$> x.run ctx := rfl
+
@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
    : (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
+
@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
    : (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
+
@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
+
@[simp] theorem run_seq {α β : Type u} [Monad m] [LawfulMonad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ) : (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := by
  rw [seq_eq_bind (m := m)]; rfl
+
@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x *> y).run ctx = (x.run ctx *> y.run ctx) := by
  rw [seqRight_eq_bind (m := m)]; rfl
+
@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ) : (x <* y).run ctx = (x.run ctx <* y.run ctx) := by
  rw [seqLeft_eq_bind (m := m)]; rfl

@ -216,6 +240,9 @@ namespace StateT
 theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
  funext h

+@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
+  rfl
+
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl

@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
@ -225,8 +252,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
  intro p; cases p; rfl

@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
-  simp [Functor.map, StateT.map, run]
-  rw [← bind_pure_comp]
+  simp [Functor.map, StateT.map, run, map_eq_pure_bind]
  apply bind_congr
  intro p; cases p; rfl

@ -234,7 +260,7 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=

@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl

-@[simp] theorem run_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
+@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl

@[simp] theorem run_monadMap [Monad m] [MonadFunctor n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ)
    : (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
@ -253,15 +279,13 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=

 theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
  apply ext; intro s
-  simp; rw [← bind_pure_comp]; simp
+  simp [map_eq_pure_bind]
  apply bind_congr; intro p; cases p
-  simp[Prod.ext]
+  simp [Prod.ext]

 theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
  apply ext; intro s
-  simp; rw [← bind_pure_comp]; simp
-  apply bind_congr; intro p; cases p
-  simp[Prod.ext, const]; rw [← bind_pure_comp]
+  simp [map_eq_pure_bind]

 instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
  id_map         := by intros; apply ext; intros; simp[Prod.ext]
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@ -603,20 +603,20 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}

 /- Universe polymorphic unit -/

-theorem punitEq (a b : PUnit) : a = b := by
+theorem PUnit.subsingleton (a b : PUnit) : a = b := by
  cases a; cases b; exact rfl

-theorem punitEqPUnit (a : PUnit) : a = () :=
-  punitEq a ()
+@[simp] theorem PUnit.eq_punit (a : PUnit) : a = () :=
+  PUnit.subsingleton a ()

 instance : Subsingleton PUnit :=
-  Subsingleton.intro punitEq
+  Subsingleton.intro PUnit.subsingleton

 instance : Inhabited PUnit where
  default := ⟨⟩

 instance : DecidableEq PUnit :=
-  fun a b => isTrue (punitEq a b)
+  fun a b => isTrue (PUnit.subsingleton a b)

 /- Setoid -/

--- a/stage0/src/Lean/Elab/Binders.lean
+++ b/stage0/src/Lean/Elab/Binders.lean
@ -477,23 +477,27 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
      `(@fun $x => $body)
  loop (getMatchAltsNumPatterns matchAlts) #[]

-@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match stx with
-  | `(fun $binders* => $body) => do
-    let (binders, body, expandedPattern) ← expandFunBinders binders body
-    if expandedPattern then
-      let newStx ← `(fun $binders* => $body)
-      withMacroExpansion stx newStx <| elabTerm newStx expectedType?
-    else
-      elabFunBinders binders expectedType? fun xs expectedType? => do
-        /- We ensure the expectedType here since it will force coercions to be applied if needed.
-           If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
-           and another instance for the dependent version. -/
-        let e ← elabTermEnsuringType body expectedType?
-        mkLambdaFVars xs e
-  | `(fun $m:matchAlts) => do
-    let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
-    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-  | _ => throwUnsupportedSyntax
+@[builtinTermElab «fun»] partial def elabFun : TermElab :=
+  fun stx expectedType? => loop stx expectedType?
+where
+  loop (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
+    match stx with
+    | `(fun $binders* => $body) => do
+      let (binders, body, expandedPattern) ← expandFunBinders binders body
+      if expandedPattern then
+        let newStx ← `(fun $binders* => $body)
+        loop newStx expectedType?
+      else
+        elabFunBinders binders expectedType? fun xs expectedType? => do
+          /- We ensure the expectedType here since it will force coercions to be applied if needed.
+             If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
+             and another instance for the dependent version. -/
+          let e ← elabTermEnsuringType body expectedType?
+          mkLambdaFVars xs e
+    | `(fun $m:matchAlts) => do
+      let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
+      withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+    | _ => throwUnsupportedSyntax

 /- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
   Otherwise, we create a term of the form `(fun (x : type) => body) val`
--- a/stage0/src/Lean/Elab/Deriving/Repr.lean
+++ b/stage0/src/Lean/Elab/Deriving/Repr.lean
@ -60,7 +60,7 @@ where
          patterns := patterns.push (← `(_))
        let mut ctorArgs := #[]
        let mut rhs := Syntax.mkStrLit (toString ctorInfo.name)
-        let mut rhs ← `(Format.text $rhs)
+        rhs ← `(Format.text $rhs)
        -- add `_` for inductive parameters, they are inaccessible
        for i in [:indVal.numParams] do
          ctorArgs := ctorArgs.push (← `(_))
@ -78,7 +78,7 @@ where
    return alts

 def mkBody (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
-  if isStructureLike (← getEnv) indVal.name then
+  if isStructure (← getEnv) indVal.name then
    mkBodyForStruct ctx header indVal
  else
    mkBodyForInduct ctx header indVal auxFunName
--- a/stage0/src/Lean/Elab/MutualDef.lean
+++ b/stage0/src/Lean/Elab/MutualDef.lean
@ -600,26 +600,40 @@ private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name
  else
    []

+/-- Eagerly convert universe metavariables occurring in theorem headers to universe parameters. -/
+private def levelMVarToParamHeaders (views : Array DefView) (headers : Array DefViewElabHeader) : TermElabM (Array DefViewElabHeader) := do
+  let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
+    let mut newHeaders := #[]
+    for view in views, header in headers do
+      if view.kind.isTheorem then
+        newHeaders := newHeaders.push { header with type := (← levelMVarToParam' header.type) }
+      else
+        newHeaders := newHeaders.push header
+    return newHeaders
+  let newHeaders ← process.run' 1
+  newHeaders.mapM fun header => return { header with type := (← instantiateMVars header.type) }
+
 def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
  let scopeLevelNames ← getLevelNames
  let headers ← elabHeaders views
+  let headers ← levelMVarToParamHeaders views headers
  let allUserLevelNames := getAllUserLevelNames headers
  withFunLocalDecls headers fun funFVars => do
    let values ← elabFunValues headers
    Term.synthesizeSyntheticMVarsNoPostponing
-    if isExample views then
-      pure ()
-    else
-      let values ← values.mapM (instantiateMVars ·)
-      let headers ← headers.mapM instantiateMVarsAtHeader
-      let letRecsToLift ← getLetRecsToLift
-      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-      checkLetRecsToLiftTypes funFVars letRecsToLift
-      withUsed vars headers values letRecsToLift fun vars => do
-        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-        let preDefs ← levelMVarToParamPreDecls preDefs
-        let preDefs ← instantiateMVarsAtPreDecls preDefs
-        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+    let values ← values.mapM (instantiateMVars ·)
+    let headers ← headers.mapM instantiateMVarsAtHeader
+    let letRecsToLift ← getLetRecsToLift
+    let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+    checkLetRecsToLiftTypes funFVars letRecsToLift
+    withUsed vars headers values letRecsToLift fun vars => do
+      let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+      let preDefs ← levelMVarToParamPreDecls preDefs
+      let preDefs ← instantiateMVarsAtPreDecls preDefs
+      let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+      if isExample views then
+        withoutModifyingEnv <| addPreDefinitions preDefs
+      else
        addPreDefinitions preDefs

 end Term
--- a/stage0/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/stage0/src/Lean/Elab/PreDefinition/Basic.lean
@ -31,15 +31,9 @@ def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Arra
  preDefs.mapM fun preDef => do
    pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }

-private def levelMVarToParamExpr (e : Expr) : StateRefT Nat TermElabM Expr := do
-  let nextIdx ← get
-  let (e, nextIdx) ← levelMVarToParam e nextIdx;
-  set nextIdx;
-  pure e
-
 private def levelMVarToParamPreDeclsAux (preDefs : Array PreDefinition) : StateRefT Nat TermElabM (Array PreDefinition) :=
  preDefs.mapM fun preDef => do
-    pure { preDef with type := (← levelMVarToParamExpr preDef.type), value := (← levelMVarToParamExpr preDef.value) }
+    pure { preDef with type := (← levelMVarToParam' preDef.type), value := (← levelMVarToParam' preDef.value) }

 def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
  (levelMVarToParamPreDeclsAux preDefs).run' 1
@ -98,7 +92,6 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U
    let env ← getEnv
    let decl :=
      match preDef.kind with
-      | DefKind.«example» => unreachable!
      | DefKind.«theorem» =>
        Declaration.thmDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value }
      | DefKind.«opaque»  =>
@ -108,7 +101,7 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U
        Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value,
                               hints := ReducibilityHints.«abbrev»,
                               safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
-      | DefKind.«def»  =>
+      | _ => -- definitions and examples
        Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value,
                               hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1),
                               safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
--- a/stage0/src/Lean/Meta/SynthInstance.lean
+++ b/stage0/src/Lean/Meta/SynthInstance.lean
@ -510,15 +510,17 @@ private def preprocess (type : Expr) : MetaM Expr :=
    let type ← whnf type
    mkForallFVars xs type

-private def preprocessLevels (us : List Level) : MetaM (List Level) := do
-  let mut r := []
+private def preprocessLevels (us : List Level) : MetaM (List Level × Bool) := do
+  let mut r := #[]
+  let mut modified := false
  for u in us do
    let u ← instantiateLevelMVars u
    if u.hasMVar then
-      r := (← mkFreshLevelMVar)::r
+      r := r.push (← mkFreshLevelMVar)
+      modified := true
    else
-      r := u::r
-  pure r.reverse
+      r := r.push u
+  return (r.toList, modified)

 private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) : MetaM (Array Expr) := do
  if h : i < args.size then
@ -532,7 +534,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) :
    | _ =>
      throwError "type class resolution failed, insufficient number of arguments" -- TODO improve error message
  else
-    pure args
+    return args

 private def preprocessOutParam (type : Expr) : MetaM Expr :=
  forallTelescope type fun xs typeBody => do
@ -540,15 +542,22 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
    | c@(Expr.const constName us _) =>
      let env ← getEnv
      if !hasOutParams env constName then
-        pure type
+        /- We treat all universe level parameters as "outParam" -/
+        let (us, modified) ← preprocessLevels us
+        if modified then
+          let c := mkConst constName us
+          mkForallFVars xs (mkAppN c typeBody.getAppArgs)
+        else
+          return type
      else do
        let args := typeBody.getAppArgs
-        let us    ← preprocessLevels us
+        let (us, _) ← preprocessLevels us
        let c := mkConst constName us
        let cType ← inferType c
        let args ← preprocessArgs cType 0 args
        mkForallFVars xs (mkAppN c args)
-    | _ => pure type
+    | _ =>
+      return type

 /-
  Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used.
@ -559,7 +568,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
  let opts ← getOptions
  let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
  let inputConfig ← getConfig
-  withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.reducible,
+  withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                          foApprox := true, ctxApprox := true, constApprox := false }) do
    let type ← instantiateMVars type
    let type ← preprocess type
--- a/stage0/stdlib/Lean/Elab/Binders.c
+++ b/stage0/stdlib/Lean/Elab/Binders.c
@ -182,6 +182,7 @@ lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_a
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_quoteAutoTactic___spec__5___lambda__1___closed__7;
 lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_quoteAutoTactic___spec__6___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_restoreSynthInstanceCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabFun_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_withoutPostponingUniverseConstraintsImp___rarg___closed__16;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__5;
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderIdent(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -239,7 +240,7 @@ lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_addLocalVarInfo(lea
 lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_getFunBinderIds_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__5;
-lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5383_(lean_object*);
+lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5388_(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__12;
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandBinderModifier___closed__8;
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_registerFailedToInferBinderTypeInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -370,7 +371,6 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___privat
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12336____closed__7;
 lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2191____closed__4;
-lean_object* l_Lean_Elab_Term_elabFun___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
 lean_object* l_Lean_Elab_Term_quoteAutoTactic___lambda__2___closed__6;
 extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_932____closed__3;
@ -463,6 +463,7 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___lambda__3___closed__2;
 lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabFun_loop___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__1;
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchAltsIntoMatchAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_elabBindersAux_loop___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -20580,7 +20581,7 @@ lean_dec(x_1);
 return x_4;
 }
 }
-lean_object* l_Lean_Elab_Term_elabFun___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
+lean_object* l_Lean_Elab_Term_elabFun_loop___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 lean_object* x_11; uint8_t x_12; lean_object* x_13; 
@ -20635,7 +20636,7 @@ return x_21;
 }
 }
 }
-lean_object* l_Lean_Elab_Term_elabFun(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+lean_object* l_Lean_Elab_Term_elabFun_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
 _start:
 {
 lean_object* x_10; uint8_t x_11; 
@ -20796,6 +20797,7 @@ return x_58;
 else
 {
 lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; uint8_t x_68; 
+lean_dec(x_1);
 x_59 = lean_unsigned_to_nat(0u);
 x_60 = l_Lean_Syntax_getArg(x_14, x_59);
 x_61 = lean_unsigned_to_nat(2u);
@ -20817,7 +20819,6 @@ lean_dec(x_67);
 if (x_68 == 0)
 {
 lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; 
-lean_dec(x_1);
 x_69 = lean_ctor_get(x_64, 1);
 lean_inc(x_69);
 lean_dec(x_64);
@ -20827,7 +20828,7 @@ lean_dec(x_65);
 x_71 = lean_ctor_get(x_66, 0);
 lean_inc(x_71);
 lean_dec(x_66);
-x_72 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabFun___lambda__1), 10, 1);
+x_72 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabFun_loop___lambda__1), 10, 1);
 lean_closure_set(x_72, 0, x_71);
 x_73 = l_Lean_Elab_Term_elabFunBinders___rarg(x_70, x_2, x_72, x_3, x_4, x_5, x_6, x_7, x_8, x_69);
 lean_dec(x_70);
@ -20835,7 +20836,7 @@ return x_73;
 }
 else
 {
-lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; 
+lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; 
 x_74 = lean_ctor_get(x_64, 1);
 lean_inc(x_74);
 lean_dec(x_64);
@ -20886,19 +20887,22 @@ x_97 = lean_array_push(x_87, x_96);
 x_98 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_98, 0, x_10);
 lean_ctor_set(x_98, 1, x_97);
-lean_inc(x_98);
-lean_inc(x_1);
-x_99 = lean_alloc_closure((void*)(l_Lean_Elab_Term_adaptExpander___lambda__1), 10, 3);
-lean_closure_set(x_99, 0, x_1);
-lean_closure_set(x_99, 1, x_98);
-lean_closure_set(x_99, 2, x_2);
-x_100 = l_Lean_Elab_withMacroExpansionInfo___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2(x_1, x_98, x_99, x_3, x_4, x_5, x_6, x_7, x_8, x_83);
-return x_100;
+x_1 = x_98;
+x_9 = x_83;
+goto _start;
 }
 }
 }
 }
 }
+lean_object* l_Lean_Elab_Term_elabFun(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l_Lean_Elab_Term_elabFun_loop(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+return x_10;
+}
+}
 static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabFun___closed__1() {
 _start:
 {
@ -22444,7 +22448,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Elab_Term_quoteAutoTactic___lambda__4___closed__1;
 x_2 = l_Lean_Elab_Term_elabLetDeclCore___closed__1;
-x_3 = lean_unsigned_to_nat(579u);
+x_3 = lean_unsigned_to_nat(583u);
 x_4 = lean_unsigned_to_nat(24u);
 x_5 = l_Lean_Name_getString_x21___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -22949,7 +22953,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5383_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5388_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -23186,7 +23190,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabLetStarDecl___closed__1);
 res = l___regBuiltin_Lean_Elab_Term_elabLetStarDecl(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5383_(lean_io_mk_world());
+res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_5388_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Lean/Elab/Declaration.c
@ -43,6 +43,7 @@ lean_object* l___regBuiltin_Lean_Elab_Command_expandBuiltinInitialize___closed__
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__1(lean_object*);
 lean_object* lean_array_uget(lean_object*, size_t);
+extern lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessLevels___closed__1;
 lean_object* l_Array_append___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_getDeclarationRange___at_Lean_Elab_Command_elabAxiom___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Modifiers_isProtected(lean_object*);
@ -196,7 +197,6 @@ lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualIndu
 lean_object* l_Lean_Elab_addDeclarationRanges___at_Lean_Elab_Command_elabAxiom___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_docStringExt;
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__2;
-lean_object* l_Lean_Elab_Command_expandMutualElement___closed__1;
 lean_object* l_Lean_Elab_Command_expandMutualPreamble___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_System_IO___hyg_2554____closed__5;
 lean_object* l_Lean_Elab_Command_elabMutual___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -6258,19 +6258,6 @@ return x_54;
 }
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_expandMutualElement___closed__1() {
-_start:
-{
-lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Array_empty___closed__1;
-x_2 = 0;
-x_3 = lean_box(x_2);
-x_4 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_4, 0, x_1);
-lean_ctor_set(x_4, 1, x_3);
-return x_4;
-}
-}
 lean_object* l_Lean_Elab_Command_expandMutualElement(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -6283,7 +6270,7 @@ x_7 = lean_array_get_size(x_6);
 x_8 = lean_usize_of_nat(x_7);
 lean_dec(x_7);
 x_9 = 0;
-x_10 = l_Lean_Elab_Command_expandMutualElement___closed__1;
+x_10 = l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessLevels___closed__1;
 x_11 = l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualElement___spec__1(x_6, x_8, x_9, x_10, x_2, x_3);
 lean_dec(x_6);
 if (lean_obj_tag(x_11) == 0)
@ -8111,8 +8098,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_expandMutualNamespace___cl
 res = l___regBuiltin_Lean_Elab_Command_expandMutualNamespace(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Elab_Command_expandMutualElement___closed__1 = _init_l_Lean_Elab_Command_expandMutualElement___closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_expandMutualElement___closed__1);
 l___regBuiltin_Lean_Elab_Command_expandMutualElement___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_expandMutualElement___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_expandMutualElement___closed__1);
 res = l___regBuiltin_Lean_Elab_Command_expandMutualElement(lean_io_mk_world());
--- a/stage0/stdlib/Lean/Elab/Deriving/Repr.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Repr.c
@ -25,7 +25,6 @@ lean_object* l_Array_allM___at_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___s
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_stringToMessageData(lean_object*);
-lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1;
 lean_object* l_Lean_Elab_Deriving_Repr_mkBodyForStruct___rarg___lambda__2___closed__7;
 extern lean_object* l_Lean_Elab_Deriving_mkContext___closed__2;
 lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -35,6 +34,7 @@ lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* l_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Subarray___hyg_932____closed__4;
 lean_object* l_Lean_throwError___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1;
 lean_object* l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__5;
 lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__4___lambda__1___closed__17;
 lean_object* l_Array_append___rarg(lean_object*, lean_object*);
@ -262,7 +262,6 @@ lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___lambda__1(lean_object*, l
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_12938____closed__13;
 extern lean_object* l_Lean_Parser_Tactic_letrec___closed__3;
 lean_object* l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__3;
-uint8_t l_Lean_isStructureLike(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_Repr_mkBodyForStruct___rarg___lambda__2___closed__2;
 lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__3(lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -282,6 +281,7 @@ lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAl
 lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__4___lambda__1___closed__28;
 lean_object* l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___closed__1;
 lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Deriving_mkInductiveApp___spec__2___rarg(lean_object*, lean_object*, lean_object*);
+uint8_t l_Lean_isStructure(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__2;
 lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__4___lambda__1___closed__5;
 lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -289,7 +289,7 @@ lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_myMacro____x40_Init_Data_Format_Macro___hyg_26____closed__4;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158_(lean_object*);
+lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164_(lean_object*);
 static lean_object* _init_l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__1() {
 _start:
 {
@ -4667,7 +4667,7 @@ lean_inc(x_15);
 x_16 = lean_ctor_get(x_15, 0);
 lean_inc(x_16);
 lean_dec(x_15);
-x_17 = l_Lean_isStructureLike(x_14, x_16);
+x_17 = l_Lean_isStructure(x_14, x_16);
 if (x_17 == 0)
 {
 lean_object* x_18; 
@ -7038,7 +7038,7 @@ lean_dec(x_2);
 return x_8;
 }
 }
-static lean_object* _init_l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1() {
+static lean_object* _init_l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -7046,12 +7046,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler
 return x_1;
 }
 }
-lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__2;
-x_3 = l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1;
+x_3 = l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1;
 x_4 = l_Lean_Elab_registerBuiltinDerivingHandler(x_2, x_3, x_1);
 if (lean_obj_tag(x_4) == 0)
 {
@ -7256,9 +7256,9 @@ l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkReprInstanceCmd
 lean_mark_persistent(l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkReprInstanceCmds___closed__1);
 l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___closed__1 = _init_l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___closed__1();
 lean_mark_persistent(l_Lean_Elab_Deriving_Repr_mkReprInstanceHandler___closed__1);
-l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1 = _init_l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1();
-lean_mark_persistent(l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158____closed__1);
-res = l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3158_(lean_io_mk_world());
+l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1 = _init_l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1();
+lean_mark_persistent(l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164____closed__1);
+res = l_Lean_Elab_Deriving_Repr_initFn____x40_Lean_Elab_Deriving_Repr___hyg_3164_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Elab/Match.c
+++ b/stage0/stdlib/Lean/Elab/Match.c
@ -90,6 +90,7 @@ lean_object* l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec_
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__14;
 lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessLevels___closed__1;
 lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabNoMatch(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__6;
@ -149,7 +150,6 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_isMatchUnit_x3f_match
 extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___closed__7;
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__8;
 lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_CollectPatternVars_processVar___lambda__3___closed__3;
-lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2;
 lean_object* l_Lean_Elab_Term_CollectPatternVars_CtorApp_processCtorApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
@ -1825,22 +1825,9 @@ return x_24;
 static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Array_empty___closed__1;
-x_2 = 0;
-x_3 = lean_box(x_2);
-x_4 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_4, 0, x_1);
-lean_ctor_set(x_4, 1, x_3);
-return x_4;
-}
-}
-static lean_object* _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_unsigned_to_nat(0u);
-x_2 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1;
+x_2 = l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessLevels___closed__1;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -1851,7 +1838,7 @@ lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchTyp
 _start:
 {
 lean_object* x_11; lean_object* x_12; lean_object* x_13; size_t x_14; size_t x_15; lean_object* x_16; lean_object* x_17; 
-x_11 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2;
+x_11 = l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1;
 x_12 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_12, 0, x_2);
 lean_ctor_set(x_12, 1, x_11);
@ -30832,8 +30819,6 @@ l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDi
 lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___spec__1___lambda__2___closed__7);
 l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1();
 lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__1);
-l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2 = _init_l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2();
-lean_mark_persistent(l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabDiscrsWitMatchType___closed__2);
 l_Lean_Elab_Term_isAuxDiscrName___closed__1 = _init_l_Lean_Elab_Term_isAuxDiscrName___closed__1();
 lean_mark_persistent(l_Lean_Elab_Term_isAuxDiscrName___closed__1);
 l_Lean_Elab_Term_isAuxDiscrName___closed__2 = _init_l_Lean_Elab_Term_isAuxDiscrName___closed__2();
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
--- a/stage0/stdlib/Lean/Meta/SynthInstance.c
+++ b/stage0/stdlib/Lean/Meta/SynthInstance.c
--- a/stage0/stdlib/Std/Data/PersistentHashMap.c
+++ b/stage0/stdlib/Std/Data/PersistentHashMap.c
@ -80,7 +80,6 @@ lean_object* l_Std_PersistentHashMap_collectStats___rarg___boxed(lean_object*, l
 lean_object* l_Std_PersistentHashMap_foldlMAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_foldlM(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_findEntryAtAux(lean_object*, lean_object*);
-lean_object* l_Std_PersistentHashMap_isUnaryEntries_match__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_find_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_toList___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_stats___rarg___closed__1;
@ -234,7 +233,6 @@ lean_object* l_Std_PersistentHashMap_instInhabitedPersistentHashMap___rarg___box
 lean_object* l_Array_modifyM___at_Std_PersistentHashMap_insertAux___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_eraseAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_foldl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_PersistentHashMap_isUnaryEntries_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_insert_match__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_eraseAux_match__5(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_eraseAux_match__4(lean_object*, lean_object*, lean_object*);
@ -2331,54 +2329,6 @@ x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_isUnaryEntries_match__1
 return x_4;
 }
 }
-lean_object* l_Std_PersistentHashMap_isUnaryEntries_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-switch (lean_obj_tag(x_1)) {
-case 0:
-{
-lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-lean_dec(x_3);
-lean_dec(x_2);
-x_5 = lean_ctor_get(x_1, 0);
-lean_inc(x_5);
-x_6 = lean_ctor_get(x_1, 1);
-lean_inc(x_6);
-lean_dec(x_1);
-x_7 = lean_apply_2(x_4, x_5, x_6);
-return x_7;
-}
-case 1:
-{
-lean_object* x_8; lean_object* x_9; 
-lean_dec(x_4);
-lean_dec(x_2);
-x_8 = lean_ctor_get(x_1, 0);
-lean_inc(x_8);
-lean_dec(x_1);
-x_9 = lean_apply_1(x_3, x_8);
-return x_9;
-}
-default: 
-{
-lean_object* x_10; lean_object* x_11; 
-lean_dec(x_4);
-lean_dec(x_3);
-x_10 = lean_box(0);
-x_11 = lean_apply_1(x_2, x_10);
-return x_11;
-}
-}
-}
-}
-lean_object* l_Std_PersistentHashMap_isUnaryEntries_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_isUnaryEntries_match__2___rarg), 4, 0);
-return x_4;
-}
-}
 lean_object* l_Std_PersistentHashMap_isUnaryEntries___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {