Trouble with injective type families
Wolfgang Jeltsch
wolfgang-it at jeltsch.info
Wed Jul 5 00:21:04 UTC 2017
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
More information about the Glasgow-haskell-users
mailing list