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.
Reproducing the behavior
The following program type-checks when it shouldn't
We expected a "can't unify (Unit, Nat) with (Nat, Nat_)" error.
System Settings
Bend commit 71fb680
Additional context
No response