diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 9136738181..e481033237 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -221,134 +221,62 @@ private def processVariable (p : Problem) : MetaM Problem := withGoalOf p do
     | _                     => unreachable!
   return { p with alts := alts, vars := xs }
 
-private def throwInductiveTypeExpected {α} (e : Expr) : MetaM α := do
-  let t ← inferType e
-  throwError "failed to compile pattern matching, inductive type expected{indentExpr e}\nhas type{indentExpr t}"
+/-
+  TODO: FIX the following issue.
+
+  `fvarId` is not an alternative variable, and we used to return `false` here, but it is incorrect, and may
+  incorrectly discard applicable alternatives. It was buggy because of the way we handle inaccessible patterns
+  in variable transitions. The bug was exposed by issue #1279
+  Here is a simplified version of the example on this issue (see test: `1279_simplified.lean`)
+  ```lean
+  inductive Arrow : Type → Type → Type 1
+    | id   : Arrow a a
+    | unit : Arrow Unit Unit
+    | comp : Arrow β γ → Arrow α β → Arrow α γ
+  deriving Repr
+
+  def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ :=
+    match f, g with
+    | id, g => g
+    | f, id => f
+    | f, g => comp f g
+  ```
+  The initial state for the `match`-expression above is
+  ```lean
+  [Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
+  alternatives:
+    [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g
+    [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f
+    [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g
+  ```
+  The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives.
+  The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable.
+  After applying the variable-transition step twice, we reach the following state
+  ```lean
+  [Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
+  alternatives:
+    [g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g
+    [f:(Arrow α γ✝)] |- [f, (Arrow.id .(α))] => h_2 γ✝ f
+    [f:(Arrow β✝ γ✝), g:(Arrow α β✝)] |- [f, g] => h_3 β✝ γ✝ f g
+  ```
+  A constructor-transition should be used, and the functions `expandVarIntoCtor?` is required for the second and
+  third alternatives. There are 3 constructors, in the `Arrow.id` case, we use unify to solve
+  ```
+  Arrow a a =?= Arrow α β✝
+  ```
+  Where `a` is new alternative variable corresponding to the `Arrow.id` field.
+  The first assignment is fine `a := α`.
+  In the second assignment we have `α := β✝` where both `α` and `β✝` are not alternative variables.
+  We did not store information that `β✝ === α` in the first step, and the alternative was being incorrectly discarded.
+  Returning `true` here "solves" the problem, but it is a bit hackish. We see two possible improvements:
+  - We store the constraint `β✝ === α`.
+  - We postpone variable-transition steps.
+  It is unclear at this point what is the best solution. We should keep accumulating problematic examples.
+-/
 
 private def inLocalDecls (localDecls : List LocalDecl) (fvarId : FVarId) : Bool :=
   localDecls.any fun d => d.fvarId == fvarId
 
