[GHC] #14937: QuantifiedConstraints: Reify implication constraints from terms lacking them

[GHC]

#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