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

3 Feb 2017

      #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 RyanGlScott):

 Thanks you Simon for the extra details. But I'm still quite fuzzy on some
 of the particulars. To be specific:

 1. You've indicated that `approximateWC` is the way to go for retrieving
 the residual constraints out of an implication. But the type signature for
 `approximateWC` is more complicated than I expected:

    {{{#!hs
    approximateWC :: Bool -> WantedConstraints -> Cts
    -- Postcondition: Wanted or Derived Cts
    -- See Note [ApproximateWC]
    approximateWC float_past_equalities wc
    }}}

    In particular, there's this mysterious `float_past_equalities`
 argument. I've tried reading `Note [ApproximateWC]` to figure out what
 this means, but it talks about inferring most general types, which I'm not
 sure is relevant to this story or not. Should `float_past_equalities` be
 `True` or `False`?

 2. I didn't really follow what you were trying to say here:

    Replying to [comment:14 simonpj]:
    > 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.
    >
    >

    First of all, you jumped from a concrete example to `forall d. CX =>
 RC` halfway through. What are `CX` and `RC` here? Why did we switch from
 `forall b.` to `forall d.`?

    Also, should I interpret this as meaning that if there are any
 implication constraints leftover after solving which contain something of
 the form `forall x. C => Foo x` (i.e., if there are constraints which
 contain type variables other than the class's type variables), that should
 be an error? Do we already take care of this with
 [http://git.haskell.org/ghc.git/blob/bbd3c399939311ec3e308721ab87ca6b9443f358...
 these lines] in `TcDerivInfer`:

    {{{#!hs
    ; (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols []
 unsolved
                -- The buildImplicationFor is just to bind the skolems,
                -- in case they are mentioned in error messages
                -- See Trac #11347
    -- Report the (bad) unsolved constraints
    ; unless defer (reportAllUnsolved (mkImplicWC implic))
    }}}

    Or does something else need to happen?

    Finally, I'm rather confused by your comments about `simplifyInfer`.
 Are you saying that I should literally use` simplifyInfer` to solve these
 implications, or that I should be copy-pasting code from `simplifyInfer`
 for this use case? If it's the former, how do I invoke `simplifyInfer`?
 Its type signature is rather daunting:

    {{{#!hs
    simplifyInfer :: TcLevel               -- Used when generating the
 constraints
                  -> InferMode
                  -> [TcIdSigInst]         -- Any signatures (possibly
 partial)
                  -> [(Name, TcTauType)]   -- Variables to be generalised,
                                           -- and their tau-types
                  -> WantedConstraints
                  -> TcM ([TcTyVar],    -- Quantify over these type
 variables
                          [EvVar],      -- ... and these constraints (fully
 zonked)
                          TcEvBinds)    -- ... binding these evidence
 variables
    }}}

    In particular, I'm unfamiliar with what the `InferMode`,
 `[TcIdSigInst]`, and `[(Name, TcTauType)]` arguments should be, and if the
 returned `TcEvBinds` is relevant.

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