haskell - 如何给 GHC 提示构建 QuantifiedConstraints？

Question

如果我有方法:

proveBar :: forall x . SingI x => Dict (Barable (Foo x))
proveBar = ...

那么我如何将其作为上下文传递给:

useBar :: forall foo . (forall x. SingI x => Barable (foo x)) => ...
useBar = ...

将foo绑定(bind)到Foo？

<小时/>

Dict 在这里定义 https://hackage.haskell.org/package/constraints-0.10.1/docs/Data-Constraint.html#g:2

Answer 1

你不能用你所拥有的东西。

为了将 useBar 与 foo ~ Foo 一起使用，您需要证据证明 (forall x.SingI x => Barable (Foo x)).

在 proveBar 上进行模式匹配将不起作用，因为当您匹配 Dict 时，x 不再是通用限定的；您已将 x 限制为特定(未指定)类型。

您真正需要的是模式匹配 Dict (forall x.SingI x => Barable (Foo x)) 类型的内容，但 GHC 目前不支持此类型:

• Illegal polymorphic type: forall x. SingI x => Barable (Foo x)
  GHC doesn't yet support impredicative polymorphism
• In the type signature: proveBar' :: Dict (forall x. SingI x => Barable (Foo x))

如果您有表格证据

proveBar :: SingIBarable Foo

data SingIBarable foo where
  SingIBarable :: (forall x. SingI x => Barable (foo x)) -> SingIBarable foo

然后您就可以通过 proveBar 上的模式匹配来使用 useBar。