[GHC] #9821: DeriveAnyClass support for higher-kinded classes + some more comments

[GHC]

#9821: DeriveAnyClass support for higher-kinded classes + some more comments
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                Owner:  dreixel
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  7.9
      Resolution:                    |             Keywords:  Generics
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #5462, #9968,     |  Differential Rev(s):  Phab:D2961
  #12144                             |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 This is respoinding to
 [https://phabricator.haskell.org/D2961#inline-25611], concerning the way
 to use implication constraints to simplify the `DeriveAnyClass`
 implementation.

 The original idea is in
 [https://phabricator.haskell.org/D2961#inline-25543], where I said:
 I think it would help to explain more carefully what is happening here.
 How come we don't need to look at the data constructors any more? Example:
 {{{
 class Foo a where
   bar :: Ix b => a -> b -> String
   default bar :: (Show a, Ix b) => a -> b -> String
   bar x y = show x

   baz :: Eq a => a -> a -> Bool
   default baz :: (Ord a, Show a) => a -> a -> Bool
   baz x y = compare x y == EQ
 }}}
 Given
 {{{
 deriving instance Foo (Maybe d)
 }}}
 we behave as if you had written
 {{{
 instance ??? => Foo (Maybe d) where {}
 }}}
 (that is, using the default methods from the class decl), and that in turn
 means
 {{{
 instance ??? => Foo (Maybe d) where
   bar = $gdm_bar
   baz = $gdm_baz
 }}}
 where
 {{{
 $gdm_bar :: forall a. Foo a
          => forall b. (Show a, Ix b)
          => a -> b -> String
 }}}
 is the generic default method defined by the class declaratation.

 Our task is to figure out what "???" should be.  Answer: enough
 constraints to satisfy the Wanteds arising from the calls of $gdm_bar and
 $gdm_baz. So we end up with two sets of constraints to simplify:
 {{{
 bar: (Givens: [Ix b],         Wanteds: [Show (Maybe d), Ix b])
 baz: (Givens: [Eq (Maybe d)], Wanteds: [Ord (Maybe d), Show (Maybe d)])
 }}}
 Important: note that

 * the Givens come from the ordinary method type, while
 * the Wanteds come from the generic method.

 These are just implication constraints. We can combine them into a single
 constraint:
 {{{
     (forall b. Ix b => Show (Maybe d), Ix b)
 /\
     (forall . Eq (Maybe d) => Ord (Maybe d), Show (Maybe d))
 }}}
 Notice that the type variables from the head of the instance decl (just
 `d` in this case) are global to this constraint, but any local
 quantification of the generic default method (e.g. `b` in the case of
 `bar`) are locally scoped to each implication, as they obviously should
 be.

 Now we solve this constraint, getting the residual constraint (RC)
 {{{
    (forall b. Ix b => Show d)
 /\
    (forall . Eq (Maybe b) => Ord d, Show d)
 }}}
 Now we need to hoist those constraints out of the implications to become
 our candidates for the "???".  That is done by `approximateWC`, which will
 return
 {{{
    (Show d, Ord d, Show d)
 }}}
 Now we can use `mkMinimalBySCs` to remove superclasses and duplicates,
 giving
 {{{
   (Show d, Ord d)
 }}}
 And that's what we need for the "???".

 --------------
 But we aren't done yet!  Suppose we had written
 {{{
   bar :: a -> b -> String
   default bar :: (Show a, C a b) => a -> b -> String
 }}}
 I've replaced `Ix b` by `C b` and I've removed it from the vanilla sig for
 `Bar`.  Now the implication constraint will be
 {{{
  forall b. () => Show (Maybe d), C (Maybe d) b
 }}}
 Suppose we have `instance Read p => C (Maybe p) q`.  Then after
 simplification, we get the residual constraint (RC):
 {{{
  forall b. () => (Show d, Read d)
 }}}
 and all is well.  But suppose we had no such instance, or we had an
 instance like `instance C p q => C (Maybe p) q`.  Then we'd finish up with
 the residual consraint (RC):
 {{{
  forall b. () => (Show d, C d b)
 }}}
 and now `approximateWC` will produce only `Show d` from this, becuase `(C
 d b)` is captured by the `forall b`.  What do to?

 Easy!  Once we have decided "???" should be CX, say, just emit this
 implication (to be solved later):
 {{{
 forall d. CX => RC
 }}}
 where RC is the residual constraint we computed earlier.  Bingo!  From CX
 we'll be able to solve all the constraints that `approximateWC` extracted,
 and we'll be left with the error that we want to report for that `(C d b)`
 constraint.

 ------------------
 This may seem complicated, but it's '''exactly what happens in
 `TcSimplify.simplifyInfer`'''.  It does a bit more besides (figuring out
 what type variables to quantify over), but it makes a good guide.  We
 might ultimately wat to share code, but for now I think it's easier to do
 one step at a time.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9821#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler