GADTs and fundeps

[Simon Peyton-Jones]

Bjorn

You are quite right.  Indeed GADTs don't interact properly with type
classes at all, let alone functional dependencies, I'm afraid.   I
decided to pause and release before attending to this; it's not trivial
to do it right.

One merit of pausing is that I can collect examples that people actually
trip over, and make sure they work.  Would you like to file a
SourceForge bug, so that your code gets preserved there?

The more people that tell us they've tripped over something in GHC, the
more likely it is that we'll do something about it -- so keep telling
us.

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org
[mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Bjorn Bringert
| Sent: 06 April 2005 17:22
| To: glasgow-haskell-users at haskell.org
| Subject: GADTs and fundeps
| 
| 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
| 
| 
| 
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users