-namespace Unify
-
-structure Context where
-  altFVarDecls : List LocalDecl
-
-structure State where
-  fvarSubst : FVarSubst := {}
-
-abbrev M := ReaderT Context $ StateRefT State MetaM
-
-def isAltVar (fvarId : FVarId) : M Bool := do
-  return inLocalDecls (← read).altFVarDecls fvarId
-
-def expandIfVar (e : Expr) : M Expr := do
-  match e with
-  | .fvar _ => return (← get).fvarSubst.apply e
-  | _       => return e
-
-def occurs (fvarId : FVarId) (v : Expr) : Bool :=
-  Option.isSome <| v.find? fun e => match e with
-     | .fvar fvarId' => fvarId == fvarId'
-     | _ => false
-
-def assign (fvarId : FVarId) (v : Expr) : M Bool := do
-  if occurs fvarId v then
-    trace[Meta.Match.unify] "assign occurs check failed, {mkFVar fvarId} := {v}"
-    return false
-  else
-    if (← isAltVar fvarId) then
-      trace[Meta.Match.unify] "{mkFVar fvarId} := {v}"
-      modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
-      return true
-    else
-      /-
-        TODO: improve this branch. Returning `true` here is an approximation.
-        `fvarId` is not an alternative variable, and we used to return `false` here, but it is incorrect, and may
-        incorrectly discard applicable alternatives. It was buggy because of the way we handle inaccessible patterns
-        in variable transitions. The bug was exposed by issue #1279
-        Here is a simplified version of the example on this issue (see test: `1279_simplified.lean`)
-        ```lean
-        inductive Arrow : Type → Type → Type 1
-          | id   : Arrow a a
-          | unit : Arrow Unit Unit
-          | comp : Arrow β γ → Arrow α β → Arrow α γ
-        deriving Repr
-
-        def Arrow.compose (f : Arrow β γ) (g : Arrow α β) : Arrow α γ :=
-          match f, g with
-          | id, g => g
-          | f, id => f
-          | f, g => comp f g
-        ```
-        The initial state for the `match`-expression above is
-        ```lean
-        [Meta.Match.match] remaining variables: [β✝:(Type), γ✝:(Type), f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
-        alternatives:
-          [β:(Type), g:(Arrow α β)] |- [β, .(β), (Arrow.id .(β)), g] => h_1 β g
-          [γ:(Type), f:(Arrow α γ)] |- [.(α), γ, f, (Arrow.id .(α))] => h_2 γ f
-          [β:(Type), γ:(Type), f:(Arrow β γ), g:(Arrow α β)] |- [β, γ, f, g] => h_3 β γ f g
-        ```
-        The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives.
-        The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable.
-        After applying the variable-transition step twice, we reach the following state
-        ```lean
-        [Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
-        alternatives:
-          [g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g
-          [f:(Arrow α γ✝)] |- [f, (Arrow.id .(α))] => h_2 γ✝ f
-          [f:(Arrow β✝ γ✝), g:(Arrow α β✝)] |- [f, g] => h_3 β✝ γ✝ f g
-        ```
-        A constructor-transition should be used, and the functions `expandVarIntoCtor?` is required for the second and
-        third alternatives. There are 3 constructors, in the `Arrow.id` case, we use unify to solve
-        ```
-        Arrow a a =?= Arrow α β✝
-        ```
-        Where `a` is new alternative variable corresponding to the `Arrow.id` field.
-        The first assignment is fine `a := α`.
-        In the second assignment we have `α := β✝` where both `α` and `β✝` are not alternative variables.
-        We did not store information that `β✝ === α` in the first step, and the alternative was being incorrectly discarded.
-        Returning `true` here "solves" the problem, but it is a bit hackish. We see two possible improvements:
-        - We store the constraint `β✝ === α`.
-        - We postpone variable-transition steps.
-        It is unclear at this point what is the best solution. We should keep accumulating problematic examples.
-      -/
-      return true
-
-partial def unify (a : Expr) (b : Expr) : M Bool := do
-  trace[Meta.Match.unify] "{a} =?= {b}"
-  if (← isDefEq a b) then
-    return true
-  else
-    let a' ← whnfD (← expandIfVar a)
-    let b' ← whnfD (← expandIfVar b)
-    if a != a' || b != b' then
-      unify a' b'
-    else match a, b with
-      | .fvar aFvarId, .fvar bFVarId => assign aFvarId b <||> assign bFVarId a
-      | .fvar aFvarId, b => assign aFvarId b
-      | a, .fvar bFVarId => assign bFVarId a
-      | .app aFn aArg, .app bFn bArg => unify aFn bFn <&&> unify aArg bArg
-      | _, _ =>
-        let a' := (← get).fvarSubst.apply a
-        let b' := (← get).fvarSubst.apply b
-        if a != a' || b != b' then
-          unify a' b'
-        else
-          return false
-
-end Unify
-
-private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option FVarSubst) := do
-  trace[Meta.Match.unify] "altFVarDecls: {altFVarDecls.map fun d => d.userName}, {a} =?= {b}"
-  let a ← instantiateMVars a
-  let b ← instantiateMVars b
-  let (r, s) ← Unify.unify a b { altFVarDecls := altFVarDecls} |>.run {}
-  if r then
-    return s.fvarSubst
-  else
-    trace[Meta.Match.unify] "failed to unify{indentExpr a}\nwith{indentExpr b}"
-    return none
-
 private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=
   withExistingLocalDecls alt.fvarDecls do
     trace[Meta.Match.unify] "expandVarIntoCtor? fvarId: {mkFVar fvarId}, ctorName: {ctorName}, alt:\n{← alt.toMessageData}"
