[GHC] #11008: Difficulties around inferring exotic contexts

[GHC]

#11008: Difficulties around inferring exotic contexts
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by crockeea):

 Replying to [comment:7 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!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11008#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler