Christophe Raffalli

Unification variable that remains after type-checking should get a default instanciation. Remark: if later we keep unification constraints, this would become very important as there could be unsolvable contraints, or...

Use unification variables parametrized by ordinals (mantis #57)

1

To do as in subml, we need this. It relies on higher-order ?

Only very simple cases are handled by Typing.is_singleton. Some quantification or Impl could be allowed.

managment of unification variable in equivalence Description (mantis #50)

1

The current implementation seems to work but should be checked. The risk is to loose some equivalence/normalisation propagation when a unification variable gets instanciated. HApp node are also concerned as...

There is a FIXME in the code ... Don't know what should be done Can add the equations that were proved for mu-abstraction and named terms: - contraction of mu-abstractions...

Would be nice to have a miltiprecision interval arithmetic too

1

May be based on gmp's mpfi ?

Constant variant types as a subtype of int

5

I would really be nice to allow (t :> int) when t is a variant type with only constant constructors. And in the same time to allow to choose the...

-opaque option breaks equivalence between release and dev compilation in presence of [@inline always]

10

## Expected Behavior dune build and dune build --release should both work or both fail ## Actual Behavior If the code contains [@inline always], dune build may fail with error...

Caqti forcing the use of Format which is thread unsafe

1

Caqti is forcing us to use Logs which in turn uses Format. But, - Format is slower than printf (around 70% slower) - More importantly, Format is thread unsafe and,...