type aliases and Id

[oleg at pobox.com]

Lennart Augustsson wrote:
> 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.

I wonder if this proposal is a good idea.

Let us consider the following near-Haskell98 code

> class C a
> instance C (m a) 
> instance C Int

(usually there will be constraints on m. We shall see a useful example of
this in a moment). This code typechecks under slight and common
relaxation of the rules on the form of instance head. That example
will probably typecheck in Haskell'.
Under the proposal that Id t === t, typechecking
of this code will require overlapping instances, which quite unlikely to
make it into Haskell' and is a quite significant and controversial 
extension.

Speaking of overlapping instances, let's generalize the example to

> class C a
> instance C (m a) 
> instance C a

It does typecheck in current Haskell. Under the Id proposal, this
example will NOT typecheck, ever. This is because the two instances
become exact duplicates. Indeed, every type that matches "a" will
match "m a" (with m = Id) and vice versa. The two instances match the
same class of types (that is, all of the types).

Let us come back to our simple example and make it practical. 

> class C a where incr :: a -> a
>
> instance (C a, Functor m) => C (m a) where incr = fmap incr
> instance C Int where incr = succ
>
> test = incr (Just [[[1::Int]]])

the example increments integers deeply embedded in some functorial
data structures. The operations of this kind are requested from time
to time on Haskell-Cafe. This code compiles and works (no overlapping
or undecidable instances are required). Under the Id t === t
proposal, this example will diverge (perhaps, it will diverge even in
the compiler). The reason is that the base case cannot be reached; the
type Int can always be considered as Id Int and so the first instance
will apply again.