type aliases and Id

[Simon Peyton-Jones]

| 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