Juggling existentials without unsafeCoerce

Question

Lately I have been playing with this type, which I understand to be an encoding of the free distributive functor (for tangential background on that, see this answer):

data Ev g a where
    Ev :: ((g x -> x) -> a) -> Ev g a

deriving instance Functor (Ev g)

The existential constructor ensures I can only consume an Ev g by supplying a polymorphic extractor forall x. g x -> x, and that the lift and lower functions of the free construction can be given compatible types:

runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv (Ev s) f = s f

evert :: g a -> Ev g a
evert u = Ev $ \f -> f u

revert :: Distributive g => Ev g a -> g a
revert (Ev s) = s <$> distribute id

However, there is a difficulty upon trying to give Ev g a Distributive instance. Given that Ev g is ultimately just a function with a weird argument type, one might hope that just threading distribute for functions (which amounts to (??) :: Functor f => f (a -> b) -> a -> f b from lens, and doesn't inspect the argument type in any way) through the Ev wrapper:

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap (\(Ev s) -> s)

That, however, does not work:

Flap3.hs:95:53: error:
    • Couldn't match type ‘x’ with ‘x0’
      ‘x’ is a rigid type variable bound by
        a pattern with constructor:
          Ev :: forall (g :: * -> *) x a. ((g x -> x) -> a) -> Ev g a,
        in a lambda abstraction
        at Flap3.hs:95:44-47
      Expected type: (g x0 -> x0) -> a
        Actual type: (g x -> x) -> a
    • In the expression: s
      In the first argument of ‘fmap’, namely ‘(\ (Ev s) -> s)’
      In the second argument of ‘(.)’, namely ‘fmap (\ (Ev s) -> s)’
    • Relevant bindings include
        s :: (g x -> x) -> a (bound at Flap3.hs:95:47)
   |
95 |     distribute = Ev . distribute . fmap (\(Ev s) -> s) 
   |                                                     ^
Failed, no modules loaded.

GHC objects to rewrapping the existential, even though we do nothing untoward with it between unwrapping and rewrapping. The only way out I found was resorting to unsafeCoerce:

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap (\(Ev s) -> unsafeCoerce s)

Or, spelling it in a perhaps more cautious manner:

instance Distributive (Ev g) where
    distribute = eevee . distribute . fmap getEv
        where
        getEv :: Ev g a -> (g Any -> Any) -> a
        getEv (Ev s) = unsafeCoerce s
        eevee :: ((g Any -> Any) -> f a) -> Ev g (f a)
        eevee s = Ev (unsafeCoerce s)

Is it possible to get around this problem without unsafeCoerce? or there truly is no other way?

Additional remarks:

• I believe Ev is the most correct type I can give to the construction, though I would be happy to be proved wrong. All my attempts to shift the quantifiers elsewhere lead either to needing unsafeCoerce somewhere else or to evert and revert having types that don't allow them to be composed.

• This situation looks, at first glance, similar to the one described in this blog post by Sandy Maguire, which ends up sticking with unsafeCoerce as well.

---

The following take at giving Ev g a Representable instance might put the problem into sharper relief. As dfeuer notes, this isn't really supposed to be possible; unsurprisingly, I had to use unsafeCoerce again:

-- Cf. dfeuer's answer.
newtype Goop g = Goop { unGoop :: forall y. g y -> y }

instance Representable (Ev g) where
    type Rep (Ev g) = Goop g
    tabulate f = Ev $ \e -> f (Goop (goopify e))
        where
        goopify :: (g Any -> Any) -> g x -> x
        goopify = unsafeCoerce
    index (Ev s) = \(Goop e) -> s e

While goopify sure looks alarming, I think there is a case for it being safe here. The existential encoding means any e that gets passed to the wrapped function will necessarily be an extractor polymorphic on the element type, that gets specialised to Any merely because I asked for that to happen. That being so, forall x. g x -> x is a sensible type for e. This dance of specialising to Any only to promptly undo it with unsafeCoerce is needed because GHC forces me to get rid of the existential by making a choice. This is what happens if I leave out the unsafeCoerce in this case:

Flap4.hs:64:37: error:
    • Couldn't match type ‘y’ with ‘x0’
      ‘y’ is a rigid type variable bound by
        a type expected by the context:
          forall y. g y -> y
        at Flap4.hs:64:32-37
      Expected type: g y -> y
        Actual type: g x0 -> x0
    • In the first argument of ‘Goop’, namely ‘e’
      In the first argument of ‘f’, namely ‘(Goop e)’
      In the expression: f (Goop e)
    • Relevant bindings include
        e :: g x0 -> x0 (bound at Flap4.hs:64:24)
   |
64 |     tabulate f = Ev $ \e -> f (Goop e) 
   |                                     ^
Failed, no modules loaded.

---

Prolegomena needed to run the code here:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Distributive
import Data.Functor.Rep
import Unsafe.Coerce
import GHC.Exts (Any)

-- A tangible distributive, for the sake of testing.
data Duo a = Duo { fstDuo :: a, sndDuo :: a }
    deriving (Show, Eq, Ord, Functor)

instance Distributive Duo where
    distribute u = Duo (fstDuo <$> u) (sndDuo <$> u)

Answer 1

danidiaz 和 dfeuer 的建议使我得到了更整洁的编码，尽管unsafeCoerce仍然是必要的：

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Unsafe.Coerce
import GHC.Exts (Any)
import Data.Distributive
import Data.Functor.Rep

-- Px here stands for "polymorphic extractor".
newtype Px g = Px { runPx :: forall x. g x -> x }

newtype Ev g a = Ev { getEv :: Px g -> a }
    deriving Functor

runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv s e = s `getEv` Px e

evert :: g a -> Ev g a
evert u = Ev $ \e -> e `runPx` u

revert :: Distributive g => Ev g a -> g a
revert (Ev s) = (\e -> s (mkPx e)) <$> distribute id
    where
    mkPx :: (g Any -> Any) -> Px g
    mkPx e = Px (unsafeCoerce e) 

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap getEv

instance Representable (Ev g) where
    type Rep (Ev g) = Px g
    tabulate = Ev 
    index = getEv

x我最初表述中的变量本质Ev上是普遍量化的。我只是将其伪装成函数箭头后面的存在主义。虽然该编码使得可以在revert没有 的情况下进行编写unsafeCoerce，但它将负担转移到了实例实现上。在这种情况下，直接使用通用量化最终会更好，因为它可以将魔力集中在一个地方。

这里的技巧本质上与问题中unsafeCoerce演示的相同： in专门化为，然后在 , 下立即撤消专门化。我相信这个技巧是安全的，因为我对所输入的内容有足够的控制权。tabulatexdistribute id :: Distributive g => g (g x -> x)AnyfmapunsafeCoerceunsafeCoerce

至于摆脱unsafeCoerce，我实在是想不出什么办法。部分问题在于，我似乎需要某种形式的谓语类型，因为这个unsafeCoerce技巧最终会forall x. g (g x -> x)变成g (forall x. g x -> x). 为了进行比较，我可以使用属于所讨论的扩展范围的命令式类型功能的子集编写一个模糊类似（如果更简单的话）的场景ExplicitImpredicativeTypes（请参阅GHC 票证 #14859和其中的链接进行讨论）：

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}

newtype Foo = Foo ([forall x. Num x => x] -> Int)

testFoo :: Applicative f => Foo -> f Int
testFoo (Foo f) = fmap @_ @[forall x. Num x => x] f 
    $ pure @_ @[forall x. Num x => x] [1,2,3]

GHCi> :set -XImpredicativeTypes 
GHCi> :set -XTypeApplications 
GHCi> testFoo @Maybe (Foo length)
Just 3

distribute id然而，比 更棘手[1,2,3]。在 中id :: g x -> g x，我想要保持量化的类型变量出现在两个位置，其中之一是distribute（(->) (g x)函子）的第二个类型参数。至少在我未经训练的眼睛看来，这看起来非常棘手。