diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index 0b24d101dc64..3fc808c55a46 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -195,59 +195,6 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
 def isLocalDecl (fvarId : FVarId) (alt : Alt) : Bool :=
    alt.fvarDecls.any fun d => d.fvarId == fvarId
 
-/--
-  Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`.
-  This extra check is necessary when performing dependent elimination and inaccessible terms have been used.
-  For example, consider the following code fragment:
-
-```
-inductive Vec (α : Type u) : Nat → Type u where
-  | nil : Vec α 0
-  | cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
-
-inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop where
-  | nil   : VecPred P Vec.nil
-  | cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
-
-theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-  | _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
-```
-Recall that `_` in a pattern can be elaborated into pattern variable or an inaccessible term.
-The elaborator uses an inaccessible term when typing constraints restrict its value.
-Thus, in the example above, the `_` at `Vec.cons head _` becomes the inaccessible pattern `.(Vec.nil)`
-because the type ascription `(w : VecPred P Vec.nil)` propagates typing constraints that restrict its value to be `Vec.nil`.
-After elaboration the alternative becomes:
-```
-  | .(0), @Vec.cons .(α) .(0) head .(Vec.nil), @VecPred.cons .(α) .(P) .(0) .(head) .(Vec.nil) h w => ⟨head, h⟩
-```
-where
-```
-(head : α), (h: P head), (w : VecPred P Vec.nil)
-```
-Then, when we process this alternative in this module, the following check will detect that
-`w` has type `VecPred P Vec.nil`, when it is supposed to have type `VecPred P tail`.
-Note that if we had written
-```
-theorem ex {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-  | _, Vec.cons head Vec.nil, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩
-```
-we would get the easier to digest error message
-```
-missing cases:
-_, (Vec.cons _ _ (Vec.cons _ _ _)), _
-```
--/
-def checkAndReplaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : MetaM Alt := do
-  match alt.fvarDecls.find? fun (fvarDecl : LocalDecl) => fvarDecl.fvarId == fvarId with
-  | none          => throwErrorAt alt.ref "Unknown free pattern variable"
-  | some fvarDecl => do
-    let vType ← inferType v
-    unless (← isDefEqGuarded fvarDecl.type vType) do
-      withExistingLocalDecls alt.fvarDecls do
-        let (expectedType, givenType) ← addPPExplicitToExposeDiff vType fvarDecl.type
-        throwErrorAt alt.ref "Type mismatch during dependent match-elimination at pattern variable `{mkFVar fvarDecl.fvarId}` with type{indentExpr givenType}\nExpected type{indentExpr expectedType}"
-    return replaceFVarId fvarId v alt
-
 end Alt
 
 inductive Example where
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 3ae769c2b893..118c8b56b3d7 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -159,13 +159,32 @@ private def isVariableTransition (p : Problem) : Bool :=
     | .var _ :: _          => true
     | _                    => false
 
-private def isConstructorTransition (p : Problem) : Bool :=
-  (hasCtorPattern p || p.alts.isEmpty)
-  && p.alts.all fun alt => match alt.patterns with
-     | .ctor .. :: _        => true
-     | .var _ :: _          => true
-     | .inaccessible _ :: _ => true
-     | _                    => false
+private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
+  let xType ← inferType x
+  let xType ← whnfD xType
+  match xType.getAppFn with
+  | Expr.const constName _ =>
+    let cinfo ← getConstInfo constName
+    match cinfo with
+    | ConstantInfo.inductInfo val => return some val
+    | _ => return none
+  | _ => return none
+
+def isCurrVarInductive (p : Problem) : MetaM Bool := do
+  match p.vars with
+  | []   => return false
+  | x::_ => withGoalOf p do
+    let val? ← getInductiveVal? x
+    return val?.isSome
+
+private def isConstructorTransition (p : Problem) : MetaM Bool := do
+  return (← isCurrVarInductive p)
+    && (hasCtorPattern p || p.alts.isEmpty)
+    && p.alts.all fun alt => match alt.patterns with
+      | .ctor .. :: _        => true
+      | .var _ :: _          => true
+      | .inaccessible _ :: _ => true
+      | _                    => false
 
 private def isValueTransition (p : Problem) : Bool :=
   hasVarPattern p && hasValPattern p
@@ -204,8 +223,7 @@ private def hasCtorOrInaccessible (p : Problem) : Bool :=
     | _                    => false
 
 private def isNatValueTransition (p : Problem) : MetaM Bool := do
-  unless (← hasNatValPattern p) do return false
-  return hasCtorOrInaccessible p
+  return (← hasNatValPattern p) && hasCtorOrInaccessible p
 
 /--
 Predicate for testing whether we need to expand `Int` value patterns into constructors.
@@ -249,6 +267,10 @@ private def reorientCnstrs (alt : Alt) : Alt :=
 /--
 Remove constraints of the form `lhs ≋ rhs` where `lhs` and `rhs` are definitionally equal,
 or `lhs` is a free variable.
+
+Dropping unsolved constraints where `lhs` is a free variable seems unsound, but simply leads to later
+errors about the type of the alternative not matching the goal type, which is arguably a bit more
+user-friendly than showing possibly match-compilation-internal variable names.
 -/
 private def filterTrivialCnstrs (alt : Alt) : MetaM Alt := do
    let cnstrs ← withExistingLocalDecls alt.fvarDecls do
@@ -334,8 +356,9 @@ private def processAsPattern (p : Problem) : MetaM Problem := withGoalOf p do
   let alts ← p.alts.mapM fun alt => do
     match alt.patterns with
     | .as fvarId p h :: ps =>
-      /- We used to use `checkAndReplaceFVarId` here, but `x` and `fvarId` may have different types
-        when dependent types are being used. Let's consider the repro for issue #471
+      /- We used to use eagerly check the types here (using what was called `checkAndReplaceFVarId`),
+        but `x` and `fvarId` can have different types when dependent types are being used.
+        Let's consider the repro for issue #471
         ```
         inductive vec : Nat → Type
         | nil : vec 0
@@ -409,11 +432,11 @@ alternative `cnstrs` field.
 private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool :=
   localDecls.any fun d => d.fvarId == fvarId
 
-private def expandVarIntoCtor? (alt : Alt) (ctorName : Name) : MetaM Alt := do
+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}"
+    trace[Meta.Match.unify] "expandVarIntoCtor fvarId: {mkFVar fvarId}, ctorName: {ctorName}, alt:\n{← alt.toMessageData}"
     let expectedType ← inferType (mkFVar fvarId)
     let expectedType ← whnfD expectedType
     let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType
