fix: dependent pattern matching bug

closes #1279
Originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/case.20in.20dependent.20match.20not.20triggering.20.28.3F.29/near/288328239

src/Lean/Meta/Match/Match.lean

@@ -267,8 +267,58 @@ def assign (fvarId : FVarId) (v : Expr) : M Bool := do
       modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
       return true
     else
-      trace[Meta.Match.unify] "assign failed variable is not local, {mkFVar fvarId} := {v}"
-      return false
+      /-
+        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}"
@@ -289,6 +339,7 @@ partial def unify (a : Expr) (b : Expr) : M Bool := do
 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 {}
@@ -300,6 +351,7 @@ private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option
 
 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}"
     let expectedType ← inferType (mkFVar fvarId)
     let expectedType ← whnfD expectedType
     let (ctorLevels, ctorParams) ← getInductiveUniverseAndParams expectedType
@@ -310,6 +362,7 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) :
       let alt  := alt.replaceFVarId fvarId ctor
       let ctorFieldDecls ← ctorFields.mapM fun ctorField => getLocalDecl ctorField.fvarId!
       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

tests/lean/1279.lean

@@ -0,0 +1,87 @@
+inductive O
+| int
+| real
+| bool
+| unit
+deriving Inhabited, BEq, Repr
+
+-- only `Arrow.id` and `Arrow.comp` really matter for my problem
+inductive Arrow : (_dom _cod : O) → Type
+  -- identity
+  | id : {α : O} → Arrow α α
+
+  -- `α → α` arrows
+  | unit : Arrow O.unit O.unit
+  | not : Arrow O.bool O.bool
+  | succᵢ : Arrow O.int O.int
+  | succᵣ : Arrow O.real O.real
+
+  | comp {α β γ} : Arrow β γ → Arrow α β → Arrow α γ
+
+  -- `unit → bool`
+  | tru : Arrow O.unit O.bool
+  | fls : Arrow O.unit O.bool
+  -- `unit → int`
+  | zero : Arrow O.unit O.int
+  -- `int → bool`
+  | isZero : Arrow O.int O.bool
+  -- `int → real`
+  | toReal : Arrow O.int O.real
+deriving Repr
+
+def Arrow.compose₁ {α β γ : O} :
+  Arrow β γ
+  → Arrow α β
+  → Arrow α γ
+-- id.compose₁ g = g
+| id, g => g
+-- f.compose₁ id = f
+| f, id => f
+-- else
+| comp f₁ f₂, g => comp f₁ (comp f₂ g)
+| f, g => comp f g
+
+#print Arrow.compose₁
+-- def Arrow.compose₁ : {α β γ : O} → Arrow β γ → Arrow α β → Arrow α γ :=
+-- fun {α β γ} x x_1 =>
+--   match β, γ, x, x_1 with
+--   | β, .(β), Arrow.id, g => g
+--   | .(α), γ, f, Arrow.id => f
+--   | β, γ, Arrow.comp f₁ f₂, g => Arrow.comp f₁ (Arrow.comp f₂ g)
+--   | β, γ, f, g => Arrow.comp f g
+#eval Arrow.compose₁ Arrow.unit Arrow.id
+-- Arrow.comp (Arrow.unit) (Arrow.id) -- Error: it should be `Arrow.unit`
+
+example : Arrow.compose₁ .id .id         = (.id (α := o)) := rfl
+example : Arrow.compose₁ .id .unit       = .unit          := rfl
+example : Arrow.compose₁ .id (.comp f g) = .comp f g      := rfl
+example : Arrow.compose₁ .unit       .id = .unit := rfl
+example : Arrow.compose₁ (.comp f g) .id = .comp f g := rfl
+example : Arrow.compose₁ .unit .unit = .comp .unit .unit := rfl
+example : Arrow.compose₁ (.comp f g) .unit = .comp f (.comp g .unit) := rfl
+example : Arrow.compose₁ .unit (.comp f g) = .comp .unit (.comp f g) := rfl
+
+theorem ex_1 : Arrow.compose₁ f .id = f := by
+  cases f <;> simp!
+
+theorem ex_2 : Arrow.compose₁ f .id = f := by
+  cases f <;> simp!
+
+theorem ex_3 : Arrow.compose₁ .id f = f := by
+  cases f <;> simp!
+
+theorem ex_4 : h ≠ .id → Arrow.compose₁ (.comp f g) h = .comp f (.comp g h) := by
+  intros
+  cases h <;> simp_all!
+
+def Arrow.isId : Arrow dom com → Prop
+  | .id => True
+  | _ => False
+
+def Arrow.isComp : Arrow dom com → Prop
+  | .comp .. => True
+  | _ => False
+
+theorem ex_5 (f : Arrow β γ) (g : Arrow α β) : ¬ f.isId → ¬ g.isId → ¬ f.isComp → Arrow.compose₁ f g = .comp f g := by
+  intros
+  cases f <;> cases g <;> simp_all!

tests/lean/1279.lean.expected.out

@@ -0,0 +1,8 @@
+def Arrow.compose₁ : {α β γ : O} → Arrow β γ → Arrow α β → Arrow α γ :=
+fun {α β γ} x x_1 =>
+  match β, γ, x, x_1 with
+  | β, .(β), Arrow.id, g => g
+  | .(α), γ, f, Arrow.id => f
+  | β, γ, Arrow.comp f₁ f₂, g => Arrow.comp f₁ (Arrow.comp f₂ g)
+  | β, γ, f, g => Arrow.comp f g
+Arrow.unit

tests/lean/1279_simplified.lean

@@ -0,0 +1,13 @@
+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
+
+#eval Arrow.compose Arrow.unit Arrow.id

tests/lean/1279_simplified.lean.expected.out

@@ -0,0 +1 @@
+Arrow.unit