max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: have elabAsElim check inferred motive for type correctness (#4722)

Browse source 
Declarations with `@[elab_as_elim]` could elaborate as type-incorrect
expressions. Reported by Jireh Loreaux [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20revert/near/450522157).

(In principle the elabAsElim routine could revert fvars appearing in the
expected type that depend on the discriminants (if the discriminants are
fvars) to increase the likelihood of type correctness, but that's at the
cost of some complexity to both the elaborator and to the user.)
This commit is contained in:
Kyle Miller 2024-07-17 13:48:03 -07:00 • committed by GitHub
parent f60721bfbd
commit 490d16c80d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 18 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/App.lean
View file

@ -742,7 +742,10 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
let motiveBody ← kabstract motive discr
/- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
unless (← isTypeCorrect motive) do
throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
return motive
/-- If the eliminator is over-applied, we "revert" the extra arguments. -/
def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=

9
tests/lean/elabAsElim.lean
View file

@ -87,3 +87,12 @@ noncomputable def f : Nat → Nat :=
example : ∀ x, x ≥ 0 :=
Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
@[elab_as_elim]
def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
example {n : Type} : {T : n} → T = T := @(Foo.induction n)

5
tests/lean/elabAsElim.lean.expected.out
View file

@ -1,3 +1,8 @@
elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
Nat
elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
fun x => T = T
elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
fun x => T✝ = T✝