fix: ensure explicit pattern variables provided by the uses are indee…

…d pattern variables

src/Lean/Elab/Match.lean

@@ -620,6 +620,10 @@ def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType :
   let explicitPatternVars := patternVarDecls.map fun decl => decl.fvarId
   let (ps, s) ← ps.mapM normalize |>.run { explicitPatternVars } |>.run {}
   let patternVars ← topSort s.patternVars
+  for explicit in explicitPatternVars do
+    unless patternVars.any (· == mkFVar explicit) do
+      withInPattern do
+        throwError "invalid patterns, `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
   let packed ← mkLambdaFVars patternVars (← packMatchTypePatterns matchType ps) (binderInfoForMVars := BinderInfo.default)
   let lctx := explicitPatternVars.foldl (init := (← getLCtx)) fun lctx d => lctx.erase d
   withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do

tests/lean/invalidPatternIssue.lean

@@ -0,0 +1,13 @@
+structure Pos where
+  protected succ ::
+  protected pred : Nat
+
+protected def Pos.add : Pos → Pos → Pos
+| Pos.succ x, Pos.succ y => Pos.succ (x + y).succ
+instance : Add Pos := ⟨Pos.add⟩
+
+instance (x : Nat) : OfNat Pos x.succ := ⟨Pos.succ x⟩
+
+def f : Pos → Pos
+| 1 => 1
+| x+1 => f x + x + 1

tests/lean/invalidPatternIssue.lean.expected.out

@@ -0,0 +1,2 @@
+invalidPatternIssue.lean:13:0-13:20: error: invalid patterns, `x` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
+  { pred := Nat.succ .(x.1) }