Opened 5 years ago

Closed 3 years ago

#9821 closed bug (fixed)

DeriveAnyClass support for higher-kinded classes + some more comments

Reported by: dreixel Owned by: dreixel
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 7.9
Keywords: Generics Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #5462, #9968, #12144 Differential Rev(s): Phab:D2961
Wiki Page:

Description

#5462 was merged before a few final fixes were done. This ticket serves to record that. Left to address are:

https://phabricator.haskell.org/D476?id=1443#inline-3652

https://phabricator.haskell.org/D476?id=1443#inline-3648

https://phabricator.haskell.org/D476?id=1443#inline-3646

Also, DeriveAnyClass currently panics at higher-kinded classes (like ((* -> *) -> *) -> Constraint).

I'll fix this.

Change History (19)

comment:1 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:2 Changed 5 years ago by dreixel

Milestone: 7.12.17.10.1

comment:3 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to the 7.12.1 milestone, as these tickets won't be fixed in time for the 7.10.1 release (unless you, the reader, help write a patch :)

comment:4 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:5 Changed 4 years ago by thomie

Status: newinfoneeded

What is the status here? Note that #9968 was fixed recently.

comment:6 Changed 4 years ago by simonpj

Keywords: Generics added

comment:7 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:8 Changed 3 years ago by RyanGlScott

To the best of my knowledge, here's a summary of the current state of each of those comments:

  1. https://phabricator.haskell.org/D476?id=1443#inline-3652 - The logic of this check is explained more thoroughly in Note (Determining whether newtype-deriving is appropriate), which will be further clarified with Phab:D2280.
  1. https://phabricator.haskell.org/D476?id=1443#inline-3648 and https://phabricator.haskell.org/D476?id=1443#inline-3646 ask to clarify that DeriveAnyClass does indeed only work on argument types of kind * and * -> * at the moment. #9968 fixed these.

So the only thing that remains is to implement support for deriving types of other kinds with DeriveAnyClass. I believe that #12144 is very relevant here, since I don't see a way to properly fix that ticket without overhauling the way DeriveAnyClass infers its instance contexts in deriving clauses. Simon's comment here provides one suggestion on how to do this.

comment:9 Changed 3 years ago by simonpj

Sounds good to me. Let's go with the email thread

comment:10 Changed 3 years ago by RyanGlScott

Blocked By: 12918 added

Simon, I've implemented most of the proposal in the e-mail thread, but I believe I'm blocked on #12918. To see why, imagine this scenario:

