| > | > instance G a b where | > | > data E a = EC b -- this line - the b is not in scope. | > | > wrap = EC | > | > unwrap (EC b) = b | > | | > | I get "Not in scope: type variable `b'". | > | > That's a bug. b should be in scope I was wrong. It's not a bug. E is supposed to be a type *function*, so it can't mention anything on the RHS that is not bound on the LHS. We'll improve the documentation. | Ahh, cool. I which case I wonder if this too is a bug? : | | data Nil = Nil | data Cons :: * -> * -> * where | Cons :: val -> tail -> Cons val tail | | class F c v t | c -> v t where | data FD c t :: * | | instance F (Cons v t) v t where | -- this blows up with "conflicting definitions for `t'" | data FD (Cons v t) t = FDC v As I said, associated types are an *alternative* to fundeps. We have not even begun to think about what happens if you use both of them together. You should not need to do so. | Somehow I doubt it, but is the following any less suspicious? | | class F a b where | type BThing a :: * | data FD a :: * | wrap :: b -> FD a | unwrap :: FD a -> b | | instance F a b where | type BThing a = b | data FD a = FDC (BThing a) | wrap b = FDC b | unwrap (FDC b) = b | | Incidentally, that "type BThing a = b" line also blows up with | "Not in scope: type variable `b'". No, that is wrong in the same way as before. BThing is a *function* so its results must depend only on its arguments. S