diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 8180644280..11191c3e05 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/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 diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index 0cbe42f570..bfceeec6ca 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/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' diff --git a/tests/lean/run/ctorAutoParams.lean b/tests/lean/run/ctorAutoParams.lean new file mode 100644 index 0000000000..5207e4c089 --- /dev/null +++ b/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