@@ -427,7 +450,7 @@ private def expandVarIntoCtor? (alt : Alt) (ctorName : Name) : MetaM Alt := do
       let mut cnstrs := alt.cnstrs
       unless (← isDefEqGuarded resultType expectedType) do
          cnstrs := (resultType, expectedType) :: cnstrs
-      trace[Meta.Match.unify] "expandVarIntoCtor? {mkFVar fvarId} : {expectedType}, ctor: {ctor}"
+      trace[Meta.Match.unify] "expandVarIntoCtor {mkFVar fvarId} : {expectedType}, ctor: {ctor}"
       let ctorFieldPatterns := ctorFieldDecls.toList.map fun decl => Pattern.var decl.fvarId
       return { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns, cnstrs }
 
@@ -443,17 +466,6 @@ private def expandInaccessibleIntoVar (alt : Alt) : MetaM Alt := do
         cnstrs := (x, e) :: alt.cnstrs
       }
 
-private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
-  let xType ← inferType x
-  let xType ← whnfD xType
-  match xType.getAppFn with
-  | Expr.const constName _ =>
-    let cinfo ← getConstInfo constName
-    match cinfo with
-    | ConstantInfo.inductInfo val => return some val
-    | _ => return none
-  | _ => return none
-
 private def hasRecursiveType (x : Expr) : MetaM Bool := do
   match (← getInductiveVal? x) with
   | some val => return val.isRec
@@ -461,28 +473,24 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do
 
 /-- Given `alt` s.t. the next pattern is an inaccessible pattern `e`,
    try to normalize `e` into a constructor application.
-   If it is not a constructor, throw an error.
-   Otherwise, if it is a constructor application of `ctorName`,
+   If it is a constructor application of `ctorName`,
    update the next patterns with the fields of the constructor.
    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}"
+  let .inaccessible e :: ps := alt.patterns | unreachable!
+  trace[Meta.Match.match] "inaccessible step {e} as ctor {ctorName}"
   withExistingLocalDecls alt.fvarDecls do
     -- Try to push inaccessible annotations.
     let e ← whnfD e
-    match (← constructorApp? e) with
-    | some (ctorVal, ctorArgs) =>
+    if let some (ctorVal, ctorArgs) ← constructorApp? e then
       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}"
+    let alt' ← expandInaccessibleIntoVar alt
+    expandVarIntoCtor alt' ctorName
 
 private def hasNonTrivialExample (p : Problem) : Bool :=
   p.examples.any fun | Example.underscore => false | _ => true
@@ -546,7 +554,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
     let newAlts ← newAlts.mapM fun alt => do
       match alt.patterns with
       | .ctor _ _ _ fields :: ps  => return { alt with patterns := fields ++ ps }
-      | .var _ :: _               => expandVarIntoCtor? alt subgoal.ctorName
+      | .var _ :: _               => expandVarIntoCtor alt subgoal.ctorName
       | .inaccessible _ :: _      => processInaccessibleAsCtor alt subgoal.ctorName
       | _                         => unreachable!
     return { mvarId := subgoal.mvarId, vars := newVars, alts := newAlts, examples := examples }
@@ -563,7 +571,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
+        | .var _ :: _          => expandVarIntoCtor alt ctorVal.name
         | _ => unreachable!
       let xFields := xArgs.extract ctorVal.numParams xArgs.size
       return { p with alts := alts, vars := xFields.toList ++ xs }
@@ -724,13 +732,6 @@ private def throwNonSupported (p : Problem) : MetaM Unit :=
     let msg ← p.toMessageData
     throwError "Failed to compile pattern matching: Stuck at{indentD msg}"
 
-def isCurrVarInductive (p : Problem) : MetaM Bool := do
-  match p.vars with
-  | []   => return false
-  | x::_ => withGoalOf p do
-    let val? ← getInductiveVal? x
-    return val?.isSome
-
 private def checkNextPatternTypes (p : Problem) : MetaM Unit := do
   match p.vars with
   | []   => return ()
@@ -760,55 +761,79 @@ def processExFalso (p : Problem) : MetaM Problem := do
 
 private partial def process (p : Problem) : StateRefT State MetaM Unit := do
   traceState p
-  let isInductive ← isCurrVarInductive p
   if isDone p then
     traceStep ("leaf")
     processLeaf p
-  else if (← isExFalsoTransition p) then
+    return
+
+  if (← isExFalsoTransition p) then
     traceStep ("ex falso")
     let p ← processExFalso p
     process p
-  else if hasAsPattern p then
+    return
+
+  if hasAsPattern p then
     traceStep ("as-pattern")
     let p ← processAsPattern p
     process p
-  else if (← isNatValueTransition p) then
+    return
+
+  if (← isNatValueTransition p) then
     traceStep ("nat value to constructor")
     process (← expandNatValuePattern p)
-  else if (← isIntValueTransition p) then
+    return
+
+  if (← isIntValueTransition p) then
     traceStep ("int value to constructor")
     process (← expandIntValuePattern p)
-  else if (← isFinValueTransition p) then
+    return
+
+  if (← isFinValueTransition p) then
     traceStep ("fin value to constructor")
     process (← expandFinValuePattern p)
-  else if (← isBitVecValueTransition p) then
+    return
+
+  if (← isBitVecValueTransition p) then
     traceStep ("bitvec value to constructor")
     process (← expandBitVecValuePattern p)
-  else if !isNextVar p then
+    return
+
+  if !isNextVar p then
     traceStep ("non variable")
     let p ← processNonVariable p
     process p
-  else if isInductive && isConstructorTransition p then
+    return
+
+  if (← isConstructorTransition p) then
     let ps ← processConstructor p
     ps.forM process
-  else if isVariableTransition p then
+    return
+
+  if isVariableTransition p then
     traceStep ("variable")
     let p ← processVariable p
     process p
-  else if isValueTransition p then
+    return
+
+  if isValueTransition p then
     let ps ← processValue p
     ps.forM process
-  else if isArrayLitTransition p then
+    return
+
+  if isArrayLitTransition p then
     let ps ← processArrayLit p
     ps.forM process
-  else if (← hasNatValPattern p) then
+    return
+
+  if (← hasNatValPattern p) then
     -- This branch is reachable when `p`, for example, is just values without an else-alternative.
     -- We added it just to get better error messages.
     traceStep ("nat value to constructor")
     process (← expandNatValuePattern p)
-  else
-    checkNextPatternTypes p
-    throwNonSupported p
+    return
+
+  checkNextPatternTypes p
+  throwNonSupported p
 
 private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) :=
   if uElim == levelZero then
diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean
deleted file mode 100644
index 4e973b2a1596..000000000000
--- a/tests/lean/match1.lean
+++ /dev/null
@@ -1,164 +0,0 @@
---
-
-#print "---- h1"
-
-def h1 (b : Bool) : Nat :=
-match b with
-| true  => 0
-| false => 10
-
-#eval h1 false
-
-#print "---- h2"
-
-def h2 (x : List Nat) : Nat :=
-match x with
-| [x1, x2] => x1 + x2
-| x::xs    => x
-| _        => 0
-
-#eval h2 [1, 2]
-#eval h2 [10, 4, 5]
-#eval h2 []
-
-#print "---- h3"
-
-def h3 (x : Array Nat) : Nat :=
-match x with
-| #[x]    => x
-| #[x, y] => x + y
-| xs      => xs.size
-
-#eval h3 #[10]
-#eval h3 #[10, 20]
-#eval h3 #[10, 20, 30, 40]
-
-#print "---- inv"
-
-inductive Image {α β : Type} (f : α → β) : β → Type
-| mk (a : α) : Image f (f a)
-
-def mkImage {α β : Type} (f : α → β) (a : α) : Image f (f a) :=
-Image.mk a
-
-def inv {α β : Type} {f : α → β} {b : β} (t : Image f b) : α :=
-match b, t with
-| _, Image.mk a => a
-
-#eval inv (mkImage Nat.succ 10)
-
-theorem foo {p q} (h : p ∨ q) : q ∨ p :=
-match h with
-| Or.inl h => Or.inr h
-| Or.inr h => Or.inl h
-
-def f (x : Nat × Nat) : Bool × Bool × Bool → Nat :=
-match x with
-| (a, b) => fun _ => a
-
-structure S :=
-(x y z : Nat := 0)
-
-def f1 : S → S :=
-fun { x := x, ..} => { y := x }
-
-theorem ex2 : f1 { x := 10 } = { y := 10 } :=
-rfl
-
-universe u
-
-inductive Vec (α : Type u) : Nat → Type u
-| nil : Vec α 0
-| cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
-
-inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop
-| nil   : VecPred P Vec.nil
-| cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
-
-theorem ex3 {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-| _, Vec.cons head _, VecPred.cons h _ => ⟨head, h⟩
-
-theorem ex4 {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
-| _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩  -- ERROR
-
-axiom someNat : Nat
-
-noncomputable def f2 (x : Nat) := -- must mark as noncomputable since it uses axiom `someNat`
-x + someNat
-
-inductive Parity : Nat -> Type
-| even (n) : Parity (n + n)
-| odd  (n) : Parity (Nat.succ (n + n))
-
-axiom nDiv2 (n : Nat)     : n % 2 = 0 → n = n/2 + n/2
-axiom nDiv2Succ (n : Nat) : n % 2 ≠ 0 → n = Nat.succ (n/2 + n/2)
-
-def parity (n : Nat) : Parity n :=
-if h : n % 2 = 0 then
-  Eq.ndrec (Parity.even (n/2)) (nDiv2 n h).symm
-else
-  Eq.ndrec (Parity.odd (n/2)) (nDiv2Succ n h).symm
-
-partial def natToBin : (n : Nat) → List Bool
-| 0 => []
-| n => match n, parity n with
-  | _, Parity.even j => false :: natToBin j
-  | _, Parity.odd  j => true  :: natToBin j
-
-#eval natToBin 6
-
-partial def natToBin' : (n : Nat) → List Bool
-| 0 => []
-| n => match parity n with
-  | Parity.even j => false :: natToBin j
-  | Parity.odd  j => true  :: natToBin j
-
-partial def natToBinBad (n : Nat) : List Bool :=
-match n, parity n with
-| 0, _             => []
-| _, Parity.even j => false :: natToBin j
-| _, Parity.odd  j => true  :: natToBin j
-
-partial def natToBin2 (n : Nat) : List Bool :=
-match n, parity n with
-| _, Parity.even 0 => []
-| _, Parity.even j => false :: natToBin j
-| _, Parity.odd  j => true  :: natToBin j
-
-#eval natToBin2 6
-
-partial def natToBin2' (n : Nat) : List Bool :=
-match parity n with
-| Parity.even 0 => []
-| Parity.even j => false :: natToBin j
-| Parity.odd  j => true  :: natToBin j
-
-#check fun (a, b) => a -- Error type of pattern variable contains metavariables
-
-#check fun (a, b) => (a:Nat) + b
-
-#check fun (a, b) => a && b
-
-#check fun ((a : Nat), (b : Nat)) => a + b
-
-#check fun
-  | some a, some b => some (a + b : Nat)
-  | _,      _      => none
-
--- overapplied matcher
-#check fun x => (match x with | 0 => id | x+1 => id) x
-
-#check fun
-  | #[1, 2]    => 2
-  | #[]        => 0
-  | #[3, 4, 5] => 3
-  | _          => 4
-
--- underapplied matcher
-def g {α} : List α → Nat
-  | [a] => 1
-  | _   => 0
-
-#check g.match_1
-
-#check fun (e : Empty) => (nomatch e : False)
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
deleted file mode 100644
index 675b23b8b824..000000000000
--- a/tests/lean/match1.lean.expected.out
+++ /dev/null
@@ -1,50 +0,0 @@
----- h1
-10
----- h2
-3
-10
-0
----- h3
-10
-30
-4
----- inv
-10
-match1.lean:82:2-82:60: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive 0 (Vec.cons head✝ Vec.nil) ⋯
-but is expected to have type
-  motive x✝ (Vec.cons head✝ tail✝) ⋯
-[false, true, true]
-match1.lean:119:2-119:18: error: Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern
-  .(j + j)
-[false, true, true]
-match1.lean:136:7-136:22: error: Invalid match expression: The type of pattern variable 'a' contains metavariables:
-  ?m
-fun x => ?m : ?m × ?m → ?m
-fun x =>
-  match x with
-  | (a, b) => a + b : Nat × Nat → Nat
-fun x =>
-  match x with
-  | (a, b) => a && b : Bool × Bool → Bool
-fun x =>
-  match x with
-  | (a, b) => a + b : Nat × Nat → Nat
-fun x x_1 =>
-  match x, x_1 with
-  | some a, some b => some (a + b)
-  | x, x_2 => none : Option Nat → Option Nat → Option Nat
-fun x =>
-  (match (motive := Nat → Nat → Nat) x with
-    | 0 => id
-    | x.succ => id)
-    x : Nat → Nat
-fun x =>
-  match x with
-  | #[1, 2] => 2
-  | #[] => 0
-  | #[3, 4, 5] => 3
-  | x => 4 : Array Nat → Nat
-g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
-  (h_2 : (x : List α) → motive x) : motive x✝
-fun e => nomatch e : ∀ (e : Empty), False
diff --git a/tests/lean/run/issue10749.lean b/tests/lean/run/issue10749.lean
new file mode 100644
index 000000000000..069f07ba7544
--- /dev/null
+++ b/tests/lean/run/issue10749.lean
@@ -0,0 +1,107 @@
+-- set_option trace.Meta.Match.debug true
+-- set_option trace.Meta.Match.match true
+
+set_option match.ignoreUnusedAlts true in
+def test (a : List Nat) : Nat :=
+  match a with
+  | _ => 3
+  | [] => 4
+
+-- Should have no `casesOn`
+
+/--
+info: def test.match_1.{u_1} : (motive : List Nat → Sort u_1) →
+  (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
+fun motive a h_1 h_2 => List.casesOn a (h_1 []) fun head tail => h_1 (head :: tail)
+-/
+#guard_msgs in #print test.match_1
+
+def test2 (a b : List Nat) : Nat :=
+  match a, b with
+  | [], _ => 3
+  | _, [] => 4
+  | _ :: _, _ :: _ => 5
+
+/--
+info: def test2.match_1.{u_1} : (motive : List Nat → List Nat → Sort u_1) →
+  (a b : List Nat) →
+    ((x : List Nat) → motive [] x) →
+      ((x : List Nat) → motive x []) →
+        ((head : Nat) →
+            (tail : List Nat) → (head_1 : Nat) → (tail_1 : List Nat) → motive (head :: tail) (head_1 :: tail_1)) →
+          motive a b :=
+fun motive a b h_1 h_2 h_3 =>
+  List.casesOn a (List.casesOn b (h_1 []) fun head tail => h_1 (head :: tail)) fun head tail =>
+    List.casesOn b (h_2 (head :: tail)) fun head_1 tail_1 => h_3 head tail head_1 tail_1
+-/
+#guard_msgs in #print test2.match_1
+
+def test3 (a : List Nat) (b : Bool) : Nat :=
+  match a, b with
+  | _, true => 0
+  | [], _ => 1
+  | _, _ => 2
+
+-- Should have exactly two `casesOn`
+
+/--
+info: def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
+  (a : List Nat) →
+    (b : Bool) →
+      ((x : List Nat) → motive x true) →
+        ((x : Bool) → motive [] x) → ((x : List Nat) → (x_1 : Bool) → motive x x_1) → motive a b :=
+fun motive a b h_1 h_2 h_3 =>
+  List.casesOn a (Bool.casesOn b (h_2 false) (h_1 [])) fun head tail =>
+    Bool.casesOn b (h_3 (head :: tail) false) (h_1 (head :: tail))
+-/
+#guard_msgs in #print test3.match_1
+
+set_option maxHeartbeats 100 in
+example (P : Nat → Prop) (x : Nat) (h : x = 12345) (hP : P 12345) : P x :=
+  match x, h with | _, rfl => hP
+
+
+def test4 : Bool → Bool → Bool → Bool → Bool → Bool
+  | _, _ , _ , _ , true => true
+  | _, _ , _ , true , _ => true
+  | _, _ , true , _ , _ => true
+  | _, true , _ , _ , _ => true
+  | true , _ , _ , _ , _ => true
+  | _ , _ , _ , _ , _ => false
+
+/--
+info: def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
+  (x x_1 x_2 x_3 x_4 : Bool) →
+    ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 x_7 true) →
+      ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 true x_7) →
+        ((x x_5 x_6 x_7 : Bool) → motive x x_5 true x_6 x_7) →
+          ((x x_5 x_6 x_7 : Bool) → motive x true x_5 x_6 x_7) →
+            ((x x_5 x_6 x_7 : Bool) → motive true x x_5 x_6 x_7) →
+              ((x x_5 x_6 x_7 x_8 : Bool) → motive x x_5 x_6 x_7 x_8) → motive x x_1 x_2 x_3 x_4 :=
+fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
+  Bool.casesOn x
+    (Bool.casesOn x_1
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_6 false false false false false) (h_1 false false false false))
+          (Bool.casesOn x_4 (h_2 false false false false) (h_1 false false false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 false false false false) (h_1 false false true false))
+          (Bool.casesOn x_4 (h_2 false false true false) (h_1 false false true true))))
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_4 false false false false) (h_1 false true false false))
+          (Bool.casesOn x_4 (h_2 false true false false) (h_1 false true false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 false true false false) (h_1 false true true false))
+          (Bool.casesOn x_4 (h_2 false true true false) (h_1 false true true true)))))
+    (Bool.casesOn x_1
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_5 false false false false) (h_1 true false false false))
+          (Bool.casesOn x_4 (h_2 true false false false) (h_1 true false false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 true false false false) (h_1 true false true false))
+          (Bool.casesOn x_4 (h_2 true false true false) (h_1 true false true true))))
+      (Bool.casesOn x_2
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_4 true false false false) (h_1 true true false false))
+          (Bool.casesOn x_4 (h_2 true true false false) (h_1 true true false true)))
+        (Bool.casesOn x_3 (Bool.casesOn x_4 (h_3 true true false false) (h_1 true true true false))
+          (Bool.casesOn x_4 (h_2 true true true false) (h_1 true true true true)))))
+-/
+#guard_msgs in
+#print test4.match_1
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index 4e90d65de1f1..f14a4ae7c6df 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -1,172 +1,246 @@
-import Lean
+set_option linter.unusedVariables false
+--
 
