[GHC] #15635: Implication introduction for quantified constraints

12 Sep 2018

      #15635: Implication introduction for quantified constraints
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Now that we have `QuantifiedConstraints`, it seems we need some
 implication introduction form. The `constraints` package has these types:

 {{{#!hs
 data Dict a where
   Dict :: a => Dict a

 newtype a :- b = Sub (a => Dict b)
 }}}

 `QuantifiedConstraints` suggests another version of `:-`:

 {{{#!hs
 newtype Imp a b = Imp
   { unImp :: forall r. ((a => b) => r) -> r}
 }}}

 We can write

 {{{#!hs
 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:

 {{{#!hs
 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:

 {{{#!hs
 implIntro
   :: ((a => b) => q)
   -> (forall r. (b => r) -> (a => r))
   -> q
 }}}

 In Core (modulo type abstraction and application), we could simply write

 {{{#!hs
 implIntro f g = f (g id)
 }}}

 Unfortunately, I doubt that `implIntro` is really general enough to do
 everything people will want in this space.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15635
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler