GADTs and fundeps don't seem to interact in the waythat I (perhaps naively) expect. I expected that foreach case, the type variables would be instantiatedaccording to the type of the constructors, and then thefundep would be used to figure out the result type. {-# OPTIONS_GHC -fglasgow-exts #-}data Succ ndata Zeroclass Plus x y z | x y -> zinstance Plus Zero x xinstance 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 zappend Nil ys = ysappend (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)-}