your type checker seems too young

[thautwarm]

Please check the most difficult project I've finished in github:
https://github.com/thautwarm/reFining/blob/master/DotNet/reFining/reFining/infr.fs

I can solve the problem you ask in QQ recently about value restrictions.

The tests indicates something meaningful:
https://github.com/thautwarm/reFining/blob/master/DotNet/reFining/test/Tests.fs

Above project is side-effect free, so I think I might get along with Haskell as well.
May I take part in this project to work with the type checkers?

[ice1000]

I can solve the problem you ask in QQ recently about value restrictions.

You mean refinement type? That'll be the greatest high!

May I take part in this project to work with the type checkers?

Yes, Yes, Yes!

Writing down some gossips:

Currently I plan to create a type system based on UTT (which has no difference with MLTT IMO -- imagine a Haskell type system with dependent type). With refinement type, we can make a better termination check.
Also, we can rewrite easier with refinement type. Imagine this Idris code:

b : bla = rua
c : rua = ora
a = rewrite b in rewrite c in Refl

Looks so ugly, hugh? In a language with refinement type we can simply

val b : x:unit{bla = rua}
val c : x:unit{rua = ora}
a = b; c; ()
(* A simplified version of let () = b in let () = c in () *)

Making the code extremely readable!

[ice1000]