Hello,
On 3/19/07, Lennart Augustsson
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