| 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. | | Having Id would be cool. If we make an instance 'Monad Id' it's now | possible to get rid of map and always use mapM instead. Similarly | with other monadic functions. I remember that I have, more than once, devoted an hour or two to the question "could one add Id as a distinguished type constructor to Haskell". Sadly, each time I concluded "no". I'm prepared to be proved wrong. But here's the difficulty. Suppose we want to unify (m a) with (Tree Int) At the moment there's no problem: m=Tree, a=Int. But with Id another solution is m=Id, a=Tree Int And there are more m=Id, a=Id (Tree Int) We don't know which one to use until we see all the *other* uses of 'm' and 'a'. I have no clue how to solve this problem. Maybe someone else does. I agree that Id alone would be Jolly Useful, even without full type-level lambdas. Simon