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
Milestone: | 7.10.1 → 7.12.1 |
---|
comment:2 Changed 5 years ago by
Milestone: | 7.12.1 → 7.10.1 |
---|---|
Related Tickets: | #5462 → #5462, #9968 |
comment:3 Changed 5 years ago by
Milestone: | 7.10.1 → 7.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:5 Changed 4 years ago by
Status: | new → infoneeded |
---|
What is the status here? Note that #9968 was fixed recently.
comment:6 Changed 4 years ago by
Keywords: | Generics added |
---|
comment:7 Changed 4 years ago by
Milestone: | 8.0.1 |
---|
comment:8 Changed 3 years ago by
Related Tickets: | #5462, #9968 → #5462, #9968, #12144 |
---|
To the best of my knowledge, here's a summary of the current state of each of those comments:
- 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.
- 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:10 Changed 3 years ago by
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
Differential Rev(s): | → Phab:D2961 |
---|
A WIP attempt at fixing this is at Phab:D2961.
comment:12 Changed 3 years ago by
Milestone: | → 8.2.1 |
---|---|
Status: | infoneeded → patch |
comment:13 Changed 3 years ago by
Blocked By: | 12918 removed |
---|
comment:14 follow-up: 15 Changed 3 years ago by
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 Changed 3 years ago by
Thanks you Simon for the extra details. But I'm still quite fuzzy on some of the particulars. To be specific:
- You've indicated that
approximateWC
is the way to go for retrieving the residual constraints out of an implication. But the type signature forapproximateWC
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 readingNote [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. Shouldfloat_past_equalities
beTrue
orFalse
?
- 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 -> StringI've replaced
Ix b
byC b
and I've removed it from the vanilla sig forBar
. Now the implication constraint will beforall b. () => Show (Maybe d), C (Maybe d) bSuppose 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 onlyShow d
from this, becuase(C d b)
is captured by theforall b
. What do to?Easy! Once we have decided "???" should be CX, say, just emit this implication (to be solved later):
forall d. CX => RCwhere 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 areCX
andRC
here? Why did we switch fromforall b.
toforall 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 inTcDerivInfer
:
; (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 usesimplifyInfer
to solve these implications, or that I should be copy-pasting code fromsimplifyInfer
for this use case? If it's the former, how do I invokesimplifyInfer
? 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 returnedTcEvBinds
is relevant.
comment:16 Changed 3 years ago by
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
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.
- 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:19 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
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.