构造函数的通用和存在量词可以在模式匹配中交换吗？

Question

这是我认为（类型）有意义的片段，但 ghc 不喜欢。我希望类型注释的一些巧妙使用可以使它起作用，但我的实验失败了。有什么建议？

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

这很可能是不可能的，因为它相当于交换一个普遍存在的量词，但我希望。

Answer 1

我在 Agda 中尝试了这个例子，\n看看它是否有意义

\n

module Comm where\n\nopen import Data.Bool using (Bool; true)\n\nrecord T (A : Set) : Set\xe2\x82\x81 where\n  constructor MkT\n  field\n    F : Set \xe2\x86\x92 Set\n    f : F A \xe2\x86\x92 A\n\nbar : {F : Set \xe2\x86\x92 Set} \xe2\x86\x92 (\xe2\x88\x80 A \xe2\x86\x92 F A \xe2\x86\x92 A) \xe2\x86\x92 Bool\nbar _ = true\n\nfoo : (\xe2\x88\x80 A \xe2\x86\x92 T A) \xe2\x86\x92 Bool\nfoo k = bar {F = k Bool .T.F} \xce\xbb A \xe2\x86\x92 {!k A .T.f!}\n-- Goal: k Bool .T.F A \xe2\x86\x92 A\n-- Have: T.F. (k A) A \xe2\x86\x92 A\n

\n

在 foo 中，我们需要forall a. T a用某种类型进行实例化。\n由于该类型是参数化的，因此任何类型都应该这样做，并且F是相同的。\n但是 Agda 和 Haskell 都没有内置这种参数化。

\n

所以我认为只要正确使用unsafeCoerce，\n事情就会成功。

\n

module Comm where\n\nopen import Data.Bool using (Bool; true)\n\nrecord T (A : Set) : Set\xe2\x82\x81 where\n  constructor MkT\n  field\n    F : Set \xe2\x86\x92 Set\n    f : F A \xe2\x86\x92 A\n\nbar : {F : Set \xe2\x86\x92 Set} \xe2\x86\x92 (\xe2\x88\x80 A \xe2\x86\x92 F A \xe2\x86\x92 A) \xe2\x86\x92 Bool\nbar _ = true\n\nfoo : (\xe2\x88\x80 A \xe2\x86\x92 T A) \xe2\x86\x92 Bool\nfoo k = bar {F = k Bool .T.F} \xce\xbb A \xe2\x86\x92 {!k A .T.f!}\n-- Goal: k Bool .T.F A \xe2\x86\x92 A\n-- Have: T.F. (k A) A \xe2\x86\x92 A\n

\n