GADTs and fundeps
Bjorn Bringert
d00bring at dtek.chalmers.se
Wed Apr 6 12:21:41 EDT 2005
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. This does not seem to
work, or am I doing something stupid?
/Bjorn
{-# 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)
{-
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)
-}
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
More information about the Glasgow-haskell-users
mailing list