Type checking allows incorrect match term

[developedby]

Reproducing the behavior

The following program type-checks when it shouldn't

type Nat_:
  Zero
  Succ {x: Unit, pred: Nat_}

type Unit:
  Unit

Test1: Nat_ -> (Nat_, Nat_)
Test1 = λx match x {
  Nat_/Zero: (Nat_/Zero, Nat_/Zero)
  Nat_/Succ: (x.x, x.pred)
}

main = *

We expected a "can't unify (Unit, Nat_) with (Nat_, Nat_)" error.

System Settings

Bend commit 71fb680

Additional context

No response