Can a universal and existential quantifier for a constructor be commuted in pattern matching?

user_649287 0
Viewed 163

Here is a snippet that I think makes (type) sense, but which ghc doesn't like. I was hoping that some tricky use of type annotations could make it work, but my experiments have failed. Any suggestions?

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Ex where

data T a where
  T :: Functor f => (f a -> a) -> T a

foo :: (forall a . T a) -> Bool
foo (T f) = bar f

bar :: Functor f => (forall a . f a -> a) -> Bool
bar _f = True

It could very well be impossible since it amounts to commuting a universal and existential quantifier, but I was hoping.

haskell
1 Answers

I tried that example in Agda, to see if it makes sense

module Comm where

open import Data.Bool using (Bool; true)

record T (A : Set) : Set₁ where
  constructor MkT
  field
    F : Set → Set
    f : F A → A

bar : {F : Set → Set} → (∀ A → F A → A) → Bool
bar _ = true

foo : (∀ A → T A) → Bool
foo k = bar {F = k Bool .T.F} λ A → {!k A .T.f!}
-- Goal: k Bool .T.F A → A
-- Have: T.F. (k A) A → A

In foo, we need to instantiate forall a. T a with some type. As the type is parametric, any should do, and F would be the same. But neither Agda nor Haskell have that parametricity built in.

So I think that with right use of unsafeCoerce, things will work.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE TypeApplications #-}
module Ex where

import Unsafe.Coerce (unsafeCoerce)
import Data.List.NonEmpty (NonEmpty (..))
import GHC.Exts (Any)

data T a where
  T :: Functor f => (f a -> a) -> T a

bar :: Functor f => (forall a . f a -> a) -> Bool
bar _f = _f `seq` True

foo :: (forall a . T a) -> Bool
foo t = foo' t t

foo' :: (forall a. T a) -> T Any -> Bool
foo' t (T f) = aux f where
    aux :: forall f. Functor f => (f Any -> Any) -> Bool
    aux f' = bar f''
      where
        f'' :: forall a. f a -> a
        f'' = unsafeCoerce f'

--- test

ex :: forall a. T a
ex = T (\(x :| _) -> x)

ex2 :: Bool
ex2 = foo ex
user_13080580
Related