[Iceland_jack]

With https://ucsd-progsys.github.io/liquidhaskell/, but as a separate checker. I think there are talks of integrating it into the compiler