Haskell：组合存在量词和通用量词意外失败

Question

[我正在尝试使用GHC版本8.6.5在Haskell中建模以下逻辑含义：

（（a.¬Φ（a））→¬（a：Φ（a））] >>

我使用的定义如下：

{-# LANGUAGE RankNTypes, GADTs #-}

import Data.Void

-- Existential quantification via GADT
data Ex phi where
  Ex :: forall a phi. phi a -> Ex phi

-- Universal quantification, wrapped into a newtype
newtype All phi = All (forall a. phi a)

-- Negation, as a function to Void
type Not a = a -> Void

-- Negation of a predicate, wrapped into a newtype
newtype NotPred phi a = NP (phi a -> Void)

-- The following definition does not work:
theorem :: All (NotPred phi) -> Not (Ex phi)
theorem (All (NP f)) (Ex a) = f a
[这里，GHC拒绝执行theorem，并显示以下错误消息：

* Couldn't match type `a' with `a0'
  `a' is a rigid type variable bound by
    a pattern with constructor:
      Ex :: forall a (phi :: * -> *). phi a -> Ex phi,
    in an equation for `theorem'
    at question.hs:20:23-26
* In the first argument of `f', namely `a'
  In the expression: f a
  In an equation for `theorem': theorem (All (NP f)) (Ex a) = f a
* Relevant bindings include
    a :: phi a (bound at question.hs:20:26)
    f :: phi a0 -> Void (bound at question.hs:20:18)
我真的不明白为什么GHC不能匹配这两种类型。以下解决方法会编译：

theorem = flip theorem' where
    theorem' (Ex a) (All (NP f)) = f a
对我来说，theorem的两个实现是等效的。为什么GHC只接受第二个？ 

[我正在尝试使用GHC版本8.6.5在Haskell中对以下逻辑含义进行建模：（∀a。Φ（a））→¬（∃a：Φ（a））我使用的定义如下： ...

Answer 1

[将模式All prf与类型All phi的值匹配时，prf被提取为类型forall a. phi a的多态实体。在这种情况下，您会得到一个no :: forall a. NotPred phi a。但是，您不能对这种类型的对象执行模式匹配。毕竟，它是一个从类型到值的函数。您需要将其应用于特定类型（称为_a），然后您会得到no @_a :: NotPred phi _a，现在可以将其匹配以提取f :: phi _a -> Void。如果您扩展定义...