Why is this injective type family not actually injective?

Question

I tried this:

{-# LANGUAGE TypeFamilyDependencies #-}
module Injective where

type family F (a :: *) = (fa :: *) | fa -> a

convert :: F a ~ F b => a -> b
convert x = x

GHC 8.6.4 gave me this error

    • 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) => a -> b
        at Injective.hs:6:1-30

Why? Surely the whole point of injectivity is that one can deduce a ~ b from F a ~ F b?

Answer 1

It turns out this is a known issue in GHC. Apparently it's because it hasn't been proven sound.