From c22100036c4c2dfb27ea752da31e619fe5515a4d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Oct 2025 19:02:54 +0200 Subject: [PATCH] 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. --- src/Lean/Meta/Match/Match.lean | 84 +++++++++++++++++++--------------- tests/lean/run/issue10794.lean | 32 +++++++++++++ 2 files changed, 79 insertions(+), 37 deletions(-) create mode 100644 tests/lean/run/issue10794.lean diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 99dc1a7eb0..e8fc20b5dc 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -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 } diff --git a/tests/lean/run/issue10794.lean b/tests/lean/run/issue10794.lean new file mode 100644 index 0000000000..91692f022e --- /dev/null +++ b/tests/lean/run/issue10794.lean @@ -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