feat: new inductive command syntax

cc @Kha

src/Lean/Elab/Inductive.lean

@@ -171,7 +171,6 @@ private partial def withInductiveLocalDeclsAux {α} (namesAndTypes : Array (Name
 | i, indFVars =>
   if h : i < namesAndTypes.size then do
     let (id, type) := namesAndTypes.get ⟨i, h⟩;
-    type ← instantiateForall type params;
     withLocalDeclD id type fun indFVar => withInductiveLocalDeclsAux (i+1) (indFVars.push indFVar)
   else
     x params indFVars
@@ -191,10 +190,10 @@ let params := r0.params;
 withLCtx r0.lctx r0.localInsts $ withRef r0.view.ref $
   withInductiveLocalDeclsAux namesAndTypes params x 0 #[]
 
-private def isInductiveFamily (indFVar : Expr) : TermElabM Bool := do
+private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
 indFVarType ← inferType indFVar;
-indFVarType ← whnf indFVarType;
-pure !indFVarType.isSort
+forallTelescopeReducing indFVarType fun xs _ =>
+  pure $ xs.size > numParams
 
 /-
   Elaborate constructor types.
@@ -205,14 +204,14 @@ pure !indFVarType.isSort
   - Universe constraints (the kernel checks for it). -/
 private def elabCtors (indFVar : Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) :=
 withRef r.view.ref do
-indFamily ← isInductiveFamily indFVar;
+indFamily ← isInductiveFamily params.size indFVar;
 r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getArgs fun ctorParams =>
   withRef ctorView.ref $ do
   type ← match ctorView.type? with
     | none          => do
       when indFamily $
         throwError "constructor resulting type must be specified in inductive family declaration";
-      pure indFVar
+      pure (mkAppN indFVar params)
     | some ctorType => do {
       type ← Term.elabTerm ctorType none;
       resultingType ← getResultingType type;
@@ -328,7 +327,7 @@ pure $ indTypes.map fun indType =>
 
 private def traceIndTypes (indTypes : List InductiveType) : TermElabM Unit :=
 indTypes.forM fun indType =>
-  indType.ctors.forM fun ctor => _root_.dbgTrace ("  >> " ++ toString ctor.name ++ " : " ++ toString ctor.type) fun _ => pure ()
+  indType.ctors.forM fun ctor => IO.println ("  >> " ++ toString ctor.name ++ " : " ++ toString ctor.type)
 
 private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
 used ← indTypes.foldlM
@@ -370,17 +369,20 @@ views.size.fold
     m.insert indFVar (mkConst view.declName levelParams))
   {}
 
-private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) (numParams : Nat) (indTypes : List InductiveType)
-    : TermElabM (List InductiveType) :=
-withRef (views.get! 0).ref $
+/- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration,
+   and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/
+private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name)
+    (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
 let indFVar2Const := mkIndFVar2Const views indFVars levelNames;
 indTypes.mapM fun indType => do
   ctors ← indType.ctors.mapM fun ctor => do {
-    type ← forallBoundedTelescope ctor.type numParams fun params type => do {
-      let type := type.replace fun e => if !e.isFVar then none else
-        match indFVar2Const.find? e with
-        | some c => some $ mkAppN c params
-        | none   => none;
+     type ← forallBoundedTelescope ctor.type numParams fun params type => do {
+      let type := type.replace fun e =>
+        if !e.isFVar then
+          none
+        else match indFVar2Const.find? e with
+          | none   => none
+          | some c => mkAppN c (params.extract 0 numVars);
       mkForallFVars params type
     };
     pure { ctor with type := type }
@@ -451,7 +453,8 @@ withRef view0.ref $ Term.withLevelNames allUserLevelNames do
     u ← getResultingUniverse indTypes;
     inferLevel ← shouldInferResultUniverse u;
     withUsed vars indTypes $ fun vars => do
-      let numParams := vars.size + numExplicitParams;
+      let numVars   := vars.size;
+      let numParams := numVars + numExplicitParams;
       indTypes ← updateParams vars indTypes;
       indTypes ← levelMVarToParam indTypes;
       indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else pure indTypes;
@@ -459,7 +462,7 @@ withRef view0.ref $ Term.withLevelNames allUserLevelNames do
       match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
       | Except.error msg      => throwError msg
       | Except.ok levelParams => do
-        indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numParams indTypes;
+        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;

tests/lean/inductive1.lean

@@ -112,7 +112,7 @@ inductive T1 : Nat → Type
 
 inductive A (α : Type u) (β : Type v)
 | nil {}
-| protected cons : α → β → A → A
+| protected cons : α → β → A α β → A α β
 
 open A
 #check cons -- unknown `cons`, it is protected

tests/lean/inductive1.lean.expected.out

@@ -27,4 +27,4 @@ inductive1.lean:105:0: error: unexpected constructor resulting type, type expect
 inductive1.lean:108:0: error: unexpected constructor resulting type
   Nat
 inductive1.lean:118:7: error: unknown identifier 'cons'
-(sorryAx ?m.134) : ?m.134
+(sorryAx ?m.139) : ?m.139

tests/lean/match1.lean

@@ -36,7 +36,7 @@ match x with
 #print "---- inv"
 
 inductive Image {α β : Type} (f : α → β) : β → Type
-| mk (a : α) : Image (f a)
+| mk (a : α) : Image f (f a)
 
 def mkImage {α β : Type} (f : α → β) (a : α) : Image f (f a) :=
 Image.mk a

tests/lean/mutualWithNamespaceMacro.lean

@@ -4,22 +4,22 @@ mutual
 
 inductive Foo.Lst (α : Type)
 | nil   : Lst
-| cons  : Tree → Lst → Lst
+| cons  : Tree α → Lst α → Lst α
 
 inductive Boo.Tree (α : Type) -- conflicting namespace
-| leaf : Tree
-| node : Lst → Tree
+| leaf : Tree α
+| node : Lst α → Tree α
 
 end
 
 mutual
 
 inductive Foo.Lst (α : Type)
-| nil   : Lst
-| cons  : Tree → Lst → Lst
+| nil   : Lst α
+| cons  : Tree α → Lst α → Lst α
 
 inductive Foo.Tree (α : Type)
-| leaf : Tree
-| node : Lst → Tree
+| leaf : Tree α
+| node : Lst α → Tree α
 
 end

tests/lean/run/inductive1.lean

@@ -2,14 +2,14 @@ new_frontend
 
 inductive L1.{u} (α : Type u)
 | nil
-| cons : α → L1 → L1
+| cons : α → L1 α → L1 α
 
 #check L1
 #check @L1.cons
 
 inductive L2.{u} (α : Type u)
 | nil
-| cons (head : α) (tail : L2)
+| cons (head : α) (tail : L2 α)
 
 #check @L2.cons
 
@@ -18,7 +18,7 @@ variable (α : Type u)
 
 inductive A (β : Type v)
 | nil {}
-| protected cons : α → β → A → A
+| protected cons : α → β → A β → A β
 
 #check @A.cons
 #check A.nil Nat Bool
@@ -37,8 +37,8 @@ end
 #check @isEven.rec
 
 inductive V (α : Type _) : Nat → Type _
-| nil  : V 0
-| cons {n : Nat} : α → V n → V (n+1)
+| nil  : V α 0
+| cons {n : Nat} : α → V α n → V α (n+1)
 
 #check @V.nil
 #check @V.cons
@@ -65,3 +65,9 @@ inductive T1
 | mk : β → β → T1
 
 #check @T1.mk
+
+
+inductive MyEq {α : Type} (a : α) : α → Prop
+| refl : MyEq a a
+
+#check @MyEq.refl