Carlo Angiuli

Can this lead to confusing situations where the distiller obscures why something isn't working? (Not objecting, just curious.)

I tried it out; it causes a bunch of the descriptions to wrap onto a second line, but otherwise looks fine, and doesn't actually change the page count of hott-ustrade....

I don't quite understand this proposal. What would a logic program look like, in that case? The underlying problem is that we still need fresh variables to be able to...

Oh, in that case, I agree. We will need GADTs in this case, and probably phantom types for fresh variables. (I don't really see the point of Data.Dynamic and Data.Typeable,...

Oh, I see. Looking deeper into `Data.Typeable`, it turns out that it is isomorphic to the solution I had in mind. I glanced at it previously and thought it was...

I really feel that we should be able to do that type check somehow. But yeah, maybe we should start by replacing the current hack with something closer to ideal,...

`Eq` distinguishes between them, though...? I still have misgivings about going down this path if it prevents the typechecker from noticing these issues.

> I think there may be some use in adding a phantom type to the `Var` constructor, then using some `Typeable` tricks to add types to the variables. This. Sorry...