我能证明 (forall x. Coercible (a x) (b x)) 蕴含 Coercible a b 吗？

Question

我正在处理强制证明：

data a ~=~ b where
  IsCoercible :: Coercible a b => a ~=~ b
infix 0 ~=~

sym :: (a ~=~ b) -> (b ~=~ a)
sym IsCoercible = IsCoercible

instance Category (~=~) where 
  id = IsCoercible
  IsCoercible . IsCoercible = IsCoercible

coerceBy :: a ~=~ b -> a -> b
coerceBy IsCoercible = coerce

我可以简单证明Coercible a b => forall x. Coercible (a x) (b x)

introduce :: (a ~=~ b) -> (forall x. a x ~=~ b x)
introduce IsCoercible = IsCoercible

但不是相反，(forall x. Coercible (a x) (b x)) => Coercible a b) 并不完全免费：

eliminate :: (forall x. a x ~=~ b x) -> (a ~=~ b)
eliminate IsCoercible = IsCoercible
{-
   • Could not deduce: Coercible a b
        arising from a use of ‘IsCoercible’
      from the context: Coercible (a x0) (b x0)
        bound by a pattern with constructor:
                   IsCoercible :: forall k (a :: k) (b :: k).
                                  Coercible a b =>
                                  a ~=~ b,
                 in an equation for ‘eliminate’
-}

我相当肯定我的主张是有效的（尽管我愿意被反驳），但我没有任何关于如何在 Haskell 中证明它的好主意，而不是 unsafeCoerce。

Answer 1

不，你不能。正如 Dominique Devriese 和 HTNW 在他们的 cmets 中所暗示的那样，GHC 根本不承认这种推论。这个要求更高的版本无法编译：

{-# language QuantifiedConstraints, RankNTypes #-}

import Data.Coerce
import Data.Type.Coercion

eliminate :: (forall a. Coercible (f a) (g a)) => Coercion f g
eliminate = Coercion

你的版本更注定失败。要对多态 Coercion（或 ~=~）参数进行模式匹配，必须将其实例化为特定类型。 GHC 会将它实例化为f Any ~=~ g Any，然后它是单态的，因此不能证明你想要它做什么。由于 GHC Core 是类型化的，所以不会飞。

旁注：没有办法写作让我感到非常沮丧

f :: (forall a. c a :- d a)
  -> ((forall a. c a => d a) => r)
  -> r