-def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit :=
-  Lean.Meta.Match.withMkMatcherInput matcher fun input => do
-  let res ← Lean.Meta.Match.mkMatcher input
-  let origMatcher ← Lean.getConstInfo matcher
-  if not <| input.matcherName == matcher then
-    throwError "matcher name not reconstructed correctly: {matcher} ≟ {input.matcherName}"
+def h1 (b : Bool) : Nat :=
+match b with
+| true  => 0
+| false => 10
 
-  let lCtx ← Lean.getLCtx
-  let fvars := Lean.collectFVars {} res.matcher
-  let closure := Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher
-
-  let origTy := origMatcher.value!
-  let newTy := closure
-  if not <| ←Lean.Meta.isDefEq origTy newTy then
-    throwError "matcher {matcher} does not round-trip correctly:\n{origTy} ≟ {newTy}"
-
-set_option smartUnfolding false
+/-- info: 10 -/
+#guard_msgs in
+#eval h1 false
 
-def f (xs : List Nat) : List Bool :=
-xs.map fun
-  | 0 => true
-  | _ => false
+def h2 (x : List Nat) : Nat :=
+match x with
+| [x1, x2] => x1 + x2
+| x::xs    => x
+| _        => 0
 
+/-- info: 10 -/
 #guard_msgs in
-#eval checkWithMkMatcherInput ``f.match_1
-
-#guard f [1, 2, 0, 2] == [false, false, true, false]
+#eval h1 false
+/-- info: 3 -/
+#guard_msgs in
+#eval h2 [1, 2]
+/-- info: 10 -/
+#guard_msgs in
+#eval h2 [10, 4, 5]
+/-- info: 0 -/
+#guard_msgs in
+#eval h2 []
 
-theorem ex1 : f [1, 0, 2] = [false, true, false] :=
-rfl
+def h3 (x : Array Nat) : Nat :=
+match x with
+| #[x]    => x
+| #[x, y] => x + y
+| xs      => xs.size
 
-#check f
+/-- info: 10 -/
+#guard_msgs in
+#eval h3 #[10]
+/-- info: 30 -/
+#guard_msgs in
+#eval h3 #[10, 20]
+/-- info: 4 -/
+#guard_msgs in
+#eval h3 #[10, 20, 30, 40]
 
-set_option pp.raw true
-set_option pp.raw.maxDepth 10
-set_option trace.Elab.step true in
-def g (xs : List Nat) : List Bool :=
-xs.map <| by {
-  intro
-    | 0 => exact true
-    | _ => exact false
-}
+inductive Image {α β : Type} (f : α → β) : β → Type
+| mk (a : α) : Image f (f a)
 
-theorem ex2 : g [1, 0, 2] = [false, true, false] :=
-rfl
+def mkImage {α β : Type} (f : α → β) (a : α) : Image f (f a) :=
+Image.mk a
 
-theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
-by intro
- | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
- | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
+def inv {α β : Type} {f : α → β} {b : β} (t : Image f b) : α :=
+match b, t with
+| _, Image.mk a => a
 
-inductive C
-| mk₁ : Nat → C
-| mk₂ : Nat → Nat → C
+/-- info: 10 -/
+#guard_msgs in
+#eval inv (mkImage Nat.succ 10)
 
-def C.x : C → Nat
-| C.mk₁ x   => x
-| C.mk₂ x _ => x
-#eval checkWithMkMatcherInput ``C.x.match_1
+theorem foo {p q} (h : p ∨ q) : q ∨ p :=
+match h with
+| Or.inl h => Or.inr h
+| Or.inr h => Or.inl h
 
-def head : {α : Type} → List α → Option α
-| _, a::as => some a
-| _, _     => none
-#eval checkWithMkMatcherInput ``head.match_1
+def f (x : Nat × Nat) : Bool × Bool × Bool → Nat :=
+match x with
+| (a, b) => fun _ => a
 
-theorem ex4 : head [1, 2] = some 1 :=
-rfl
+structure S where
+  (x y z : Nat := 0)
 
-def head2 : {α : Type} → List α → Option α :=
-@fun
-  | _, a::as => some a
-  | _, _     => none
+def f1 : S → S :=
+fun { x := x, ..} => { y := x }
 
-theorem ex5 : head2 [1, 2] = some 1 :=
+theorem ex2 : f1 { x := 10 } = { y := 10 } :=
 rfl
 
-def head3 {α : Type} (xs : List α) : Option α :=
-let rec aux {α : Type} : List α → Option α
-  | a::_ => some a
-  | _    => none;
-aux xs
-
-theorem ex6 : head3 [1, 2] = some 1 :=
-rfl
+universe u
 
-inductive Vec.{u} (α : Type u) : Nat → Type u
+inductive Vec (α : Type u) : Nat → Type u
 | nil : Vec α 0
 | cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
 
-def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
-| _,   nil,       nil,       f => none
-| _, cons a as, cons b bs,   f => some (f a b)
+inductive VecPred {α : Type u} (P : α → Prop) : {n : Nat} → Vec α n → Prop
+| nil   : VecPred P Vec.nil
+| cons  {n : Nat} {head : α} {tail : Vec α n} : P head → VecPred P tail → VecPred P (Vec.cons head tail)
 
+theorem ex3 {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
+| _, Vec.cons head _, VecPred.cons h _ => ⟨head, h⟩
 
-def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
-| _, nil,            nil,         f => none
-| _, @cons _ n a as, cons b bs,   f => some (f a b)
-set_option pp.match false in
-#print Vec.mapHead2 -- reused Vec.mapHead1.match_1
-
-def Vec.mapHead3 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
-| _, nil,            nil,         f => none
-| _, cons (tail := as) (head := a), cons b bs,   f => some (f a b)
+/--
+error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
+  motive 0 (Vec.cons head✝ Vec.nil) ⋯
+but is expected to have type
+  motive x✝ (Vec.cons head✝ tail✝) ⋯
+-/
+#guard_msgs in
+theorem ex4 {α : Type u} (P : α → Prop) : {n : Nat} → (v : Vec α (n+1)) → VecPred P v → Exists P
+| _, Vec.cons head _, VecPred.cons h (w : VecPred P Vec.nil) => ⟨head, h⟩  -- ERROR
 
-inductive Foo
-| mk₁ (x y z w : Nat)
-| mk₂ (x y z w : Nat)
+axiom someNat : Nat
 
-def Foo.z : Foo → Nat
-| mk₁ (z := z) .. => z
-| mk₂ (z := z) .. => z
+noncomputable def f2 (x : Nat) := -- must mark as noncomputable since it uses axiom `someNat`
+x + someNat
 
-#eval checkWithMkMatcherInput ``Foo.z.match_1
+inductive Parity : Nat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (Nat.succ (n + n))
 
-#guard (Foo.mk₁ 10 20 30 40).z == 30
+axiom nDiv2 (n : Nat)     : n % 2 = 0 → n = n/2 + n/2
+axiom nDiv2Succ (n : Nat) : n % 2 ≠ 0 → n = Nat.succ (n/2 + n/2)
 
-theorem ex7 : (Foo.mk₁ 10 20 30 40).z = 30 :=
-rfl
+def parity (n : Nat) : Parity n :=
+if h : n % 2 = 0 then
+  Eq.ndrec (Parity.even (n/2)) (nDiv2 n h).symm
+else
+  Eq.ndrec (Parity.odd (n/2)) (nDiv2Succ n h).symm
 
-def Foo.addY? : Foo × Foo → Option Nat
-| (mk₁ (y := y₁) .., mk₁ (y := y₂) ..) => some (y₁ + y₂)
-| _ => none
+partial def natToBin : (n : Nat) → List Bool
+| 0 => []
+| n => match n, parity n with
+  | _, Parity.even j => false :: natToBin j
+  | _, Parity.odd  j => true  :: natToBin j
 
-#eval checkWithMkMatcherInput ``Foo.addY?.match_1
+/-- info: [false, true, true] -/
+#guard_msgs in
+#eval natToBin 6
+
+partial def natToBin' : (n : Nat) → List Bool
+| 0 => []
+| n => match parity n with
+  | Parity.even j => false :: natToBin j
+  | Parity.odd  j => true  :: natToBin j
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  Nat.zero = n✝.add n✝
+at case `Parity.even` after processing
+  Nat.zero, _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs in
+partial def natToBinBad (n : Nat) : List Bool :=
+match n, parity n with
+| 0, _             => []
+| _, Parity.even j => false :: natToBin j
+| _, Parity.odd  j => true  :: natToBin j
+
+partial def natToBin2 (n : Nat) : List Bool :=
+match n, parity n with
+| _, Parity.even 0 => []
+| _, Parity.even j => false :: natToBin j
+| _, Parity.odd  j => true  :: natToBin j
+
+/-- info: [false, true, true] -/
+#guard_msgs in
+#eval natToBin2 6
+
+partial def natToBin2' (n : Nat) : List Bool :=
+match parity n with
+| Parity.even 0 => []
+| Parity.even j => false :: natToBin j
+| Parity.odd  j => true  :: natToBin j
+
+/--
+error: Invalid match expression: The type of pattern variable 'a' contains metavariables:
+  ?m.12
+---
+info: fun x => ?m.3 : ?m.12 × ?m.13 → ?m.12
+-/
+#guard_msgs in
+#check fun (a, b) => a -- Error type of pattern variable contains metavariables
 
-#guard Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) == some 22
+/--
+info: fun x =>
+  match x with
+  | (a, b) => a + b : Nat × Nat → Nat
+-/
+#guard_msgs in
+#check fun (a, b) => (a:Nat) + b
 
-theorem ex8 : Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) = some 22 :=
-rfl
+/--
+info: fun x =>
+  match x with
+  | (a, b) => a && b : Bool × Bool → Bool
+-/
+#guard_msgs in
+#check fun (a, b) => a && b
 
