为什么这个内射型家庭实际上不是内射型？

Question

我尝试了这个：

{-# 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给了我这个错误

    • 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

为什么？当然，单射性的全部要点是可以从中推论a ~ b得出F a ~ F b吗？

Answer 1

事实证明这是GHC 中的一个已知问题。显然这是因为它尚未被证明是正确的。