[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 goldfire):

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

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