#14937: QuantifiedConstraints: Reify implication constraints from terms lacking them -------------------------------------+------------------------------------- Reporter: Bj0rn | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #14822 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is possibly the same question as #14822, 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: {{{#!hs 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: {{{#!hs 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler