feat: auto bound implicit at constructors

@Kha This commit adds auto bound implicits to constructors.
I was excited until I tried to define the `Bigstep` type again without
`autoBoundImplicitLocal`, and found small typos.
Example, I had
```
  | ifTrue  : eval σ₁ b = true  → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t₁ + 1)
```
where `t₁` should be `t`, but the declaration was accepted. I am
wondering whether Isabelle performs some kind of sanity checking,
and/or enforces rules such as: auto-bound implicits may only be
introduced by hypotheses.
Note that this is not an issue for definitions, because the body of
the definition will probably not type check when we have this kind of
typo in the header.
Anyway, I am putting the experiment in this branch for now.
That being said, the `Bigstep` declaration is way nicer with
`autoBoundImplicitLocal`s.

Another option is to add a new option `ctorAutoBoundImplicitLocal`
that is false by default, and activates auto implicit locals for
constructors when set to true.

src/Lean/Elab/Inductive.lean

@@ -184,7 +184,7 @@ private partial def withInductiveLocalDecls {α} (rs : Array ElabHeaderResult) (
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
   let indFVarType ← inferType indFVar
   forallTelescopeReducing indFVarType fun xs _ =>
-    pure $ xs.size > numParams
+    return xs.size > numParams
 
 /-
   Elaborate constructor types.
@@ -193,36 +193,38 @@ private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Boo
   we do not check for:
   - Positivity (it is a rare failure, and the kernel already checks for it).
   - 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
+private def elabCtors (indFVar : Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) := withRef r.view.ref do
   let indFamily ← isInductiveFamily params.size indFVar
-  r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getArgs fun ctorParams =>
-    withRef ctorView.ref do
-    let type ← match ctorView.type? with
-      | none          =>
-        if indFamily then
-          throwError "constructor resulting type must be specified in inductive family declaration"
-        pure (mkAppN indFVar params)
-      | some ctorType =>
-        /- Remark: we don't use `Term.elabType` because we produce a better error message when
-           `ctorType` doesn't elaborate into a type. -/
-        let type ← Term.withSynthesize (mayPostpone := true) <| Term.elabTerm ctorType none
-        let type ← instantiateMVars type
-        let resultingType ← getResultingType type
-        unless resultingType.getAppFn == indFVar do
-          throwError! "unexpected constructor resulting type{indentExpr resultingType}"
-        unless (← isType resultingType) do
-          throwError! "unexpected constructor resulting type, type expected{indentExpr resultingType}"
-        let args := resultingType.getAppArgs
-        for i in [:params.size] do
-          let param := params[i]
-          let arg   := args[i]
-          unless (← isDefEq param arg) do
-            throwError! "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
-        pure type
-    let type ← mkForallFVars ctorParams type
-    let type ← mkForallFVars params type
-    pure { name := ctorView.declName, type := type }
+  r.view.ctors.toList.mapM fun ctorView =>
+    Term.withAutoBoundImplicitLocal <| Term.elabBinders (catchAutoBoundImplicit := true) ctorView.binders.getArgs fun ctorParams =>
+      withRef ctorView.ref do
+        let rec elabCtorType (k : Expr → TermElabM Constructor) : TermElabM Constructor := do
+          match ctorView.type? with
+          | none          =>
+            if indFamily then
+              throwError "constructor resulting type must be specified in inductive family declaration"
+            k <| mkAppN indFVar params
+          | some ctorType =>
+            Term.elabTypeWithAutoBoundImplicit ctorType fun type => do
+              Term.synthesizeSyntheticMVars (mayPostpone := true)
+              let type ← instantiateMVars type
+              let resultingType ← getResultingType type
+              unless resultingType.getAppFn == indFVar do
+                throwError! "unexpected constructor resulting type{indentExpr resultingType}"
+              unless (← isType resultingType) do
+                throwError! "unexpected constructor resulting type, type expected{indentExpr resultingType}"
+              let args := resultingType.getAppArgs
+              for i in [:params.size] do
+                let param := params[i]
+                let arg   := args[i]
+                unless (← isDefEq param arg) do
+                  throwError! "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
+              k type
+        elabCtorType fun type => do
+          let ctorParams ← Term.addAutoBoundImplicits ctorParams
+          let type ← mkForallFVars ctorParams type
+          let type ← mkForallFVars params type
+          return { name := ctorView.declName, type := type }
 
 /- Convert universe metavariables occurring in the `indTypes` into new parameters.
    Remark: if the resulting inductive datatype has universe metavariables, we will fix it later using

tests/lean/inductive1.lean.expected.out

@@ -22,8 +22,9 @@ inductive1.lean:82:0-82:29: error: invalid use of attributes in inductive declar
 inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype
 inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
 inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration
-inductive1.lean:105:0-105:9: error: unexpected constructor resulting type, type expected
-  T1
+inductive1.lean:105:7-105:9: error: type expected
+failed to synthesize instance
+  CoeSort (Nat → Type) ?m
 inductive1.lean:108:0-108:10: error: unexpected constructor resulting type
   Nat
 inductive1.lean:118:7-118:11: error: unknown identifier 'cons'

tests/lean/run/ctorAutoParams.lean

@@ -0,0 +1,36 @@
+structure State -- TODO
+
+structure Expr -- TODO
+
+def eval : State → Expr → Bool :=
+  fun _ _ => true
+
+inductive Command where
+  | skip
+  | cond  : Expr → Command → Command → Command
+  | while : Expr → Command → Command
+  | seq   : Command → Command → Command
+
+open Command
+
+infix:10 ";;" => Command.seq
+
+inductive Bigstep : Command × State → State → Nat → Prop where
+  | skip    : Bigstep (skip, σ) σ 1
+  | seq     : Bigstep (c₁, σ₁) σ₂ t₁ → Bigstep (c₂, σ₂) σ₃ t₂ → Bigstep (c₁ ;; c₂, σ₁) σ₃ (t₁ + t₂ + 1)
+  | ifTrue  : eval σ₁ b = true  → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t + 1)
+  | ifFalse : eval σ₁ b = false → Bigstep (c₂, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t + 1)
+
+#check @Bigstep.seq
+
+namespace WithoutAutoImplicit
+
+set_option autoBoundImplicitLocal false
+
+inductive Bigstep : Command × State → State → Nat → Prop where
+  | skip    {σ} : Bigstep (skip, σ) σ 1
+  | seq     {c₁ c₂ σ₁ σ₂ σ₃ t₁ t₂} : Bigstep (c₁, σ₁) σ₂ t₁ → Bigstep (c₂, σ₂) σ₃ t₂ → Bigstep (c₁ ;; c₂, σ₁) σ₃ (t₁ + t₂ + 1)
+  | ifTrue  {b c₁ c₂ σ₁ σ₂ t} : eval σ₁ b = true  → Bigstep (c₁, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t + 1)
+  | ifFalse {b c₁ c₂ σ₁ σ₂ t} : eval σ₁ b = false → Bigstep (c₂, σ₁) σ₂ t → Bigstep (cond b c₁ c₂, σ₁) σ₂ (t + 1)
+
+end WithoutAutoImplicit