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-Fo... [2] https://hackage.haskell.org/package/constraints-0.14/docs/Data-Constraint-Fo...