Non-Injective Closed Type Family

Question

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?

score 4 · Accepted Answer · edited Jan 24 '22 at 16:22

4

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.

edited Jan 24 '22 at 16:22

Sridhar Ratnakumar

81,433
63
146
187

answered Sep 28 '18 at 03:40

Li-yao Xia

31,896
2
33
56

I only want to add that, in my limited experience, injective type families never solved any problem I expected them to solve ;-). Perhaps the OP's is one of those cases where they work. I recall that some trivial examples like `f :: F a ~ F b => a -> b ; f x = x` surprisingly fail to work since injectivity is not fully exploited during type checking. – chi Sep 28 '18 at 19:51
@chi Unfortunately, you're right that it seems GHC still doesn't accept my type as injective even with an explicit annotation. However, this does answer my question, so thank you both for the help! :) – Silvio Mayolo Sep 29 '18 at 01:58

Non-Injective Closed Type Family

1 Answers1

Linked