1437033e69
Type mismatch errors have a nice feature where expressions are annotated
with `pp.explicit` to expose differences via `isDefEq` checking.
However, this procedure has side effects since `isDefEq` may assign
metavariables. This PR wraps the procedure with `withoutModifyingState`
to prevent assignments from escaping.
Assignments can lead to confusing behavior. For example, in the
following a higher-order unification fails, but the difference-finding
procedure unifies metavariables in a naive way, producing a baffling
error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
f (g n) = n := hfg n
example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
with_reducible refine test n2 ?_
/-
type mismatch
test n2 ?m.648
has type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
but is expected to have type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
-/
```
With the change, it now says `has type ?m.153 (?m.154 n2) = n2`.
Note: this uses `withoutModifyingState` instead of `withNewMCtxDepth`
because we want to know something about where `isDefEq` failed — we are
trying to simulate a very basic version of `isDefEq` for function
applications, and we want the state at the point of failure to know
which argument is "at fault".
82 lines
5.4 KiB
Text
82 lines
5.4 KiB
Text
[Elab.info] • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
|
||
• [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩
|
||
• option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
|
||
1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
|
||
context:
|
||
α✝ β : Type
|
||
x : Fam2 α✝ β
|
||
α : Type
|
||
a : α
|
||
⊢ α
|
||
[Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
|
||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
|
||
• α : Type @ ⟨7, 13⟩-⟨7, 14⟩
|
||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||
• Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
|
||
• [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
|
||
• Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
|
||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||
• α : Type @ ⟨7, 26⟩-⟨7, 27⟩
|
||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||
• β : Type @ ⟨7, 28⟩-⟨7, 29⟩
|
||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
|
||
• β : Type @ ⟨7, 33⟩-⟨7, 34⟩
|
||
• _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
|
||
• a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
|
||
• x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
|
||
• match α, β, x, a with
|
||
| α_1, .(α_1), Fam2.any, a => ?m x α_1 a
|
||
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ MutualDef.body
|
||
• match α, β, x, a with
|
||
| α_1, .(α_1), Fam2.any, a => ?m x α_1 a
|
||
| .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
|
||
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
|
||
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• FVarAlias a: _uniq.632 -> _uniq.312
|
||
• FVarAlias α: _uniq.631 -> _uniq.310
|
||
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
|
||
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
|
||
• [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
|
||
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
|
||
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
|
||
• FVarAlias a: _uniq.663 -> _uniq.312
|
||
• FVarAlias n: _uniq.662 -> _uniq.310
|
||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
|
||
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
|
||
• @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
|
||
[Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
|