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 Changed 4 years ago by goldfire

Summary: GND with Type FamiliesDifficulties around inferring exotic contexts

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:

data X a b = MkX (a -> b) deriving Eq

This fails, complaining about a missing Eq (a -> b) instance. (My choice of data vs. newtype is utterly irrelevant here.) But I can write this:

deriving instance Eq (a -> b) => Eq (X a b)

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.

comment:2 in reply to:  1 ; Changed 4 years ago by crockeea

With the deriving clause, which instance does GHC try to create?

  1. instance (Eq (Foo r)) => Eq (Bar r)
  2. 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 in reply to:  2 Changed 4 years ago by goldfire

Replying to crockeea:

With the deriving clause, which instance does GHC try to create?

  1. instance (Eq (Foo r)) => Eq (Bar r)
  2. 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 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.

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 crockeea

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.

Last edited 4 years ago by crockeea (previous) (diff)

comment:5 Changed 4 years ago by goldfire

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 Changed 4 years ago by crockeea

All I'm suggesting is that rather than the iterative process of

  1. GHC writes an instance
  2. GHC checks for a (single?) matching instance head for all constraints
  3. GHC simplifies those constraints
  4. 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

  1. If there's a single instance in scope, GHC should assume I know how to use it.
  2. 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 in reply to:  6 ; Changed 4 years ago by goldfire

Replying to crockeea:

  1. GHC writes an instance
  2. GHC checks for a (single?) matching instance head for all constraints
  3. GHC simplifies those constraints
  4. 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

  1. If there's a single instance in scope, GHC should assume I know how to use it.
  2. 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:

  1. GHC generates a set of constraints appropriate for deriving a given class. (That is, for deriving (Eq X), this would be Eq (a -> b).) These are all considered "unsimplified" constraints.
  2. 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.
  3. GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does not check "simplified" constraints.
  4. If there are no exotic "unsimplified" constraints, accept the declaration.

Is that about right?

comment:8 in reply to:  7 Changed 4 years ago by crockeea

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 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.

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:

  1. GHC generates a set of constraints appropriate for deriving a given class. (That is, for deriving (Eq X), this would be Eq (a -> b).) These are all considered "unsimplified" constraints.
  2. 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.
  3. GHC checks the "unsimplified" constraints, if there are any left, to make sure they are not exotic. It does not check "simplified" constraints.
  4. 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:

  1. GHC generates a set of constraints for deriving a given class. (For example, deriving (Eq X) would generate the context Eq (a -> b). For the purposes of this algorithm, let's just use this example.
  2. GHC tries to simplify the constraint Eq (a -> b). If it can, go to step 3. Otherwise, throw an error and require StandaloneDeriving.
  3. GHC found a matching instance for Eq (a -> b) (is this equivalent to "GHC was able to simplify the constraint Eq (a -> b)"?). Assume that the instance Eq (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 goldfire

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 simonpj

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 RyanGlScott

Cc: RyanGlScott added

comment:12 Changed 10 months ago by RyanGlScott

Keywords: deriving added
Note: See TracTickets for help on using tickets.