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到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为特定（未指定）类型。

您真正需要的是模式匹配 type 的东西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

然后你就可以useBar通过模式匹配来使用proveBar.