fix: reject unsound unification hints #8988
Conversation
|
changelog-language |
|
This doesn't actually fix #8982, as the following example is accepted but still causes a crash. abbrev const (_ : Type) : Unit := ()
unif_hint (x y : Type) where const x ≟ const y ⊢ x ≟ y
inductive W {α : Type} (β : α → Type)
| mk a (w : β a → W β)However, the change does make it harder to write unsound unification hints. |
|
Surely these should be free vars and not mvars |
|
Could you elaborate what you had in mind? One approach to ensure that unification hints are sound is to require that all the premises are valid assignments of the form |
|
I mean private partial def validateHint (hint : UnificationHint) : MetaM Unit := do
hint.constraints.forM fun c => do
unless c.lhs.isMVar || c.rhs.isMVar then
throwError "invalid unification hint, neither constraint left-hand-side{indentExpr c.lhs}\nor right-hand-side {indentExpr c.rhs}\nis a variable"
unless (← isDefEq c.lhs c.rhs) do
throwError "invalid unification hint, failed to unify constraint left-hand-side{indentExpr c.lhs}\nwith right-hand-side{indentExpr c.rhs}"
unless (← withNewMCtxDepth <| isDefEq hint.pattern.lhs hint.pattern.rhs) do
throwError "invalid unification hint, failed to unify pattern left-hand-side{indentExpr hint.pattern.lhs}\nwith right-hand-side{indentExpr hint.pattern.rhs}"so defeq can't assign anything. |
|
Yes I had the same idea that all of the constraints should look like assignments to mvars. I checked all the unification hints in the tests and in mathlib and they all already fit this pattern, so adding this check shouldn't break the existing uses. The check you wrote is not enough since you can write: abbrev const (_ : Type) : Unit := ()
unif_hint (x y : Type) (u : Unit) where
u ≟ const x
u ≟ const y
⊢ x ≟ y
inductive W {α : Type} (β : α → Type)
| mk a (w : β a → W β)I believe checking that the mvar is unassigned should be enough to avoid this, and I'll update the PR with a new implementation if it works. |
|
Meta-variables are a bit weird to work with (see your own zulip post) so I'd try free variables: private partial def decodeUnificationHintAndSubstitute (e : Expr) : Except MessageData (Expr × Expr) := do
match e with
| Expr.forallE _ d b _ => do
if b.hasLooseBVars then
throw m!"invalid unification hint constraint, unexpected dependency{indentExpr e}"
let some (_, lhs, rhs) := d.eq? |
throw m!"invalid unification hint constraint, unexpected term{indentExpr e}"
if lhs.isFVar then
if rhs.hasAnyFVar (· == lhs.fvarId!) then
throw m!"invalid unification hint, cyclic constraint{indentD m!"{lhs} =?= {rhs}"}"
decodeUnificationHintAndSubstitute (b.replaceFVar lhs rhs)
else if rhs.isFVar then
if lhs.hasAnyFVar (· == rhs.fvarId!) then
throw m!"invalid unification hint, cyclic constraint{indentD m!"{lhs} =?= {rhs}"}"
decodeUnificationHintAndSubstitute (b.replaceFVar rhs lhs)
else
throw m!"invalid unification hint, constraint{indentD m!"{lhs} =?= {rhs}"}\ndoes not contain a variable on either side"
| _ => do
match e.eq? with
| some (_, lhs, rhs) => return (lhs, rhs)
| none => throw m!"invalid unification hint conclusion, unexpected term{indentExpr e}"
def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit := do
let info ← getConstInfo declName
match info.value? with
| none => throwError "invalid unification hint, it must be a definition"
| some val =>
lambdaTelescope val fun vars body => do
match decodeUnificationHintAndSubstitute body with
| Except.error msg => throwError msg
| Except.ok (lhs, rhs) =>
unless ← isDefEq lhs rhs do
throwError "invalid unification hint, failed to unify pattern left-hand-side\
{indentExpr lhs}\n\
with right-hand-side\
{indentExpr rhs}"
let mvars ← vars.mapM (fun v => do mkFreshExprMVar (← inferType v))
let keys ← withConfigWithKey config <| DiscrTree.mkPath (lhs.replaceFVars vars mvars)
unificationHintExtension.add { keys := keys, val := declName } kindEdit: Your example then fails with: |
This PR validates the soundness of unification hints by requiring all the premises to be variable assignments and checking that the conclusion follows from the assignments.
Closes #8982