[Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?

[Tom Ellis]

The constraints library [1] has

    implied :: forall a b. (a => b) => a :- b

from which I can obtain

    implied' :: Dict (a |- b) -> a :- b
    implied' Dict = implied

but can I get the converse of this, that is

    coimplied :: (a :- b) -> Dict (a |- b)
    coimplied = error "Can it be done?"

I don't see how.  The library itself only mentions "|-" in its
definition.  Would this combinator violate some guarantee that's
essential for the safe use of type classes?

I'm a bit confused why the same library allows abstraction over type
variables with forall_[2]

    forall_ :: (forall a. Dict (p a)) -> Dict (Forall p) 

but not abstraction over "term" variables (i.e. of kind Constraint),
as in coimplied.

Alternatively, can someone help me achieve my goal another way?  That
is, I need to be able to dischange the quantified constraint

    forall i. T0 i => T2 i

given that I can already discharge the constraint

    forall i. T1 i => T2 i

and I have available the value

    forall i. T0 i => Dict (T1 i)

>From the latter I can easily get

    forall i. T0 i :- T1 i

But without coimplied I don't know how to proceed.

Thanks,

Tom


[1] https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Forall.html

[2] https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Forall.html#v:forall_