feat: ignore {} annotation at constructors

src/Lean/Elab/Inductive.lean

@@ -269,6 +269,16 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
       let binderNames := getArrowBinderNames (← instantiateMVars (← inferType C))
       return replaceArrowBinderNames r binderNames[:bsPrefix.size]
 
+/--
+  Execute `k` with updated binder information for `xs`. Any `x` that is explicit becomes implicit.
+-/
+private def withExplicitToImplicit (xs : Array Expr) (k : TermElabM α) : TermElabM α := do
+  let mut toImplicit := #[]
+  for x in xs do
+    if (← getFVarLocalDecl x).binderInfo.isExplicit then
+      toImplicit := toImplicit.push (x.fvarId!, BinderInfo.implicit)
+  withNewBinderInfos toImplicit k
+
 /-
   Elaborate constructor types.
 
@@ -522,7 +532,7 @@ private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : T
   indTypes.mapM fun indType => do
     let type ← mkForallFVars vars indType.type
     let ctors ← indType.ctors.mapM fun ctor => do
-      let ctorType ← mkForallFVars vars ctor.type
+      let ctorType ← withExplicitToImplicit vars (mkForallFVars vars ctor.type)
       return { ctor with type := ctorType }
     return { indType with type := type, ctors := ctors }
 
@@ -561,24 +571,6 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars :
       return { ctor with type := type }
     return { indType with ctors := ctors }
 
-abbrev Ctor2InferMod := Std.HashMap Name Bool
-
-private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod := Id.run do
-  let mut m := {}
-  for view in views do
-    for ctorView in view.ctors do
-      m := m.insert ctorView.declName ctorView.inferMod
-  return m
-
-private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : List InductiveType :=
-  let ctor2InferMod := mkCtor2InferMod views
-  indTypes.map fun indType =>
-    let ctors := indType.ctors.map fun ctor =>
-      let inferMod := ctor2InferMod.find! ctor.name -- true if `{}` was used
-      let ctorType := ctor.type.inferImplicit numParams !inferMod
-      { ctor with type := ctorType }
-    { indType with ctors := ctors }
-
 private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
   let env ← getEnv
   let hasEq   := env.contains ``Eq
@@ -700,7 +692,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         Term.addLocalVarInfo views[i].declId indFVar
         let r       := rs[i]
         let type  ← mkForallFVars params r.type
-        let ctors ← elabCtors indFVars indFVar params r
+        let ctors ← withExplicitToImplicit params (elabCtors indFVars indFVar params r)
         indTypesArray := indTypesArray.push { name := r.view.declName, type := type, ctors := ctors : InductiveType }
       Term.synthesizeSyntheticMVarsNoPostponing
       let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
@@ -723,7 +715,6 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
         | Except.error msg      => throwError msg
         | Except.ok levelParams => do
           let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
-          let indTypes := applyInferMod views numParams indTypes
           let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
           Term.ensureNoUnassignedMVars decl
           addDecl decl

tests/lean/ctorUnivTooBig.lean.expected.out

@@ -17,20 +17,20 @@ at universe level
 it must be smaller than or equal to the inductive datatype universe level
   u+1
 @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)
-ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'a' has type
-  α
+ctorUnivTooBig.lean:35:2-35:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'as' has type
+  List α
 at universe level
   ?u+1
 it must be smaller than or equal to the inductive datatype universe level
   max (u+1) (v+1)
-ctorUnivTooBig.lean:41:2-41:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'a' has type
-  α
+ctorUnivTooBig.lean:41:2-41:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'as' has type
+  List α
 at universe level
   ?u+1
 it must be smaller than or equal to the inductive datatype universe level
   u+2
-ctorUnivTooBig.lean:47:2-47:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'a' has type
-  α
+ctorUnivTooBig.lean:47:2-47:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'as' has type
+  List α
 at universe level
   ?u+1
 it must be smaller than or equal to the inductive datatype universe level

tests/lean/match2.lean

@@ -10,10 +10,10 @@ structure Node : Type where
 
 def h1 (x : List Node) : Bool :=
   match x with
-  | _ :: Node.mk 0 _ Op.mk :: _  => true
-  | _                            => false
+  | _ :: Node.mk 0 _ (Op.mk _) :: _  => true
+  | _                                => false
 
-def mkNode (n : Nat) : Node := { id₁ := n, id₂ := n, o := Op.mk }
+def mkNode (n : Nat) : Node := { id₁ := n, id₂ := n, o := Op.mk _ }
 
 #eval h1 [mkNode 1, mkNode 0, mkNode 3]
 #eval h1 [mkNode 1, mkNode 1, mkNode 3]
@@ -53,7 +53,7 @@ def h3 {b : Bool} (x : Foo b) : Bool :=
 
 def h4 (x : List Node) : Bool :=
   match x with
-  | _ :: ⟨1, 1, Op.mk⟩ :: _  => true
+  | _ :: ⟨1, 1, Op.mk _⟩ :: _  => true
   | _                          => false
 
 #eval h4 [mkNode 1, mkNode 0, mkNode 3]

tests/lean/run/633.lean

@@ -3,8 +3,8 @@ abbrev semantics (α:Type) := StateM (List Nat) α
 inductive expression : Nat → Type
 | const : (n : Nat) → expression n
 
-def uext {w:Nat} (x: expression w) (o:Nat) : expression w := expression.const
-def eval {n : Nat} (v:expression n) : semantics (expression n) := pure expression.const
+def uext {w:Nat} (x: expression w) (o:Nat) : expression w := expression.const _
+def eval {n : Nat} (v:expression n) : semantics (expression n) := pure (expression.const _)
 def set_overflow {w : Nat} (e : expression w) : semantics Unit := pure ()
 
 structure instruction :=
@@ -13,7 +13,7 @@ structure instruction :=
 
 def definst (mnem:String) (body: expression 8 -> semantics Unit) : instruction :=
 { mnemonic := mnem
-, patterns := ((body expression.const).run []).snd.reverse
+, patterns := ((body (expression.const _)).run []).snd.reverse
 }
 
 def mul : instruction := Id.run <| do -- this is a "pure" do block (as in it is the Id monad)

tests/lean/run/inductive1.lean

@@ -15,11 +15,11 @@ universe u v
 variable (α : Type u)
 
 inductive A (β : Type v)
-| nil {}
+| nil
 | protected cons : α → β → A β → A β
 
 #check @A.cons
-#check A.nil Nat Bool
+#check A.nil (α := Nat) (β := Bool)
 
 mutual
   inductive isEven : Nat → Prop

tests/lean/run/inductive2.lean

@@ -1,17 +1,14 @@
-
-
 mutual
-universe u
-variable (α : Type u)
 
 inductive isEvenList : List α → Prop
-| nil {}  : isEvenList []
+| nil (α)  : isEvenList (α := α) []
 | cons (h : α) {t : List α} : isOddList t → isEvenList (h::t)
 
 inductive isOddList : List α → Prop
 | cons (h : α) {t : List α} : isEvenList t → isOddList (h::t)
 end
-
+set_option pp.explicit true
+#print isEvenList
 #check @isEvenList.nil
 #check @isEvenList.cons
 #check @isOddList.cons

tests/lean/run/matchGenBug.lean

@@ -12,8 +12,8 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a
   induction as with
   | nil          => cases h
   | cons b bs ih => cases h with
-    | head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
-    | tail a b bs h =>
+    | head bs => exact ⟨[], ⟨bs, rfl⟩⟩
+    | tail b bs h =>
       match bs, ih h with
       | _, ⟨s, t, rfl⟩ =>
         exists b::s; exists t