Trouble with injective type families

[Wolfgang Jeltsch]

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