Implication introduction for quantified constraints

Now that we have QuantifiedConstraints, it seems we need some implication introduction form. The constraints package has these types:

data Dict a where
  Dict :: a => Dict a

newtype a :- b = Sub (a => Dict b)

QuantifiedConstraints suggests another version of :-:

newtype Imp a b = Imp
  { unImp :: forall r. ((a => b) => r) -> r}

We can write

fromImp :: Imp a b -> a :- b
fromImp (Imp f) = Sub (f Dict)

But ... there's no way to go the other way!

Let's try it:

toImp :: a :- Dict b -> a :- b
toImp (Sub ab) = Imp $ \r -> _

We get

* Found hole: _ :: r
* Relevant bindings include
    r :: (a => b) => r
    ab :: a => Dict b

There's no way to put these things together. But there's no terribly obvious reason they ''can't* be combined. a => b is a function from an a dictionary to a b dictionary. a => Dict b is a function from an a dictionary to a value that *contains'' a b dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:

implIntro
  :: ((a => b) => q)
  -> (forall r. (b => r) -> (a => r))
  -> q

In Core (modulo type abstraction and application), we could simply write

implIntro f g = f (g id)

Unfortunately, I doubt that implIntro is really general enough to do everything people will want in this space.

Trac metadata

Trac field	Value
Version	8.6.1-beta1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture