On Wed, Dec 11, 2013 at 10:29 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:

Hello,

I am pleased to release the first version of InvarGenT, a system that performs full type inference for a type system with GADTs, and also generates new GADTs to serve as existential types. In addition to algebraic types, the first version handles linear arithmetic constraints.

https://github.com/lukstafi/invargent/releases/tag/v1.0

Regards,
Łukasz Stafiniak

Bug fix: the remark in the manual about `let..in` as syntactic sugar is erroneous, ignore it. 'let..in' nodes differ from beta-redexes in that the former can be used for existential type elimination.