Hi! Injective type families as supported by GHC 8.0.1 do not behave like I would expect them to behave from my intuitive understanding.
Let us consider the following example: > {-# LANGUAGE RankNTypes, TypeFamilyDependencies #-} > > class C a where > > type T a = b | b -> a > > instance C Bool where > > type T Bool = Int > > type X b = forall a . T a ~ b => a > > x :: X Int > x = False I would expect this code to be accepted. However, I get the following error message: > A.hs:14:5: error: > • Could not deduce: a ~ Bool > from the context: T a ~ Int > bound by the type signature for: > x :: T a ~ Int => a > at A.hs:13:1-10 > ‘a’ is a rigid type variable bound by > the type signature for: > x :: forall a. T a ~ Int => a > at A.hs:11:19 > • In the expression: False > In an equation for ‘x’: x = False > • Relevant bindings include x :: a (bound at A.hs:14:1) This is strange, since injectivity should exactly make it possible to deduce a ~ Bool from T a ~ Int. Another example is this: > {-# LANGUAGE GADTs, TypeFamilyDependencies #-} > > class C a where > > type T a = b | b -> a > > instance C Bool where > > type T Bool = Int > > data G b where > > G :: Eq a => a -> G (T a) > > instance Eq (G b) where > > G a1 == G a2 = a1 == a2a I would also expect this code to be accepted. However, I get the following error message: > B.hs:17:26: error: > • Could not deduce: a1 ~ a > from the context: (b ~ T a, Eq a) > bound by a pattern with constructor: > G :: forall a. Eq a => a -> G (T a), > in an equation for ‘==’ > at B.hs:17:5-8 > or from: (b ~ T a1, Eq a1) > bound by a pattern with constructor: > G :: forall a. Eq a => a -> G (T a), > in an equation for ‘==’ > at B.hs:17:13-16 > ‘a1’ is a rigid type variable bound by > a pattern with constructor: G :: forall a. Eq a => a -> G (T a), > in an equation for ‘==’ > at B.hs:17:13 > ‘a’ is a rigid type variable bound by > a pattern with constructor: G :: forall a. Eq a => a -> G (T a), > in an equation for ‘==’ > at B.hs:17:5 > • In the second argument of ‘(==)’, namely ‘a2’ > In the expression: a1 == a2 > In an equation for ‘==’: (G a1) == (G a2) = a1 == a2 > • Relevant bindings include > a2 :: a1 (bound at B.hs:17:15) > a1 :: a (bound at B.hs:17:7) If b ~ T a and b ~ T a1, then T a ~ T a1 and subsequently a ~ a1, because of injectivity. Unfortunately, GHC does not join the two contexts (b ~ T a, Eq a) and (b ~ T a1, Eq a1). Are these behaviors really intended, or are these bugs showing up? All the best, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users