@@ -357,27 +285,23 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) :
     let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType
     let ctor := mkAppN (mkConst ctorName ctorLevels) ctorParams
     let ctorType ← inferType ctor
-    -- TODO: try to rewrite this code using metavariables using `isDefEq` instead of `unify?`, and then
-    -- convert unassigned metavariables to fresh free variables.
-    -- Reason: `unify?` is too buggy
-    forallTelescopeReducing ctorType fun ctorFields resultType => do
-      let ctor := mkAppN ctor ctorFields
+    let ctorAbst? ← withNewMCtxDepth do
+      let (ctorFields, _, resultType) ← forallMetaTelescopeReducing ctorType
+      unless (← isDefEq resultType expectedType) do
+        return none
+      return some (← abstractMVars (mkAppN ctor ctorFields))
+    let some ctorAbst := ctorAbst? | return none
+    lambdaTelescope ctorAbst.expr fun newFVars ctor => do
+      let ctorArgs := ctor.getAppArgs
+      let ctorFields := ctorArgs[ctorParams.size:].toArray
       let alt  := alt.replaceFVarId fvarId ctor
-      let ctorFieldDecls ← ctorFields.mapM fun ctorField => ctorField.fvarId!.getDecl
-      let newAltDecls := ctorFieldDecls.toList ++ alt.fvarDecls
-      trace[Meta.Match.unify] "expandVarIntoCtor? {mkFVar fvarId} : {expectedType}, ctor: {ctor}, resultType: {resultType}"
-      let subst? ← unify? newAltDecls resultType expectedType
-      match subst? with
-      | none       => return none
-      | some subst =>
-        let newAltDecls := newAltDecls.filter fun d => !subst.contains d.fvarId -- remove declarations that were assigned
-        let newAltDecls := newAltDecls.map fun d => d.applyFVarSubst subst -- apply substitution to remaining declaration types
-        let patterns    := alt.patterns.map fun p => p.applyFVarSubst subst
-        let rhs         := subst.apply alt.rhs
-        let ctorFieldPatterns := ctorFields.toList.map fun ctorField => match subst.get ctorField.fvarId! with
-          | e@(.fvar fvarId) => if inLocalDecls newAltDecls fvarId then .var fvarId else .inaccessible e
-          | e                => .inaccessible e
-        return some { alt with fvarDecls := newAltDecls, rhs := rhs, patterns := ctorFieldPatterns ++ patterns }
+      let newAltDecls ← newFVars.mapM fun newFVar => newFVar.fvarId!.getDecl
+      let newAltDecls := newAltDecls.toList ++ alt.fvarDecls
+      trace[Meta.Match.unify] "expandVarIntoCtor? {mkFVar fvarId} : {expectedType}, ctor: {ctor}"
+      let ctorFieldPatterns := ctorFields.toList.map fun ctorField => match ctorField with
+        | .fvar fvarId => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible ctorField
+        | _            => Pattern.inaccessible ctorField
+      return some { alt with fvarDecls := newAltDecls, patterns := ctorFieldPatterns ++ alt.patterns }
 
 private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
   let xType ← inferType x
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index f6a7ba6eb3..8310742c55 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -240,108 +240,3 @@ default
 
 -- set_option trace.Meta.Match.match true
 -- set_option trace.Meta.Match.debug true