{-# LANGUAGE DefaultSignatures, DeriveAnyClass #-}
module T9821 where

class Eq1 f where
  (==#) :: (Eq a1) => f a1 -> f a1 -> Bool
  default (==#) :: Eq (f a2) => f a2 -> f a2 -> Bool
  (==#) = (==)

data Foo x = Foo (Either x x)
    deriving (Eq, Eq1)

In order to derive Eq1 with DeriveAnyClass, we need to be able to solve the wanted constraint Eq (Foo a2), which in turn demands that we solve Eq a2. But we have as a given constraint Eq a1, not Eq a2! So this would suggest that in TcDerivInfer, we need to unify f a1 -> f a1 -> Bool with f a2 -> f a2 -> Bool.

But there's a big problem with doing this during the deriving stage: deriving happens before instances are validity-checked. That means that there's no guarantee that this unification is guaranteed to succeed. For instance, what if Eq1 were defined this way?

class Eq1 f where
  (==#) :: (Eq a1) => f a1 -> f a1 -> Bool
  default (==#) :: f Int
  (==#) = undefined

Currently, GHC HEAD accepts this as a valid class definition. If you tried to define:

instance Eq1 Foo

Then naturally things go awry, since the two type signatures for (==#) can't unify. But if you were to derive Eq1, then this validity check wouldn't happen before we try to unify the two type signatures in TcDerivInfer! And if they fail to unify, I have no idea what kind of error message we'd give.

It all seems to point to the fact that we need a stronger validity check for typeclass definitions (that incorporates #12918) to rule out scenarios like the one above. That way, when we unify the type signatures in TcDerivInfer, we are guaranteed to succeed.

What do you think, Simon?

comment:11 Changed 3 years ago by RyanGlScott

Differential Rev(s): Phab:D2961

A WIP attempt at fixing this is at Phab:D2961.

comment:12 Changed 3 years ago by RyanGlScott

Milestone: 8.2.1
Status: infoneededpatch

comment:13 Changed 3 years ago by simonpj

Blocked By: 12918 removed

comment:14 Changed 3 years ago 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.

comment:15 in reply to:  14 Changed 3 years ago 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:
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?

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

Replying to 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 these lines in TcDerivInfer:

; (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:

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.

comment:16 Changed 3 years ago by simonpj

but it talks about inferring most general types, which I'm not sure is relevant to this story or not

Yes it's relevant. In inferring "???" we are indeed trying to infer the most general type for the instances. We seek the context with fewest constraints (i.e. most general).

The equalities thing doesn't matter much, but for consistency with simplifyInfer set it to True.

What are CX and RC here?

I defined them earlier in the text you quoted! RC = residual context, CX is what we decide ??? should be.

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?

Yes, certainly. Notice that approximateWC doesn't remove the constraints it floats out; it just floats them out. They are still there in RC; but we'll solve them easily from CX.

Do we already take care of this with ​these lines in TcDerivInfer:

I'm not sure.. too much is in flux. But you don't need to solve it because you don't need to know the answer here: just emit it and it'll get solved later.

Are you saying that I should literally use simplifyInfer to solve these implications

No: sharing code with simplifyInfer in due course would be a good plan, but it does a lot more so just use it as a source of inspiration, no more.

comment:17 Changed 3 years ago by simonpj

Further clarifications

Currently in simplifyDeriv, we are using the function simplifyWantedsTcM to simplify the constraints, which seemed to work well back when all of our deriving-related constraints were simple wanteds. But now we're throwing implication constraints into the mix. Are you proposing to replace the use of simplifyWantedsTcM entirely with something la simplifyInfer? Are you proposing to invoke a simplifyInfer-like function after simplifyWantedsTcM? Something else?

Something like simplifyInfer, but simpler. Call simplifyWanteds; then approximateWC; then mkMinimalBySCs; then emit the residual constraint as above.

  1. When you say "just emit this implication": forall d. CX => RC.. To tie it back to your example in comment:10, are you proposing to emit this?
forall d. Show d => ((forall b. () => (Show d, C d b)) ^ (forall . Eq (Maybe d) => (Ord d, Show d))

That is, letting

CX = (Show d)
RC = ((forall b. () => (Show d, C d b)) ^ (forall . Eq (Maybe d) => (Ord d, Show d))

Maybe you meant comment:14. Then yes. (There are several related examples in comment:14, so I'm not sure precisely which one you mean.

I see that there is a function emitImplication, which appears to modify the state of TcM. But I'm still unsure of when the error message involving (C d b) is supposed to be thrown. That is, what specific action causes the typechecker to see the bogus (C d b) and complain?

It's the simplifyTop called right at the top level, in TcRnDriver. Most constraint solving is done by this single call to simplifyTop; only when we MUST solve eagerly (as here, to get CX) do we call the solver. Usually we just toss the unsolved constraint into the monad and solve it right at the end.

comment:18 Changed 3 years ago by Ryan Scott <ryan.gl.scott@…>

In 639e702/ghc:

Refactor DeriveAnyClass's instance context inference

Summary:
Currently, `DeriveAnyClass` has two glaring flaws:

* It only works on classes whose argument is of kind `*` or `* -> *` (#9821).
* The way it infers constraints makes no sense. It basically co-opts the
  algorithms used to infer contexts for `Eq` (for `*`-kinded arguments) or
  `Functor` (for `(* -> *)`-kinded arguments). This tends to produce overly
  constrained instances, which in extreme cases can lead to legitimate things
  failing to typecheck (#12594). Or even worse, it can trigger GHC panics
  (#12144 and #12423).

This completely reworks the way `DeriveAnyClass` infers constraints to fix
these two issues. It now uses the type signatures of the derived class's
methods to infer constraints (and to simplify them). A high-level description
of how this works is included in the GHC users' guide, and more technical notes
on what is going on can be found as comments (and a Note) in `TcDerivInfer`.

Fixes #9821, #12144, #12423, #12594.

Test Plan: ./validate

Reviewers: dfeuer, goldfire, simonpj, austin, bgamari

Subscribers: dfeuer, thomie

Differential Revision: https://phabricator.haskell.org/D2961

comment:19 Changed 3 years ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.