循环键入约束
在下面的例子中，我试图让foo返回它的“预期”多态输出类型。 这个想法是， foo返回一个多态值和一个存在类型，然后bar将元组的类型指定为隐藏类型。 （当然这只有在bar的类型也是存在的时才有效，在我的例子中是这样。）下面的例子编译：
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
module Foo where
import Data.Proxy
import Data.Typeable
data HiddenType where
Hidden :: (Typeable a) => Proxy a -> HiddenType
foo :: (i,HiddenType)
foo = (undefined, Hidden (Proxy::Proxy Int))
data Foo where
Foo :: i -> Foo
bar :: Foo
bar =
let (x,h) = foo
in case h of
(Hidden (p::Proxy i)) -> Foo (x :: i)
我真的需要在foo上有一个Typeable约束：
foo :: (Typeable i) => (i,HiddenType)
当我添加该约束（没有其他更改）时，我得到这些错误：
Foo.hs:20:15:
No instance for (Typeable t0) arising from a use of ‘foo’
The type variable ‘t0’ is ambiguous
Relevant bindings include x :: t0 (bound at Foo.hs:20:8)
Note: there are several potential instances:
instance [overlap ok] Typeable ()
-- Defined in ‘Data.Typeable.Internal’
instance [overlap ok] Typeable Bool
-- Defined in ‘Data.Typeable.Internal’
instance [overlap ok] Typeable Char
-- Defined in ‘Data.Typeable.Internal’
...plus 14 others
In the expression: foo
In a pattern binding: (x, h) = foo
In the expression:
let (x, h) = foo
in case h of { (Hidden (p :: Proxy i)) -> Foo (x :: i) }
Foo.hs:22:35:
Couldn't match expected type ‘a’ with actual type ‘t0’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor
Hidden :: forall a. Typeable a => Proxy a -> HiddenType,
in a case alternative
at Foo.hs:22:6-24
Relevant bindings include
p :: Proxy a (bound at Foo.hs:22:14)
x :: t0 (bound at Foo.hs:20:8)
In the first argument of ‘Foo’, namely ‘(x :: i)’
In the expression: Foo (x :: i)
Failed, modules loaded: none.
我知道限制会变成核心的争论，所以我认为这里的问题是GHC无法处理GADT的模式绑定。 如果可以的话，我可以使用递归的方式来表达这样的内容：
bar :: Foo
bar =
let (x :: i,h) = foo
(Hidden (p::Proxy i)) = h
in Foo x
这应该会限制范围，为foo提供额外的参数。 我的意图是h包含一些（隐藏的）具体类型i ，它应该用作GHC抱怨的多态函数的具体类型：
Foo.hs:19:8:
You cannot bind scoped type variable ‘i’
in a pattern binding signature
In the pattern: x :: i
In the pattern: (x :: i, h)
In a pattern binding:
(x :: i, h) = foo
Foo.hs:20:8:
My brain just exploded
I can't handle pattern bindings for existential or GADT data constructors.
Instead, use a case-expression, or do-notation, to unpack the constructor.
In the pattern: Hidden (p :: Proxy i)
In a pattern binding: (Hidden (p :: Proxy i)) = h
In the expression:
let
(x :: i, h) = foo
(Hidden (p :: Proxy i)) = h
in Foo x
我的用例的假设是1. foo同时计算i和HiddenType 2.隐藏类型的值涉及（至少部分）第一个元组元素的计算。 这意味着我不想在bar调用foo两次（一次获取HiddenType ，一次使用该类型绑定第一个元组元素）。 有没有办法在存在foo约束的情况下使bar的定义成为可能？
我想问题是foo的返回值实际上并不是多态的。 foo本身是多态的，但返回值必须存在于特定类型中。 不幸的是，您要使用的类型尚不可用，并且因为有循环引用，因此无法在foo的呼叫站点引入该范围。 如果我们在伪核心中写出foo的定义，问题foo清楚了：
foo (@ iType) _ = (undefined @ iType, HiddenType...)
这里@ iType是一个类型参数。 在获取HiddenType之前，我们需要首先执行foo的类型应用程序（以及未使用的字典应用程序），因此无法按HiddenType执行此操作。
幸运的是，有一种方法可以说服ghc foo应该返回一个实际的多态值：
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE ImpredicativeTypes #-}
module Foo where
import Data.Proxy
import Data.Typeable
data HiddenType where
Hidden :: (Typeable a) => Proxy a -> HiddenType
foo :: (forall i. Typeable i => i,HiddenType)
foo = (undefined, Hidden (Proxy::Proxy Int))
data Foo where
Foo :: i -> Foo
bar =
let (x,h) = foo
in case h of
Hidden p -> Foo (x `asProxyTypeOf` p)
如果你熟悉更高级的类型（例如RankNTypes扩展），你可以将ImpredicativeTypes看作类似的东西，除了数据结构而不是函数。 例如，没有ImpredicativeTypes你可以写：
list1 :: forall t. Typeable t => [t]
这是包含t类型所有值的列表的类型，对于具有Typeable约束的某些t 。 即使它是多态的，列表中的每个元素都将是相同的类型！ 相反，如果你要移动的forall名单内，让每一个元件可以是不同类型的t ， ImpredicativeTypes将允许这样的：
list2 :: [forall t. Typeable t => t]
这不是一个通常启用的扩展，但它偶尔有用。
foo的impandicative版本的核心也有点不同：
foo = ((@ iType) _ -> undefined @ iType, HiddenType...)
你可以看到，如果你给let添加一个注解，这就允许x是多态的：
bar :: Foo
bar =
let (x :: forall i. Typeable i => i,h) = foo
in case h of
Hidden p -> Foo (x `asProxyTypeOf` p)
这允许你延迟隐藏类型的x的实例化，直到它可用时为止。 你仍然需要将它放在Foo或另一个Hidden ，因为ghc不允许该类型在第一个Hidden模式匹配下退出。