type aliases and Id

[Iavor Diatchki]

Hello,

On 3/19/07, Lennart Augustsson <lennart at augustsson.net> wrote:
> Ravi,
>
> Ganesh and I were discussing today what would happen if one adds Id
> as a primitive type constructor.  How much did you have to change the
> type checker?  Presumably if you need to unify 'm a' with 'a' you now
> have to set m=Id.  Do you know if you can run into higher order
> unification problems?  My gut feeling is that with just Id, you
> probably don't, but I would not bet on it.

It seems to me that even with just ''Id'' the problem is tricky.
Suppose, for example, that we need to solve ''f x = g y''.  In the
present system we can reduce this to ''f = g'' and ''x = y'''.
However, if we had ''Id'', then we would have to delay this equation
until we know more about the variables that are involved (e.g., the
correct solution might be ''f = Id'' and ''x = g y'').

-Iavor