## 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 |