GADT - fundep interaction

[bring]

GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used to figure out the result type. 

{-# OPTIONS_GHC -fglasgow-exts #-}

data Succ n
data Zero

class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)

infixr 5 :::

data List :: * -> * -> * where
              Nil :: List a Zero
              (:::) :: a -> List a n -> List a (Succ n)

append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys

{-
  GHC 6.4 says:

    Couldn't match the rigid variable `y' against `Succ z'
      `y' is bound by the type signature for `append'
      Expected type: List a y
      Inferred type: List a (Succ z)
    In the expression: x ::: (append xs ys)
    In the definition of `append': append (x ::: xs) ys
= x ::: (append xs ys)
-}

[simonpj]

This one still doesn't work, even with the new implication-constraint machinery. It's a good example of the need for full-on equality constraints.

Simon

[jyrinx]

GHC doesn't even like the first clause nowadays. Sez version 6.7.20070224:

    Couldn't match expected type `z' (a rigid variable)
           against inferred type `y' (a rigid variable)
      `z' is bound by the type signature for `append' at Bug345.hs:16:19
      `y' is bound by the type signature for `append' at Bug345.hs:16:17
      Expected type: List a z
      Inferred type: List a y
    In the expression: ys
    In the definition of `append': append Nil ys = ys

(I did have to compile with -fallow-undecidable-instances, though.)

[simonpj]

See also #1573, which gives another example.

I plan to fix this by the upcoming work on indexed type families. Tom Schrivjers has built a prototype implementation, which mostly works. I need to review and commit it. Stay tuned.

Simon

[igloo]

Simon PJ will look at this in the HEAD, after 6.8 is forked.

[simonpj]

To clarify, my intention is that we'll solve it with type functions, which will play nice with GADTs. I'm not sure fundeps ever will.

Simon

[chak]

The corresponding problem in the type families world has now been fixed - eg #1723. I am unsure what the intention with this bug is. Close it, and tell people to use type families? Wait until FDs are being implemented by way of type families?

[simonpj]

Ultimately, I think we can implement fundeps using type families, and then the fundep version will work too. Until then, it'll only work in type-family form.

So, since we now have a good workaround (well, actually, a better way to write the program rather than a workaround), I'll leave it open, but at low priority and with milestone bottom.

Simon