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

 In your example GHC is being stupidly conservative.  Consider the
 superclasses of `(H1 f g)`:
 {{{
 transitive superclasses of (H1 f g)
  = (by immediate superclsases of H1)
    Forall (H f g)
  = (expand Forall)
    H f g (Skolem (H f g))
  = (superclasses of H)
    f (Skolem (H f g)) ~ g (Skolem (H f g))
 }}}
 And there the process stops.  Once we get to an ''equality'' we can't go
 further.  We do not have an infinite tower of superclasses, and that is
 statically visible.  GHC is probably worried about the occurrences of `H`
 on the bottom line, but it shouldn't be.

 That would (probably) be fairly easy to fix.

 The possibility of type functions in a "superclass" position is more
 worrying.  As you point out, the type function could hide arbitrary
 recursion and indeed loops could result.  I'm strongly inclined to make
 type function in superclass positions illegal:
 {{{
 class F ty => C a
 }}}
 would be illegal if `F` is a type function. However
 {{{
 class D (F ty) => C a
 }}}
 would be ok (c.f. #10318).

 I have yet to see a good reason for a type function in head position,
 except to work around bugs.  Maybe we could allow it with some suitably
 terrifying-sounding extension.

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