[ ghc-Bugs-1179108 ] GADT - fundep interaction

[SourceForge.net]

Bugs item #1179108, was opened at 2005-04-08 10:02
Message generated for change (Settings changed) made by simonpj
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1179108&group_id=8032

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: Compiler (Type checker)
Group: 6.4
Status: Open
Resolution: None
Priority: 5
Submitted By: Bjorn Bringert (bring)
>Assigned to: Simon Peyton Jones (simonpj)
Summary: GADT - fundep interaction

Initial Comment:
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)
-}

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=108032&aid=1179108&group_id=8032