How to give GHC a hint for constructing QuantifiedConstraints?

Question

If I have the method:

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

Then how do I pass this as the context to:

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

binding foo to Foo ?

---

Dict is defined here https://hackage.haskell.org/package/constraints-0.10.1/docs/Data-Constraint.html#g:2

Answer 1

You can't with what you've got.

In order to use useBar with foo ~ Foo you need evidence that (forall x. SingI x => Barable (Foo x)).

Pattern matching on proveBar won't work, because by the time you match Dict, x is no longer universally qualified; you've constrained x to be a particular (unspecified) type.

What you really need is to pattern match something of type Dict (forall x. SingI x => Barable (Foo x)), but this type isn't currently supported by 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))

If instead you had evidence of the form

proveBar :: SingIBarable Foo

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

Then you'd be able to use useBar by pattern matching on proveBar.