The type of `x` should be refined in `if x = e0 then e1 else e2`
Closed this issue · 0 comments
thufschmitt commented
It should have at most the type of e0
in the "then" branch.
Furthermore, if e0
has a singleton type c
, then x
should have type not c
in the "else" branch.
For example, if x = 1 then x else 1
should have type 1
.