def Main =
block
v = First
A = Accept
B = Accept
case v of
C -> Accept
We infer the following incorrect type for it:
test.Main ?a0 (HasUnion test.Main2 C ?a0) : Grammar test.Main =
do (v : test.Main2) <- Choose biased
{ {- A -} do (_2 : {}) <- pure {}
pure {A: _2}
| {- B -} do (_3 : {}) <- pure {}
pure {B: _3}
}
case v is
{ {| C = _ |} -> {- case branch {| C = _ |} -} pure {}
}
pure {v = v}
This is because we have a constructor that only appears in a pattern, but not in an actual constructor.
We could fix this by generating 3 constructors, but it is probably better to just reject such programs, as there is no reason
to match on a constructor that is never created.
Consider this example:
We infer the following incorrect type for it:
This is because we have a constructor that only appears in a pattern, but not in an actual constructor.
We could fix this by generating 3 constructors, but it is probably better to just reject such programs, as there is no reason to match on a constructor that is never created.