[GHC] #11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.

[GHC]

#11523: Infinite Loop when mixing UndecidableSuperClasses and the class/instance
constraint synonym trick.
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:  simonpj
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |             Keywords:
      Resolution:                    |  UndecidableSuperClasses
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  polykinds/T11523
      Blocked By:                    |             Blocking:
 Related Tickets:  #11480            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > What if you take instances into account in considering when to
 terminate?

 That's a very interesting point.

 Currently, for each new "Given" (of which the potential superclasses are
 an example), GHC
  1. Rewrites it with currently available Given equalities, a kind of
 normalisation step
  2. And then sees if it is syntactically equal to one of the existing
 Givens.

 You are suggesting changing Step 2 to
  2. See if it is ''completely provable from'' the existing Givens and top-
 level instances

 That is an intriguing thought.  I say "completely" provable from because
 suppose you had
 {{{
    instance (C a, D a) => D (T a)
    [G] C a
 }}}
 and you were about to add `[G] D (T a)`.  The instance declaration
 applies, yielding sub-goals `(C a, D a)`.  We have `(C a)`, but not `D a`.
 So I think we then must abandon the attempt -- even if only one out of
 hundreds of sub-goals fails -- and add the proposed new Given after all.

 I worry a bit about solve order.  In the original example, suppose we
 added `[G] Category (Cod p)` ''before'' we added `Category p`.  If we were
 going to be solidly robust to solve order, whenever we added a new Given
 we'd have to check all the ''existing'' Givens to see if any of them could
 be proved from the new one (and the others).

 But perhaps we could apply this magic only to the superclass expansion
 step; for "normal" Givens it's at most an optimisation.

 Interesting!  I wonder if there are any other compelling examples.
 Edward??

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