Multiple match cases trigger

match_repro.lean

inductive Term : Type
| const : Nat -> Term
| app   : List Term -> Term

namespace Term
instance : Inhabited Term := ⟨Term.const 0⟩
partial def hasToString : Term -> String | (const n) := "[CONST]" | (app ts)  := "[APP]"
instance : HasToString Term := ⟨hasToString⟩
end Term

open Term

structure MyState : Type := (ts : List Term)

partial def foo : MyState -> Term -> List Term
| ms₀ t :=
  -- Also: why doesn't this print?
  -- let foo := dbgTrace ("t: " ++ toString t ) id;

  -- Both branches fire!
  -- But, it seems that if we ever trace 't', only the right branch fires.
  let stateT : State MyState Unit :=
    match t with
    | const n => dbgTrace "CONST" pure
    | app ts  => dbgTrace "APP" pure ;

  (stateT.run ⟨[]⟩).2.ts

def main : IO Unit := IO.println $ foo ⟨[]⟩ (app [])