Opened 4 years ago
Last modified 10 months ago
#11008 new bug
Difficulties around inferring exotic contexts
Reported by: | crockeea | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.10.2 |
Keywords: | deriving | Cc: | RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #15868 | Differential Rev(s): | |
Wiki Page: |
Description
In the following code:
{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-} class C r type family F r newtype Foo r = Foo r instance (C (F r), Eq r) => Eq (Foo r) newtype Bar r = Bar (Foo r) deriving (Eq)
GHC produces the error
No instance for (C (F r)) arising from the 'deriving' clause of a data type declaration Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (Eq (Bar r))
If I enable StandaloneDeriving
, I am able to derive the instance: deriving instance (Eq (Foo r)) => Eq (Bar r)
The docs indicate that this is exactly the instance that should be generated by GND for
newtype T v1..vn = MkT (t vk+1..vn) deriving (C t1..tj)
,
where my code uses the following parameters:
T = Bar v1 = r n = 1 MkT = Bar t = Foo r k= 1 C = Eq j = 0
and all of the conditions enumerated in the docs seem to be met. Furthermore, Bar
seems to fit squarely into the format of data T1
in section 7.5.1 of the same documentation, which indicates it should not need StandaloneDeriving
. It seems that the type family constraint on the Eq
instance for Foo
is causing the problem, but it's not clear why I'm forced to write a standalone instance that is identical to the one that should be generated by GND.
Change History (12)
comment:1 follow-up: 2 Changed 4 years ago by
Summary: | GND with Type Families → Difficulties around inferring exotic contexts |
---|
comment:2 follow-up: 3 Changed 4 years ago by
With the deriving clause, which instance does GHC try to create?
- instance (Eq (Foo r)) => Eq (Bar r)
- instance (C (F r), Eq r) => Eq (Bar r)
If option 1, GHC has no business inspecting the constraints on the Foo r
instance. If option 2, why? Is it due to slower instances?
In either case, since I *have* a matching Eq
instance for Foo
, GHC should assume that I knew what I was doing when I wrote it, and just use it. This doesn't change the behavior when no matching instance is found, like in your example.
Whatever the result, the docs definitely need to be clearer.
comment:3 Changed 4 years ago by
Replying to crockeea:
With the deriving clause, which instance does GHC try to create?
instance (Eq (Foo r)) => Eq (Bar r)
instance (C (F r), Eq r) => Eq (Bar r)
Option 1. But it then tries to simplify the constraint, finding the minimal set of constraints that imply Eq (Foo r)
. Here, minimal does not mean smallest, but instead minimal in a logical sense -- as in, the minimum set of assumptions that proves the desired constraint. So, option 1 very quickly becomes option 2.
Note that if we didn't try to simplify, then you'd end up with constraints like Eq (Maybe a)
a lot, and these would be rejected.
In either case, since I *have* a matching
Eq
instance forFoo
, GHC should assume that I knew what I was doing when I wrote it, and just use it. This doesn't change the behavior when no matching instance is found, like in your example.
But you have no matching instance for C (F r)
. So I'm not sure how GHC should recognize the difference.
comment:4 Changed 4 years ago by
Without knowing anything about the internals of GHC, it seems there are two ways to simplify instance contexts: either we "simplify and reject" if they are "exotic" (in the case of GND instances), or just "simplify and typecheck" (in the case of hand-written instances of any variety). So if an instance head matches (Eq (Foo r)), trigger the "simplify and typecheck" rather than "simplify and reject exotic constraints" behavior.
I suppose the only reason we would fall into the second case is if there was no matching instance, which means GND would always just reject anyway. This all seems like reasonable behavior to me.
comment:5 Changed 4 years ago by
I'm sorry -- I'm afraid I don't understand your last comment. Or, rather, my understanding leads me directly to the behavior we currently have: check derived instances for exotic contexts and reject if exotic, but skip the exotic-check for hand-written instances (including standalone-deriving). (Note that there is no GND in sight here -- just normal deriving
.) Perhaps illustrate your idea with a few examples?
comment:6 follow-up: 7 Changed 4 years ago by
All I'm suggesting is that rather than the iterative process of
- GHC writes an instance
- GHC checks for a (single?) matching instance head for all constraints
- GHC simplifies those constraints
- Go to step 1 until minimal constraints found
(which I refer to as the "simplify and reject" method), GHC could get to step 3, and then just continue to simplify the constraints without checking for matching instances on all simplified constraints (i.e. more like how a function (presumably) simplifies constraints, which I refer to as the "simplify and typecheck" method, where no rejection occurs if no matching instance is found).
Thus GHC would still require a standalone instance for data X a b = MkX (a -> b) deriving Eq
because step (in the first round) would fail. The idea is that the above process would allow auto-deriving when a single matching instance is found for the unsimplified context. In the case of overlapping or missing instances, I have no opinion on the behavior.
Maybe this approach is too ad-hoc, but I think it would result in expected behavior.
My main reasons for this are that
- If there's a single instance in scope, GHC should assume I know how to use it.
- Writing the standalone instance
deriving instance (Eq (Foo r)) => Eq (Bar r)
does nothing to help me understand the exotic nature of the instance. [Not that I feel like I want advice in this area, mind you. I want GHC to assume I know what I'm doing.]
comment:7 follow-up: 8 Changed 4 years ago by
Replying to crockeea:
- GHC writes an instance
- GHC checks for a (single?) matching instance head for all constraints
- GHC simplifies those constraints
- Go to step 1 until minimal constraints found
I'm afraid I still don't understand. (I really don't! I'm not trying to be obtuse. It comes naturally.) Do you mean to go back to step 2? Then I think I understand.
(which I refer to as the "simplify and reject" method), GHC could get to step 3,
But now I'm lost again. How could we jump to step 3 without going through step 2? Step 2, as I understand it, is the step that actually finds a matching instance head, from which we can simplify. Step 3 would require the output of step 2 as its input. To be concrete, suppose we have a constraint Eq [(a, Int)]
. I understand step 2 as identifying the instance head Eq [b]
, which then, in step 3, uses its constraint Eq b
to simplify the original constraint to Eq (a, Int)
. So step 2 seems vital.
and then just continue to simplify the constraints without checking for matching instances on all simplified constraints (i.e. more like how a function (presumably) simplifies constraints, which I refer to as the "simplify and typecheck" method, where no rejection occurs if no matching instance is found).
This seems to suggest just omitting the "exotic constraint" check. Because functions don't have that check. Otherwise, I don't see a difference between what goes on with deriving
and what goes on with functions. The simplification algorithm looks the same to me.
Thus GHC would still require a standalone instance for
data X a b = MkX (a -> b) deriving Eq
because step (in the first round) would fail.
Which step did you mean?
The idea is that the above process would allow auto-deriving when a single matching instance is found for the unsimplified context. In the case of overlapping or missing instances, I have no opinion on the behavior.
Maybe this approach is too ad-hoc, but I think it would result in expected behavior.
My main reasons for this are that
- If there's a single instance in scope, GHC should assume I know how to use it.
- Writing the standalone instance
deriving instance (Eq (Foo r)) => Eq (Bar r)
does nothing to help me understand the exotic nature of the instance. [Not that I feel like I want advice in this area, mind you. I want GHC to assume I know what I'm doing.]
This part makes more sense to me. But then, consider the following:
data X a b = MkX (a -> b) deriving instance Eq (a -> b) => Eq (X a b) data Y a b = MkY (X a b) deriving Eq
My understanding tells me that this should work under your proposal. This is because Y
uses X
's instance, which GHC assumes is appropriate.
Maybe I can paraphrase your idea:
- GHC generates a set of constraints appropriate for deriving a given class. (That is, for
deriving (Eq X)
, this would beEq (a -> b)
.) These are all considered "unsimplified" constraints. - GHC tries to simplify all constraints. Any constraint produced as an output of simplification is considered "simplified". This step repeats until it can make no more progress.
- GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does not check "simplified" constraints.
- If there are no exotic "unsimplified" constraints, accept the declaration.
Is that about right?
comment:8 Changed 4 years ago by
Replying to goldfire:
I'm afraid I still don't understand. (I really don't! I'm not trying to be obtuse. It comes naturally.)
I'm quite sure your confusion is my fault. It's hard for me to talk reasonably about this since I know so little about how it works.
Do you mean to go back to step 2? Then I think I understand.
Yes, I did mean step 2.
But now I'm lost again. How could we jump to step 3 without going through step 2? Step 2, as I understand it, is the step that actually finds a matching instance head, from which we can simplify.
Ah, that makes sense. (Told you I don't know what I'm saying!) So GHC doesn't simplify constraints in functions? This is where the confusion arises for me. I can write:
foo a@(Foo _) = a == a
and GHC is perfectly happy to infer the context.
This seems to suggest just omitting the "exotic constraint" check. Because functions don't have that check.
Right! This is what I'm trying to get at.
Which step did you mean?
Step 2, where we check for a matching instance head.
But then, consider the following:
data X a b = MkX (a -> b) deriving instance Eq (a -> b) => Eq (X a b) data Y a b = MkY (X a b) deriving EqMy understanding tells me that this should work under your proposal. This is because
Y
usesX
's instance, which GHC assumes is appropriate.
Under my proposal, GHC would accept your example. And this makes sense to me: GHC has (rightly) forced me to write an "explicit" instance for X
(a standalone instance instead of an auto-derived one) which should tip me off that I'm doing something weird. At that point GHC has done its due diligence to warn me, it should then accept the instance for Y
without question.
Maybe I can paraphrase your idea:
- GHC generates a set of constraints appropriate for deriving a given class. (That is, for
deriving (Eq X)
, this would beEq (a -> b)
.) These are all considered "unsimplified" constraints.- GHC tries to simplify all constraints. Any constraint produced as an output of simplification is considered "simplified". This step repeats until it can make no more progress.
- GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does not check "simplified" constraints.
- If there are no exotic "unsimplified" constraints, accept the declaration.
Is that about right?
Well, almost. It seems that my original example would not be accepted with this algorithm because C (F r)
can't be simplified, but also doesn't have a matching instance. I'll try one more time:
- GHC generates a set of constraints for deriving a given class. (For example,
deriving (Eq X)
would generate the contextEq (a -> b)
. For the purposes of this algorithm, let's just use this example. - GHC tries to simplify the constraint
Eq (a -> b)
. If it can, go to step 3. Otherwise, throw an error and require StandaloneDeriving. - GHC found a matching instance for
Eq (a -> b)
(is this equivalent to "GHC was able to simplify the constraintEq (a -> b)
"?). Assume that the instanceEq (a -> b)
has already been simplified to something like(C a b) => Eq (a -> b)
. Then rewrite the auto-generated instance(Eq (a -> b)) => Eq (X a b)
to the already simplified instance(C a b) => Eq (X a b)
, without doing any checks on constraints(C a b)
at all. (They already typecheck, and since there is a matching instance, GHC will ignore anything exotic about it.)
Thanks for your patience while I try to figure out what I mean!
comment:9 Changed 4 years ago by
I think our algorithms are the same. Mine accepts your original example, because it simplifies Eq (Foo r)
to get C (F r)
, so in my terminology, C (F r)
is considered "simplified".
Now that we have an idea of what we're talking about, we can think about whether or not it is actually a good idea.
I'm inclined to think it is.
One tiny, easily-surmountable wrinkle is that we'd need to check for FlexibleContexts
and/or UndecidableInstances
and/or ... before accepting the constraint. But that's fairly routine.
I'd want Simon's opinion on this before rubber stamping it. And then there's the matter of implementation.
comment:10 Changed 4 years ago by
If you want an opinion, and you propose something different than what currently happens, can you write the wiki page?
Selfishly I don't want to wade through the long thread to find out what you are discussing.
Thanks
Simon
comment:11 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:12 Changed 10 months ago by
Keywords: | deriving added |
---|---|
Related Tickets: | → #15868 |
This is by design. GHC refuses to infer so-called exotic contexts, believing that sufficiently exotic contexts should be written by the user. This behavior is independent of whether GND or other
deriving
features are used. Here is an extreme example:This fails, complaining about a missing
Eq (a -> b)
instance. (My choice ofdata
vs.newtype
is utterly irrelevant here.) But I can write this:Should GHC infer the context automatically here? I think not -- it masks a deeper problem.
Now, returning to the original post: should GHC infer that context? It looks just like the example I just gave, where the context requires an
Eq
constraint on some other type constructor.It all boils down to yet another knob we can turn in the internals of GHC. It's a very easy knob to turn, with no interactions throughout the code. See the relevant function here, with a Note directly above.
If you can suggest a better setting for the knob, go right ahead. :)
Regardless, we should document this in the manual somewhere, as it is all user-facing.