title: Non-Injective Closed Type Family
body: <p>I have this admittedly contrived chunk of code</p>
  
  <pre><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 -&gt; Bar n -&gt; a
  
  consume' :: Dispatch n =&gt; Id n [Bool] -&gt; Bar n -&gt; [Bool]
  consume' = consume
  
  consume'' :: Dispatch n =&gt; Id n [Bool] -&gt; Bar n -&gt; Bool
  consume'' g x = and (consume' g x)
  </code></pre>
  
  <p>This compiles and works fine. However, if I replace the final <code>consume''</code> definition with</p>
  
  <pre><code>consume'' :: Dispatch n =&gt; Id n [Bool] -&gt; Bar n -&gt; Bool
  consume'' g x = and (consume g x)
  </code></pre>
  
  <p>(Note the <code>consume</code> rather than <code>consume'</code>), then I get an error</p>
  
  <pre><code>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] -&gt; Bar n -&gt; Bool
            (bound at noinject.hs:17:1)
     |
  17 | consume'' g x = and (consume g x)
     |                              ^
  Failed, no modules loaded.
  </code></pre>
  
  <p>If we assume <code>Id</code> is non-injective, then the error occurs because <code>consume</code> could feasibly specialize to <code>consume :: Id n (t0 Bool) -&gt; Bar n -&gt; t0 Bool</code>, for some foldable <code>t0</code> that isn't <code>[]</code>. I understand that much. My question is: why is <code>Id</code> <em>not</em> actually injective. It takes two arguments: there's only one valid value for the first argument, and <code>Id</code> is pretty clearly injective in its second argument, so why does GHC think this is a non-injective family?</p>