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