[GHC] #11067: Spurious superclass cycle error with type equalities

[GHC]

#11067: Spurious superclass cycle error with type equalities
-------------------------------------+-------------------------------------
        Reporter:  oerjan            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by oerjan):

 After meditating on the
 [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/type-
 class-extensions.html#superclass-rules User's Guide's]

  "A superclass context for a class C is allowed if, after expanding type
 synonyms to their right-hand-sides, and uses of classes (other than C) to
 their superclasses, C does not occur syntactically in the context."

 I've concluded that the behavior I'm seeing, even if strange, is exactly
 as advertised. Type families and equations are not expanded, but their
 arguments are checked for whether a class occurs cyclically there.

 Thus dependent on where in the hierarchy it is placed, a type family can
 either:
 * prevent cycle detection by hiding the cyclic use inside an instance (and
 our workaround in the new `Data.Constraint.Forall` depends on this), or
 * trigger spurious cycle detection by one of its arguments containing a
 class that is never actually be used as a constraint. (In our case, the
 `Skolem`s are essentially phantom type arguments.)

 On the plus side, the first case can be used to encode superclass
 recursion when GHC does not otherwise understand that it is harmless.

 On the minus side, the first case can probably get GHC's constraint
 resolution to loop if there actually *is* a real constraint cycle or
 infinite expansion.

 (Wild idea: would it be possible to use lazy breadth first search to make
 some infinite superclass hierarchies actually work?)

 However, I would say the plus side is big: there really *should* be a way
 for the programmer to encode a terminating superclass recursion if they
 know what they're doing.  Of course a more intentionally enabled method
 might be better.

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