title: Why is this injective type family not actually injective?
body: <p>I tried this:</p>
  
  <pre><code>{-# LANGUAGE TypeFamilyDependencies #-}
  module Injective where
  
  type family F (a :: *) = (fa :: *) | fa -&gt; a
  
  convert :: F a ~ F b =&gt; a -&gt; b
  convert x = x
  </code></pre>
  
  <p>GHC 8.6.4 gave me this error</p>
  
  <pre><code>    • Could not deduce: a ~ b
        from the context: F a ~ F b
          bound by the type signature for:
                     convert :: forall a b. (F a ~ F b) =&gt; a -&gt; b
          at Injective.hs:6:1-30
  </code></pre>
  
  <p>Why? Surely the whole point of injectivity is that one <em>can</em> deduce <code>a ~ b</code> from <code>F a ~ F b</code>?</p>