[GHC] #345: GADT - fundep interaction

[GHC]

#345: GADT - fundep interaction
--------------------------------------+-------------------------------------
  Reporter:  bring                    |          Owner:  simonpj 
      Type:  bug                      |         Status:  assigned
  Priority:  normal                   |      Milestone:  6.8     
 Component:  Compiler (Type checker)  |        Version:  6.4     
  Severity:  normal                   |     Resolution:  None    
  Keywords:                           |             Os:  Unknown 
Difficulty:  Unknown                  |   Architecture:  Unknown 
--------------------------------------+-------------------------------------
Changes (by simonpj):

  * architecture:  => Unknown
  * difficulty:  => Unknown
  * milestone:  => 6.8
  * os:  => Unknown

Old description:

> {{{
> 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)
> -}
> }}}

New description:

 {{{
 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)
 -}
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/345>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler