Почему эта семья инъективного типа на самом деле не инъективна?

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 . Видимо, потому, что это не было доказано.