case in dependent match not triggering (?)

Stream: lean4

[Adrien Champion]

# on macos 12.4 (m1)
❯ lean -version
Lean (version 4.0.0-nightly-2022-07-02, commit a639eb185cab, Release)

I'm quite out of my depth here, I'm messing with dependent pattern matching and there's something I
just don't understand. Here's my non-minimal but small example.

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)

I really don't get why this #eval produces a comp and not Arrow.unit as per the second branch
of compose₁'s match. I guess I'm making a stupid, obvious mistake as that's what I usually do as
a noob, but I just can't see it.

[Adrien Champion]

In case it helps, my actual code is here

• https://github.com/AdrienChampion/experimentalean4/blob/04ad4ad283a270b1834e96828565b0eda15184d8/catFplIssue/Cat.lean

with slightly more context, and an Arrow.compose₂ with a more type-explicit match

[Leonardo de Moura]

This looks like a bug in the match compiler. I will take a look.

[Adrien Champion]

Not sure if that's useful, but when I try to prove the theorem compose_id I am interested in, I get this error when I simplify:

theorem Arrow.id_compose : Arrow.compose₁ id g = g :=
  by
    simp only [compose₁]
theorem Arrow.compose_id : Arrow.compose₁ f id = f :=
  by
    simp only [compose₁]
-- failed to generate equality theorems for `match` expression `Arrow.compose₁.match_1`
-- case unit
-- motive : (β γ : O) → Arrow β γ → Arrow O.unit β → Sort u_1
-- h_1 : (β : O) → (g : Arrow O.unit β) → motive β β id g
-- h_2 : (γ : O) → (f : Arrow O.unit γ) → motive O.unit γ f id
-- h_3 : (β γ β_1 : O) → (f₁ : Arrow β_1 γ) → (f₂ : Arrow β β_1) → (g : Arrow O.unit β) → motive β γ (comp f₁ f₂) g
-- h_4 : (β γ : O) → (f : Arrow β γ) → (g : Arrow O.unit β) → motive β γ f g
-- : O.unit = O.unit → HEq unit id → False
-- ⊢ h_4 O.unit O.unit unit id = h_2 O.unit unit

[Leonardo de Moura]

Pushed a fix for this issue: https://github.com/leanprover/lean4/commit/03ce7cb17ccdbbb1874654766a470c8816f3aa3d

[Adrien Champion]

Awesome, thanks :smiley_cat:

I'm not in a rush so I'll wait until it reaches nightly, unless you want me to confirm the problem is fixed in which case just let me know