Correct README to README.md in the cabal file, and add freshenAndFree

[UnkindPartition]

trafficstars

[UnkindPartition]

I pushed a second, independent commit (let me know if you'd like me to split this into separate PRs).

Hopefully the haddock there is self-explanatory. I've always assumed that freshen/freshenAll "took care" of variable capture, and today I learn that it doesn't, so I added a function that does.

[wrengr]

Sorry for the slow turn around. I'll take a look at the second patch and get back to you soon

[wrengr]

I'm not sure I like freshenAndFree (the way it's currently phrased), because it seems to rely on breaking the abstraction boundary. That is, unification variables should never "escape"; and writing them to a file lets them escape, hence the issues you mention in the haddock. This is a big part of why there's no Read (UTerm t v) instance. Depending on the details of your use case I see a few alternative ways forward.

The simplest option (from the library's perspective :) would be to augment your data type to include type variables, and then convert those into unification variables during/after parsing the interface files.

Or, equivalently, you can treat the saved UTerms as if they were such an augmented datatype. That is, when parsing interface files, instead of treating the parsed UVar as if it were a real UVar, you should treat it as a type variable and allocate a fresh unification variable to represent it (keeping a map from these serialized type variables to their associated unification variables). This approach is basically just the generic version of the first one, since augmenting Fix (i.e., the result of freeze) with a constructor for type variables would look isomorphic to UTerm.

A variation on that DIY approach would be to have the interface files actually be Haskell programs: that way you can explicitly call freeVar to allocate the unification variables used therein.

As far as library support, I think the best option would be to have functions to explicitly transport terms and bindings from one BindingMonad to another. This would allow to preserve sharing, and would enable a bunch of other use cases. I'll see if I can whip up an implementation of this over the weekend.