fix: missing case at Match.lean

src/Lean/Meta/Match/Match.lean

@@ -372,7 +372,16 @@ private def processNonVariable (p : Problem) : MetaM Problem :=
         | _       => unreachable!
       let xFields := xArgs.extract ctorVal.nparams xArgs.size
       pure { p with alts := alts, vars := xFields.toList ++ xs }
-    | none => throwError! "failed to compile pattern matching, constructor expected{indentExpr x}"
+    | none =>
+      let alts ← p.alts.filterMapM fun alt => match alt.patterns with
+        | Pattern.inaccessible e :: ps => do
+          if (← isDefEq x e) then
+            pure $ some { alt with patterns := ps }
+          else
+            pure none
+        | p :: _ => throwError! "failed to compile pattern matching, unexpected pattern{indentD p.toMessageData}\ndiscriminant{indentExpr x}"
+        | _      => unreachable!
+      pure { p with alts := alts, vars := xs }
 
 private def collectValues (p : Problem) : Array Expr :=
   p.alts.foldl (init := #[]) fun values alt =>

tests/lean/run/Dorais1.lean

@@ -0,0 +1,29 @@
+inductive Tree (α : Type _) : Type _
+| leaf : α → Tree α
+| branch : Tree α → Tree α → Tree α
+
+inductive Path {α : Type _} : Tree α → Type _
+| term (x : α) : Path (Tree.leaf x)
+| left (tl tr : Tree α) : Path tl → Path (Tree.branch tl tr)
+| right (tl tr : Tree α) : Path tr → Path (Tree.branch  tl tr)
+
+section map
+variables {α : Type _} {β : Type _} (f : α → β)
+
+protected def Tree.map : Tree α → Tree β
+| Tree.leaf x => Tree.leaf (f x)
+| Tree.branch tl tr => Tree.branch (Tree.map tl) (Tree.map tr)
+
+protected def Path.map : {t : Tree α} → Path t → Path (t.map f)
+| Tree.leaf _, Path.term x => Path.term (f x)
+| Tree.branch _ _, Path.left tl tr p => Path.left (tl.map f) (tr.map f) (Path.map p)
+| Tree.branch _ _, Path.right tl tr p => Path.right (tl.map f) (tr.map f) (Path.map p)
+
+protected def Path.unmap : {t : Tree α} → Path (t.map f) → Path t
+| Tree.leaf x,   Path.term _   => Path.term x
+| Tree.branch tl tr, Path.left _ _ p => Path.left tl tr (Path.unmap p)
+| Tree.branch tl tr, Path.right _ _ p => Path.right tl tr (Path.unmap p)
+
+#print Path.unmap
+
+end map