# Implication introduction for quantified constraints

Reported by: Owned by: dfeuer normal 8.6.1 Compiler 8.6.1-beta1 QuantifiedConstraints Bj0rn Unknown/Multiple Unknown/Multiple None/Unknown #14937

### Description

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.

### comment:1 Changed 13 months ago by Bj0rn

This is the same as #14937.