The compilation of list regexes is buggy.

For example, [ (t1 | t2)* ] is interpreted as [ t1 t2*]

Currently, the gradual type is nothing but a type constant, i.e. it is a subtype only of itself and Any (and a supertype only of itself and Emply), which makes it rather useless

An expression such as if e || e' then e1 else e2 should be rewritten to if e then e1 else if e' then e1 else e2 (and likewise for other boolean connectives).

This allows the type-checker to detect more cases where it can refine without complicating it too much.

Currently, a Failure exception is raised.
This should be rewritten to use the same writer monad as the typechecking, so that errors aren't fatal and we also can raise warnings.

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.

Currently { x /*: Int */ ? 1 }:x is valid, while { x ? 1 /*: Int */ } isn't. Imho, both should be valid.

Proposal : give them different typing semantics:

• { x /*: τ */ ? c }:x : {x=τ} → (τ | B(c))
• { x ? c /*: τ */ } : {x=τ} → τ if B(c) ≤ τ

(ie require only in the second case that the default value has the annotated type).

This makes the behaviour slightly more complex, but remains quite logical and allows distinguishing the case where the argument is not given, which isn't possible to do as directly now:

{ x /*: Int */ ? true }:
if x == true then
  "x wasn't defined"
else
  "x was defined, with value ${x}"

{ x }@x: x should raise an error but currently doesn't