## QuantifiedConstraints: Reify implication constraints from terms lacking them

This is possibly the same question as #14822 (closed), asked in more general terms. Would it be viable/sound to have a way of extracting implication constraints out of terms which effectively encode such constraints, such as `(:-)`

from `Data.Constraint`

?

Here's how I think about it. `a :- b`

is equivalent to `forall r. a => (b => r) -> r`

. This is a type that, as I read it, expresses "if you can show `a`

, then I can show `b`

". This is very similar to `forall r. ((a => b) => r) -> r`

, which expresses "(without obligations) I can show that `a`

implies `b`

".

It seems to me (and I know this is hand-wavy) like expressions of both of these types actually must have the same "knowledge", i.e. that `a`

imples `b`

. Is this actually correct?

I am wondering whether we could have a built-in function like:

`reifyImplication :: forall a b. (forall r. a => (b => r) -> r) -> (forall r. ((a => b) => r) -> r)`

We can already write the function that goes the other direction.

There are plenty of ways to represent this conversion. Some more straight-forward, using `a :- b`

or `Dict a -> Dict b`

. I just went with one that doesn't require any types beyond arrows.

I'm curious about the soundness of this. I have tried really hard to implement this function, but I don't think it can be done.

I don't know if this proves anything, but replacing `(=>)`

with `(->)`

and all constraints `c`

with `Dict c`

, this function can be written:

```
dictReifyImplication :: forall a b. (forall r. Dict a -> (Dict b -> r) -> r) -> (forall r. ((Dict a -> Dict b) -> r) -> r)
dictReifyImplication f g = g (\a -> f a id)
```

## Trac metadata

Trac field | Value |
---|---|

Version | 8.5 |

Type | FeatureRequest |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | #14822 (closed) |

Blocking | |

CC | |

Operating system | |

Architecture |