-
-#eval test `ex6 2 `elimTest6
--- #print elimTest6
-
-def ex7 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil))
-× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-default
-
-#eval test `ex7 2 `elimTest7
--- #check elimTest7
-
-def isSizeOne {n : Nat} (xs : Vec Nat n) : Bool :=
-elimTest7 _ (fun _ _ => Bool) n xs (fun _ => true) (fun _ _ => false)
-
-#eval isSizeOne Vec.nil
-#eval isSizeOne (Vec.cons 1 Vec.nil)
-#eval isSizeOne (Vec.cons 2 (Vec.cons 1 Vec.nil))
-
-def singleton? {n : Nat} (xs : Vec Nat n) : Option Nat :=
-elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none)
-
-#eval singleton? Vec.nil
-#eval singleton? (Vec.cons 10 Vec.nil)
-#eval singleton? (Vec.cons 20 (Vec.cons 10 Vec.nil))
-
-def ex8 (α : Type u) (n : Nat) (xs : Vec α n) :
-  LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil)))
-× LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) :=
-default
-
-#eval test `ex8 2 `elimTest8
-#print elimTest8
-
-def pair? {n : Nat} (xs : Vec Nat n) : Option (Nat × Nat) :=
-elimTest8 _ (fun _ _ => Option (Nat × Nat)) n xs (fun a b => some (a, b)) (fun _ _ => none)
-
-#eval pair? Vec.nil
-#eval pair? (Vec.cons 10 Vec.nil)
-#eval pair? (Vec.cons 20 (Vec.cons 10 Vec.nil))
-
-inductive Op : Nat → Nat → Type
-| mk : ∀ n, Op n n
-
-#print Op
-
-inductive Foo : Bool → Prop
-| bar : Foo false
-| baz : Foo false
-
-def ex10 (x : Bool) (y : Foo x) :
-  LHS (Pat (inaccessible false) × Pat Foo.bar)
-× LHS (forall (x : Bool) (y : Foo x), Pat (inaccessible x) × Pat y) :=
-default
-
-#eval test `ex10 2 `elimTest10 true
-
-
-def ex12 (x y z : Bool) :
-  LHS (forall (x y : Bool), Pat x × Pat y    × Pat true)
-× LHS (forall (x z : Bool), Pat false × Pat true × Pat z)
-× LHS (forall (y z : Bool), Pat true × Pat false × Pat z) :=
-default
-
-#eval testFailure `ex12 3 `elimTest12 -- should produce error message
-
-def ex14 (x y : Nat) :
-  LHS (Pat (val 1) × Pat (val 2))
-× LHS (Pat (val 2) × Pat (val 3))
-× LHS (forall (x y : Nat), Pat x × Pat y) :=
-default
-
--- set_option trace.Meta.Match true
-
-#eval test `ex14 2 `elimTest14
-#print elimTest14
-
-def h2 (x y : Nat) : Nat :=
-elimTest14 (fun _ _ => Nat) x y (fun _ => 0) (fun _ => 1) (fun x y => x + y)
-
-#eval check (h2 1 2 == 0)
-#eval check (h2 1 4 == 5)
-#eval check (h2 2 3 == 1)
-#eval check (h2 2 4 == 6)
-#eval check (h2 3 4 == 7)
-
-def ex15 (xs : Array (List Nat)) :
-  LHS (forall (a : Nat), Pat (ArrayLit1 [a]))
-× LHS (forall (a b : Nat), Pat (ArrayLit2 [a] [b]))
-× LHS (forall (ys : Array (List Nat)), Pat ys) :=
-default
-
-#eval test `ex15 1 `elimTest15
--- #check elimTest15
-
-def h3 (xs : Array (List Nat)) : Nat :=
-elimTest15 (fun _ => Nat) xs
- (fun a   => a + 1)
- (fun a b => a + b)
- (fun ys  => ys.size)
-
-#eval check (h3 #[[1]] == 2)
-#eval check (h3 #[[3], [2]] == 5)
-#eval check (h3 #[[1, 2]] == 1)
-#eval check (h3 #[[1, 2], [2, 3], [3]] == 3)