I have this admittedly contrived chunk of code
{-# LANGUAGE DataKinds, TypeFamilies #-}
data Foo = Foo
type family Id (n :: Foo) a where
Id 'Foo a = a
data Bar (n :: Foo) = Bar
class Dispatch (n :: Foo) where
consume :: Id n a -> Bar n -> a
consume' :: Dispatch n => Id n [Bool] -> Bar n -> [Bool]
consume' = consume
consume'' :: Dispatch n => Id n [Bool] -> Bar n -> Bool
consume'' g x = and (consume' g x)
This compiles and works fine. However, if I replace the final consume'' definition with
consume'' :: Dispatch n => Id n [Bool] -> Bar n -> Bool
consume'' g x = and (consume g x)
(Note the consume rather than consume'), then I get an error
noinject.hs:17:30: error:
• Couldn't match expected type ‘Id n (t0 Bool)’
with actual type ‘Id n [Bool]’
NB: ‘Id’ is a non-injective type family
The type variable ‘t0’ is ambiguous
• In the first argument of ‘consume’, namely ‘g’
In the first argument of ‘and’, namely ‘(consume g x)’
In the expression: and (consume g x)
• Relevant bindings include
x :: Bar n (bound at noinject.hs:17:13)
g :: Id n [Bool] (bound at noinject.hs:17:11)
consume'' :: Id n [Bool] -> Bar n -> Bool
(bound at noinject.hs:17:1)
|
17 | consume'' g x = and (consume g x)
| ^
Failed, no modules loaded.
If we assume Id is non-injective, then the error occurs because consume could feasibly specialize to consume :: Id n (t0 Bool) -> Bar n -> t0 Bool, for some foldable t0 that isn't []. I understand that much. My question is: why is Id not actually injective. It takes two arguments: there's only one valid value for the first argument, and Id is pretty clearly injective in its second argument, so why does GHC think this is a non-injective family?
Injective type families are a separate extension on top of type families, and you need special syntax to declare a type family as one. Injectivity does not get inferred.