fix: more pedantic checking of inaccessible patterns (#10796)
This PR changes match compilation to reject some pattern matches that were previously accepted due to inaccessible patterns sometimes treated like accessible ones. Fixes #10794.
This commit is contained in:
Joachim Breitner
GitHub
parent
5800ce17b3
commit
c22100036c
2 changed files with 79 additions and 37 deletions
|
|
@ -287,10 +287,10 @@ where
|
|||
Solve pending alternative constraints. If all constraints can be solved perform assignment
|
||||
`mvarId := alt.rhs`, and return true.
|
||||
-/
|
||||
private partial def solveCnstrs (mvarId : MVarId) (alt : Alt) : StateRefT State MetaM Bool := do
|
||||
private partial def solveCnstrs (mvarId : MVarId) (alt : Alt) : StateRefT State MetaM Unit := do
|
||||
go (reorientCnstrs alt)
|
||||
where
|
||||
go (alt : Alt) : StateRefT State MetaM Bool := do
|
||||
go (alt : Alt) : StateRefT State MetaM Unit := do
|
||||
match (← solveSomeLocalFVarIdCnstr? alt) with
|
||||
| some alt => go alt
|
||||
| none =>
|
||||
|
|
@ -303,10 +303,12 @@ where
|
|||
throwErrorAt alt.ref "Dependent elimination failed: Type mismatch when solving this alternative: it {← mkHasTypeButIsExpectedMsg eType targetType}"
|
||||
mvarId.assign alt.rhs
|
||||
modify fun s => { s with used := s.used.insert alt.idx }
|
||||
return true
|
||||
else
|
||||
trace[Meta.Match.match] "alt has unsolved cnstrs:\n{← alt.toMessageData}"
|
||||
return false
|
||||
let mut msg := m!"Dependent match elimination failed: Could not solve constraints"
|
||||
for (lhs, rhs) in alt.cnstrs do
|
||||
msg := msg ++ m!"\n {lhs} ≋ {rhs}"
|
||||
throwErrorAt alt.ref msg
|
||||
|
||||
/--
|
||||
Try to solve the problem by using the first alternative whose pending constraints can be resolved.
|
||||
|
|
@ -325,8 +327,7 @@ where
|
|||
p.mvarId.admit
|
||||
modify fun s => { s with counterExamples := p.examples :: s.counterExamples }
|
||||
| alt :: _ =>
|
||||
unless (← solveCnstrs p.mvarId alt) do
|
||||
throwErrorAt alt.ref "Dependent match elimination failed: Could not solve constraints"
|
||||
solveCnstrs p.mvarId alt
|
||||
|
||||
private def processAsPattern (p : Problem) : MetaM Problem := withGoalOf p do
|
||||
let x :: _ := p.vars | unreachable!
|
||||
|
|
@ -408,7 +409,9 @@ alternative `cnstrs` field.
|
|||
private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool :=
|
||||
localDecls.any fun d => d.fvarId == fvarId
|
||||
|
||||
private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=
|
||||
private def expandVarIntoCtor? (alt : Alt) (ctorName : Name) : MetaM Alt := do
|
||||
let .var fvarId :: ps := alt.patterns | unreachable!
|
||||
let alt := { alt with patterns := ps}
|
||||
withExistingLocalDecls alt.fvarDecls do
|
||||
trace[Meta.Match.unify] "expandVarIntoCtor? fvarId: {mkFVar fvarId}, ctorName: {ctorName}, alt:\n{← alt.toMessageData}"
|
||||
let expectedType ← inferType (mkFVar fvarId)
|
||||
|
|
@ -426,7 +429,19 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) :
|
|||
cnstrs := (resultType, expectedType) :: cnstrs
|
||||
trace[Meta.Match.unify] "expandVarIntoCtor? {mkFVar fvarId} : {expectedType}, ctor: {ctor}"
|
||||
let ctorFieldPatterns := ctorFieldDecls.toList.map fun decl => Pattern.var decl.fvarId
|
||||
return some { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns, cnstrs }
|
||||
return { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns, cnstrs }
|
||||
|
||||
private def expandInaccessibleIntoVar (alt : Alt) : MetaM Alt := do
|
||||
let .inaccessible e :: ps := alt.patterns | unreachable!
|
||||
withExistingLocalDecls alt.fvarDecls do
|
||||
let type ← inferType e
|
||||
withLocalDeclD `x type fun x => do
|
||||
trace[Meta.Match.unify] "expandInaccessibleIntoVar {x} : {type} := {e}"
|
||||
return { alt with
|
||||
fvarDecls := (← x.fvarId!.getDecl) :: alt.fvarDecls
|
||||
patterns := .var x.fvarId! :: ps
|
||||
cnstrs := (x, e) :: alt.cnstrs
|
||||
}
|
||||
|
||||
private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
|
||||
let xType ← inferType x
|
||||
|
|
@ -449,24 +464,25 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do
|
|||
If it is not a constructor, throw an error.
|
||||
Otherwise, if it is a constructor application of `ctorName`,
|
||||
update the next patterns with the fields of the constructor.
|
||||
Otherwise, return none. -/
|
||||
def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt) := do
|
||||
match alt.patterns with
|
||||
| p@(.inaccessible e) :: ps =>
|
||||
trace[Meta.Match.match] "inaccessible in ctor step {e}"
|
||||
withExistingLocalDecls alt.fvarDecls do
|
||||
-- Try to push inaccessible annotations.
|
||||
let e ← whnfD e
|
||||
match (← constructorApp? e) with
|
||||
| some (ctorVal, ctorArgs) =>
|
||||
if ctorVal.name == ctorName then
|
||||
let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
|
||||
let fields := fields.toList.map .inaccessible
|
||||
return some { alt with patterns := fields ++ ps }
|
||||
else
|
||||
return none
|
||||
| _ => throwErrorAt alt.ref "Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern{indentD p.toMessageData}"
|
||||
| _ => unreachable!
|
||||
Otherwise, move it to contraints, so that we fail unless some later step
|
||||
eliminates this alternative.
|
||||
-/
|
||||
def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM Alt := do
|
||||
let p@(.inaccessible e) :: ps := alt.patterns | unreachable!
|
||||
trace[Meta.Match.match] "inaccessible in ctor step {e}"
|
||||
withExistingLocalDecls alt.fvarDecls do
|
||||
-- Try to push inaccessible annotations.
|
||||
let e ← whnfD e
|
||||
match (← constructorApp? e) with
|
||||
| some (ctorVal, ctorArgs) =>
|
||||
if ctorVal.name == ctorName then
|
||||
let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
|
||||
let fields := fields.toList.map .inaccessible
|
||||
return { alt with patterns := fields ++ ps }
|
||||
else
|
||||
let alt' ← expandInaccessibleIntoVar alt
|
||||
expandVarIntoCtor? alt' ctorName
|
||||
| _ => throwErrorAt alt.ref "Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern{indentD p.toMessageData}"
|
||||
|
||||
private def hasNonTrivialExample (p : Problem) : Bool :=
|
||||
p.examples.any fun | Example.underscore => false | _ => true
|
||||
|
|
@ -527,25 +543,18 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
|
|||
| .inaccessible _ :: _ => true
|
||||
| _ => false
|
||||
let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
|
||||
let newAlts ← newAlts.filterMapM fun alt => do
|
||||
let newAlts ← newAlts.mapM fun alt => do
|
||||
match alt.patterns with
|
||||
| .ctor _ _ _ fields :: ps => return some { alt with patterns := fields ++ ps }
|
||||
| .var fvarId :: ps => expandVarIntoCtor? { alt with patterns := ps } fvarId subgoal.ctorName
|
||||
| .ctor _ _ _ fields :: ps => return { alt with patterns := fields ++ ps }
|
||||
| .var _ :: _ => expandVarIntoCtor? alt subgoal.ctorName
|
||||
| .inaccessible _ :: _ => processInaccessibleAsCtor alt subgoal.ctorName
|
||||
| _ => unreachable!
|
||||
return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
|
||||
|
||||
private def altsAreCtorLike (p : Problem) : MetaM Bool := withGoalOf p do
|
||||
pure (hasCtorPattern p) <&&>
|
||||
p.alts.allM fun alt => do match alt.patterns with
|
||||
| .ctor .. :: _ => return true
|
||||
| .inaccessible e :: _ => isConstructorApp e
|
||||
| _ => return false
|
||||
|
||||
private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
|
||||
let x :: xs := p.vars | unreachable!
|
||||
if let some (ctorVal, xArgs) ← withTransparency .default <| constructorApp'? x then
|
||||
if (← altsAreCtorLike p) then
|
||||
if hasCtorPattern p then
|
||||
let alts ← p.alts.filterMapM fun alt => do
|
||||
match alt.patterns with
|
||||
| .ctor ctorName _ _ fields :: ps =>
|
||||
|
|
@ -554,6 +563,7 @@ private def processNonVariable (p : Problem) : MetaM Problem := withGoalOf p do
|
|||
else
|
||||
return some { alt with patterns := fields ++ ps }
|
||||
| .inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name
|
||||
| .var _ :: _ => expandVarIntoCtor? alt ctorVal.name
|
||||
| _ => unreachable!
|
||||
let xFields := xArgs.extract ctorVal.numParams xArgs.size
|
||||
return { p with alts := alts, vars := xFields.toList ++ xs }
|
||||
|
|
|
|||
32
tests/lean/run/issue10794.lean
Normal file
32
tests/lean/run/issue10794.lean
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
/--
|
||||
error: Dependent match elimination failed: Could not solve constraints
|
||||
true ≋ false
|
||||
-/
|
||||
#guard_msgs in
|
||||
def test1 b := match b with
|
||||
| .(false) => 1
|
||||
| true => 2
|
||||
|
||||
/--
|
||||
error: Dependent match elimination failed: Could not solve constraints
|
||||
true ≋ false
|
||||
-/
|
||||
#guard_msgs in
|
||||
def test2 : (b : Bool) → (h : b = false) → Nat
|
||||
| .(false), .(rfl) => 1
|
||||
| true, _ => 2
|
||||
|
||||
-- works
|
||||
def test3 : (b : Bool) → (h : b = false) → Nat
|
||||
| .(false), rfl => 1
|
||||
|
||||
/--
|
||||
@ +3:4...11
|
||||
error: Redundant alternative: Any expression matching
|
||||
true, x✝
|
||||
will match one of the preceding alternatives
|
||||
-/
|
||||
#guard_msgs (positions := true) in
|
||||
def test4 : (b : Bool) → (h : b = false) → Nat
|
||||
| .(false), rfl => 1
|
||||
| true, _ => 2 -- error here
|
||||
Loading…
Add table
Reference in a new issue