oerjan

I had an idea purely in my mind last autumn of doing something like this with de Bruijn indices and a `Constraint`-returning continuation monad in the type system. Then I...

I initially implemented the new system's `ForallT` precisely as you suggest, but restricted it again because it broke one of the packages on Hackage. See [this pull request](https://github.com/ekmett/constraints/pull/16).

Gah. I still don't have a working Haskell environment, but unraveling the definitions a bit more by hand: `Forall (Pure (ReaderT () n))` requires expanding ``` StM (ReaderT () n)...

Or perhaps this less complicated function, which was (with a different implementation) in the provisional rewrite after `A`/`B` were shown broken and before adding Skolems: ``` forall :: forall p....