fix: mutual inductives with instance parameters (#4342)

closes #4310

src/Lean/Elab/DeclUtil.lean

@@ -9,19 +9,25 @@ import Lean.Meta.Check
 
 namespace Lean.Meta
 
-def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α
+def forallTelescopeCompatibleAux (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α
   | 0, type₁, type₂, xs   => k xs type₁ type₂
   | i+1, type₁, type₂, xs => do
     let type₁ ← whnf type₁
     let type₂ ← whnf type₂
     match type₁, type₂ with
-    | Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ =>
-      unless n₁ == n₂ do
-        throwError "parameter name mismatch '{n₁}', expected '{n₂}'"
-      unless (← isDefEq d₁ d₂) do
-        throwError "parameter '{n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}"
+    | .forallE n₁ d₁ b₁ c₁, .forallE n₂ d₂ b₂ c₂ =>
+      -- Remark: we use `mkIdent` to ensure macroscopes do not leak into error messages
       unless c₁ == c₂ do
-        throwError "binder annotation mismatch at parameter '{n₁}'"
+        throwError "binder annotation mismatch at parameter '{mkIdent n₁}'"
+      /-
+      Remark: recall that users may suppress parameter names for instance implicit arguments.
+      A fresh name (with macro scopes) is generated in this case. Thus, we allow the names
+      to be different in this case. See issue #4310.
+      -/
+      unless n₁ == n₂ || (c₁.isInstImplicit && n₁.hasMacroScopes && n₂.hasMacroScopes) do
+        throwError "parameter name mismatch '{mkIdent n₁}', expected '{mkIdent n₂}'"
+      unless (← isDefEq d₁ d₂) do
+        throwError "parameter '{mkIdent n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}"
       withLocalDecl n₁ c₁ d₁ fun x =>
         let type₁ := b₁.instantiate1 x
         let type₂ := b₂.instantiate1 x
@@ -30,7 +36,7 @@ def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → Meta
 
 /-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and
     then execute `k` with the parameters and remaining types. -/
-def forallTelescopeCompatible {α m} [Monad m] [MonadControlT MetaM m] (type₁ type₂ : Expr) (numParams : Nat) (k : Array Expr → Expr → Expr → m α) : m α :=
+def forallTelescopeCompatible [Monad m] [MonadControlT MetaM m] (type₁ type₂ : Expr) (numParams : Nat) (k : Array Expr → Expr → Expr → m α) : m α :=
   controlAt MetaM fun runInBase =>
     forallTelescopeCompatibleAux (fun xs type₁ type₂ => runInBase $ k xs type₁ type₂) numParams type₁ type₂ #[]
 

src/Lean/Elab/Level.lean

@@ -78,7 +78,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
       if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName (relaxedAutoImplicit.get (← read).options) then
         modify fun s => { s with levelNames := paramName :: s.levelNames }
       else
-        throwError "unknown universe level '{paramName}'"
+        throwError "unknown universe level '{mkIdent paramName}'"
     return mkLevelParam paramName
   else if kind == `Lean.Parser.Level.addLit then
     let lvl ← elabLevel (stx.getArg 0)

tests/lean/run/4310.lean

@@ -0,0 +1,41 @@
+class Foo
+
+mutual
+  inductive Bar [Foo] where
+  inductive Baz [Foo] where -- Should not fail
+end
+
+/--
+error: invalid mutually inductive types, parameter name mismatch 'x', expected 'inst✝'
+-/
+#guard_msgs in
+mutual
+  inductive Bar1 [Foo] where
+  inductive Baz1 [x : Foo] where -- Should fail
+end
+
+
+/--
+error: invalid mutually inductive types, parameter name mismatch 'β', expected 'α'
+-/
+#guard_msgs in
+mutual
+  inductive Boo (α : Type u) where
+  inductive Bla (β : Type u) where
+end
+
+macro "gen_mutual" : command =>
+  `(mutual
+    inductive Boo (α : Type u) where
+    inductive Bla (β : Type u) where
+   end)
+
+/--
+error: unknown universe level 'u✝'
+---
+error: unknown universe level 'u✝'
+---
+error: invalid mutually inductive types, parameter name mismatch 'β✝', expected 'α✝'
+-/
+#guard_msgs in
+gen_mutual