Difference between forall quantifier inside a constructor and outside a constructor

Question

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}

import Data.Proxy

data Foo = FooA | FooB

class Bar (a :: k) where
    bar :: Proxy a -> Int

instance Bar FooA where
    bar _ = 1

instance Bar FooB where
    bar _ = 2

foo1 :: forall (a :: Foo). Proxy a -> (Bar a => Proxy a)
foo1 p = p

data BarProxy = BarProxy (forall a. Bar a => Proxy a)

foo2 :: forall (a :: Foo). Proxy a -> BarProxy
foo2 p = BarProxy (foo1 p)

main = print "Hello World"

In this code:

Doesn't foo1, given any Proxy a where a is of kind Foo, return a Proxy a such that a has an instance of Bar?
Doesn't BarProxy constructor accept any Proxy a, where a has an instance of Bar? How is it different from data BarProxy = forall a. BarProxy (Bar a => Proxy a)?
Why does foo2 p = BarProxy (foo1 p) fail with the below error?

Test6.hs:27:20: error:
    • Couldn't match type ‘a1’ with ‘a’
      ‘a1’ is a rigid type variable bound by
        a type expected by the context:
          forall (a1 :: Foo). Bar a1 => Proxy a1
        at Test6.hs:27:10-26
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo2 :: forall (a :: Foo). Proxy a -> BarProxy
        at Test6.hs:26:1-46
      Expected type: Proxy a1
        Actual type: Proxy a
    • In the first argument of ‘BarProxy’, namely ‘(foo1 p)’
      In the expression: BarProxy (foo1 p)
      In an equation for ‘foo2’: foo2 p = BarProxy (foo1 p)
    • Relevant bindings include
        p :: Proxy a (bound at Test6.hs:27:6)
        foo2 :: Proxy a -> BarProxy (bound at Test6.hs:27:1)
   |
27 | foo2 p = BarProxy (foo1 p)
   |                    ^^^^^^

user_8075159 · Answer

No. My understanding is that the signature of foo1 is the same as forall (a :: Foo). Bar a => Proxy a -> Proxy a (though I couldn't find any document). In ghci, :t foo1 gives foo1 :: Bar a => Proxy a -> Proxy a. Given any Proxy a where a is of kind Foo and an instance of Bar, it returns Proxy a.
No. The constructor BarProxy has rank-2 polymorphic type (forall a. Bar a => Proxy a) -> BarProxy. This means that an argument p can be passed to BarProxy only if p has the type Proxy a for all type a which is an instance of Bar. If you want existentially quantified one, you may write
```
data BarProxy = forall a. Bar a => BarProxy (Proxy a)
```
or
```
data BarProxy where
  BarProxy :: forall a. Bar a => Proxy a -> BarProxy
```
with -XGADTs enabled.

Let us call BarProxy of type forall a. Bar a => Proxy a -> BarProxy existential BarProxy and that of type (forall a. Bar a => Proxy a) -> BarProxy universal BarProxy. For existential one, the argument p should have type either Proxy FooA or Proxy FooB (existentially quantified over {a | a is an instance of Bar} = {FooA,FooB}). For universal one, on the other hand, p should have type both Proxy FooA and Proxy FooB (universally quantified over the same set). Let us consider three proxies below.
```
proxyFooA :: Proxy FooA
proxyFooA = Proxy

proxyFooB :: Proxy FooB
proxyFooB = Proxy

proxyPoly :: forall a. Proxy a
proxyPoly = Proxy
```
Existential BarProxy accepts any of the three while universal one accepts only proxyPoly.
foo2 p = BarProxy (foo1 p) compiles for existential BarProxy.

Difference between forall quantifier inside a constructor and outside a constructor

1 Answers