-instance {α} : Inhabited (Sigma fun m => Vec α m) :=
-⟨⟨0, Vec.nil⟩⟩
-
-partial def filter {α} (p : α → Bool) : {n : Nat} → Vec α n → Sigma fun m => Vec α m
-| _, Vec.nil        => ⟨0, Vec.nil⟩
-| _, Vec.cons x xs  => match p x, filter p xs with
-  | true,  ⟨_, ys⟩ => ⟨_, Vec.cons x ys⟩
-  | false, ys      => ys
-#eval checkWithMkMatcherInput ``filter.match_1
-
-inductive Bla
-| ofNat  (x : Nat)
-| ofBool (x : Bool)
-
-def Bla.optional? : Bla → Option Nat
-| ofNat x  => some x
-| ofBool _ => none
-#eval checkWithMkMatcherInput ``Bla.optional?.match_1
-
-def Bla.isNat? (b : Bla) : Option { x : Nat // optional? b = some x } :=
-match b.optional? with
-| some y => some ⟨y, rfl⟩
-| none   => none
-#eval checkWithMkMatcherInput ``Bla.isNat?.match_1
-
-def foo (b : Bla) : Option Nat := b.optional?
-theorem fooEq (b : Bla) : foo b = b.optional? :=
-rfl
+/--
+info: fun x =>
+  match x with
+  | (a, b) => a + b : Nat × Nat → Nat
+-/
+#guard_msgs in
+#check fun ((a : Nat), (b : Nat)) => a + b
+
+/--
+info: fun x x_1 =>
+  match x, x_1 with
+  | some a, some b => some (a + b)
+  | x, x_2 => none : Option Nat → Option Nat → Option Nat
+-/
+#guard_msgs in
+#check fun
+  | some a, some b => some (a + b : Nat)
+  | _,      _      => none
+
+-- overapplied matcher
+/--
+info: fun x =>
+  (match (motive := Nat → Nat → Nat) x with
+    | 0 => id
+    | x.succ => id)
+    x : Nat → Nat
+-/
+#guard_msgs in
+#check fun x => (match x with | 0 => id | x+1 => id) x
+
+#guard_msgs(drop info) in
+#check fun
+  | #[1, 2]    => 2
+  | #[]        => 0
+  | #[3, 4, 5] => 3
+  | _          => 4
+
+-- underapplied matcher
+def g {α} : List α → Nat
+  | [a] => 1
+  | _   => 0
+
+/--
+info: g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
+  (h_2 : (x : List α) → motive x) : motive x✝
+-/
+#guard_msgs in
+#check g.match_1
 
-def Bla.isNat2? (b : Bla) : Option { x : Nat // optional? b = some x } :=
-match h : foo b with
-| some y => some ⟨y, Eq.trans (fooEq b).symm h⟩
-| none   => none
-#eval checkWithMkMatcherInput ``Bla.isNat2?.match_1
-
-def foo2 (x : Nat) : Nat :=
-match (motive := (y : Nat) → x = y → Nat) x, rfl with
-| 0,   h => 0
-| x+1, h => 1
-#eval checkWithMkMatcherInput ``foo2.match_1
+#guard_msgs(drop info) in
+#check fun (e : Empty) => (nomatch e : False)
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
new file mode 100644
index 000000000000..4e90d65de1f1
--- /dev/null
+++ b/tests/lean/run/match2.lean
@@ -0,0 +1,172 @@
+import Lean
+
+def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit :=
+  Lean.Meta.Match.withMkMatcherInput matcher fun input => do
+  let res ← Lean.Meta.Match.mkMatcher input
+  let origMatcher ← Lean.getConstInfo matcher
+  if not <| input.matcherName == matcher then
+    throwError "matcher name not reconstructed correctly: {matcher} ≟ {input.matcherName}"
+
+  let lCtx ← Lean.getLCtx
+  let fvars := Lean.collectFVars {} res.matcher
+  let closure := Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher
+
+  let origTy := origMatcher.value!
+  let newTy := closure
+  if not <| ←Lean.Meta.isDefEq origTy newTy then
+    throwError "matcher {matcher} does not round-trip correctly:\n{origTy} ≟ {newTy}"
+
+set_option smartUnfolding false
+
+def f (xs : List Nat) : List Bool :=
+xs.map fun
+  | 0 => true
+  | _ => false
+
+#guard_msgs in
+#eval checkWithMkMatcherInput ``f.match_1
+
+#guard f [1, 2, 0, 2] == [false, false, true, false]
+
+theorem ex1 : f [1, 0, 2] = [false, true, false] :=
+rfl
+
+#check f
+
+set_option pp.raw true
+set_option pp.raw.maxDepth 10
+set_option trace.Elab.step true in
+def g (xs : List Nat) : List Bool :=
+xs.map <| by {
+  intro
+    | 0 => exact true
+    | _ => exact false
+}
+
+theorem ex2 : g [1, 0, 2] = [false, true, false] :=
+rfl
+
+theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
+by intro
+ | Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
+ | Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
+
+inductive C
+| mk₁ : Nat → C
+| mk₂ : Nat → Nat → C
+
+def C.x : C → Nat
+| C.mk₁ x   => x
+| C.mk₂ x _ => x
+#eval checkWithMkMatcherInput ``C.x.match_1
+
+def head : {α : Type} → List α → Option α
+| _, a::as => some a
+| _, _     => none
+#eval checkWithMkMatcherInput ``head.match_1
+
+theorem ex4 : head [1, 2] = some 1 :=
+rfl
+
+def head2 : {α : Type} → List α → Option α :=
+@fun
+  | _, a::as => some a
+  | _, _     => none
+
+theorem ex5 : head2 [1, 2] = some 1 :=
+rfl
+
+def head3 {α : Type} (xs : List α) : Option α :=
+let rec aux {α : Type} : List α → Option α
+  | a::_ => some a
+  | _    => none;
+aux xs
+
+theorem ex6 : head3 [1, 2] = some 1 :=
+rfl
+
+inductive Vec.{u} (α : Type u) : Nat → Type u
+| nil : Vec α 0
+| cons {n} (head : α) (tail : Vec α n) : Vec α (n+1)
+
+def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
+| _,   nil,       nil,       f => none
+| _, cons a as, cons b bs,   f => some (f a b)
+
+
+def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
+| _, nil,            nil,         f => none
+| _, @cons _ n a as, cons b bs,   f => some (f a b)
+set_option pp.match false in
+#print Vec.mapHead2 -- reused Vec.mapHead1.match_1
+
+def Vec.mapHead3 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
+| _, nil,            nil,         f => none
+| _, cons (tail := as) (head := a), cons b bs,   f => some (f a b)
+
+inductive Foo
+| mk₁ (x y z w : Nat)
+| mk₂ (x y z w : Nat)
+
+def Foo.z : Foo → Nat
+| mk₁ (z := z) .. => z
+| mk₂ (z := z) .. => z
+
+#eval checkWithMkMatcherInput ``Foo.z.match_1
+
+#guard (Foo.mk₁ 10 20 30 40).z == 30
+
+theorem ex7 : (Foo.mk₁ 10 20 30 40).z = 30 :=
+rfl
+
+def Foo.addY? : Foo × Foo → Option Nat
+| (mk₁ (y := y₁) .., mk₁ (y := y₂) ..) => some (y₁ + y₂)
+| _ => none
+
+#eval checkWithMkMatcherInput ``Foo.addY?.match_1
+
+#guard Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) == some 22
+
+theorem ex8 : Foo.addY? (Foo.mk₁ 1 2 3 4, Foo.mk₁ 10 20 30 40) = some 22 :=
+rfl
+
+instance {α} : Inhabited (Sigma fun m => Vec α m) :=
+⟨⟨0, Vec.nil⟩⟩
+
+partial def filter {α} (p : α → Bool) : {n : Nat} → Vec α n → Sigma fun m => Vec α m
+| _, Vec.nil        => ⟨0, Vec.nil⟩
+| _, Vec.cons x xs  => match p x, filter p xs with
+  | true,  ⟨_, ys⟩ => ⟨_, Vec.cons x ys⟩
+  | false, ys      => ys
+#eval checkWithMkMatcherInput ``filter.match_1
+
+inductive Bla
+| ofNat  (x : Nat)
+| ofBool (x : Bool)
+
+def Bla.optional? : Bla → Option Nat
+| ofNat x  => some x
+| ofBool _ => none
+#eval checkWithMkMatcherInput ``Bla.optional?.match_1
+
+def Bla.isNat? (b : Bla) : Option { x : Nat // optional? b = some x } :=
+match b.optional? with
+| some y => some ⟨y, rfl⟩
+| none   => none
+#eval checkWithMkMatcherInput ``Bla.isNat?.match_1
+
+def foo (b : Bla) : Option Nat := b.optional?
+theorem fooEq (b : Bla) : foo b = b.optional? :=
+rfl
+
+def Bla.isNat2? (b : Bla) : Option { x : Nat // optional? b = some x } :=
+match h : foo b with
+| some y => some ⟨y, Eq.trans (fooEq b).symm h⟩
+| none   => none
+#eval checkWithMkMatcherInput ``Bla.isNat2?.match_1
+
+def foo2 (x : Nat) : Nat :=
+match (motive := (y : Nat) → x = y → Nat) x, rfl with
+| 0,   h => 0
+| x+1, h => 1
+#eval checkWithMkMatcherInput ``foo2.match_1
diff --git a/tests/lean/run/matchOverlapInaccesible.lean b/tests/lean/run/matchOverlapInaccesible.lean
new file mode 100644
index 000000000000..af459f68a350
--- /dev/null
+++ b/tests/lean/run/matchOverlapInaccesible.lean
@@ -0,0 +1,72 @@
+set_option warn.sorry false
+
+inductive Parity : Nat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (Nat.succ (n + n))
+
+axiom nDiv2 (n : Nat)     : n % 2 = 0 → n = n/2 + n/2
+axiom nDiv2Succ (n : Nat) : n % 2 ≠ 0 → n = Nat.succ (n/2 + n/2)
+
+def parity (n : Nat) : Parity n :=
+if h : n % 2 = 0 then
+  Eq.ndrec (Parity.even (n/2)) (nDiv2 n h).symm
+else
+  Eq.ndrec (Parity.odd (n/2)) (nDiv2Succ n h).symm
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  Nat.zero = n✝.add n✝
+at case `Parity.even` after processing
+  Nat.zero, _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs in
+partial def natToBinBad (n : Nat) : List Bool :=
+match n, parity n with
+| 0, _             => []
+| _, Parity.even j => false :: natToBinBad j
+| _, Parity.odd  j => true  :: natToBinBad j
+
+
+inductive MyNat : Type where
+| zero : MyNat
+| succ : MyNat -> MyNat
+
+def MyNat.add : MyNat -> MyNat -> MyNat
+  | zero, n => n
+  | succ m, n => succ (add m n)
+
+instance : Add MyNat where
+  add := MyNat.add
+
+namespace MyNat
+
+inductive Parity : MyNat -> Type
+| even (n) : Parity (n + n)
+| odd  (n) : Parity (MyNat.succ (n + n))
+
+def parity (n : MyNat) : Parity n := sorry
+
+-- set_option trace.Meta.Match.match true
+
+/--
+error: Tactic `cases` failed with a nested error:
+Dependent elimination failed: Failed to solve equation
+  zero = n✝.add n✝
+at case `Parity.even` after processing
+  zero, _
+the dependent pattern matcher can solve the following kinds of equations
+- <var> = <term> and <term> = <var>
+- <term> = <term> where the terms are definitionally equal
+- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
+-/
+#guard_msgs(pass trace, all) in
+partial def myNatToBinBad (n : MyNat) : List Bool :=
+match n, parity n with
+| zero, _             => []
+| _, Parity.even j => false :: myNatToBinBad j
+| _, Parity.odd  j => true  :: myNatToBinBad j