Haskell: Combining existential and universal quantifiers fails unexpectedly

Question

I am trying to model the following logical implication in Haskell with GHC, version 8.6.5:

(∀ a. ¬ Φ(a)) → ¬ (∃ a: Φ(a))

The definitions I used are the following:

{-# 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

Here, GHC rejects the implementation of the theorem with the following error message:

* 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)

I do not really understand why GHC shouldn't be able to match the two types. The following workaround compiles:

theorem = flip theorem' where
    theorem' (Ex a) (All (NP f)) = f a

To me, the two implementations of theorem are equivalent. Why does GHC only accept the second one?

Answer 1

When you match the pattern All prf against a value of type All phi, prf is extracted as a polymorphic entity of type forall a. phi a. In this case, you get a no :: forall a. NotPred phi a. However, you cannot perform pattern matching on an object of this type. After all, it's a function from types to values. You need to apply it to a specific type (call it _a), and you'll get no @_a :: NotPred phi _a, which now can be matched to extract a f :: phi _a -> Void. If you expand your definition...

{-# LANGUAGE ScopedTypeVariables #-}
-- type signature with forall needed to bind the variable phi
theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem prf wit = case prf of
    All no -> case no @_a of -- no :: forall a. NotPred phi a
        NP f -> case wit of -- f :: phi _a -> Void
            Ex (x :: phi b) -> f x -- matching against Ex extracts a type variable, call it b, and then x :: phi b

So the question is, what type should be used for _a? Well, we are applying f :: phi _a -> Void to x :: b (where b is the type variable stored in wit), so we should set _a := b. But this is a scoping violation. b is only extracted by matching against Ex, which happens after we've specialized no and extracted f, so f's type cannot depend on b. Thus, there's no choice of _a that can make this work without letting the existential variable escape its scope. Error.

The solution, as you've discovered, is to match against Ex (thus extracting the type inside it) before applying that type to no.

theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem prf wit = case wit of
    Ex (x :: phi b) -> case prf of
        All no -> case no @b of
            NP f -> f x
-- or
theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem (All no) (Ex x) | NP f <- no = f x