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

 Replying to [comment:8 simonpj]:

 First, I don't think #10592 and #10318 are that relevant, because there is
 no ''actual'' infinite recursion involved, it's all terminating. Not that
 it wouldn't be nice to support true infinite recursion, too, if it were
 possible.

 > That would (probably) be fairly easy to fix.

 Unfortunately this is only a special case of the problem, where I first
 discovered it.

 > 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).

 Disallowing this without changing a lot more would kill
 `Data.Constraint.Forall` (again), because removing all the superclass type
 functions doesn't currently work either. The problem, as my comment
 [comment:4] implies, is that even with just `ConstraintKinds` and no type
 function classes, it is still possible to create terminating recursion:

 {{{
 Monoid2 t => ForallF Monoid1 t
 => Monoid1 (t (SkolemF Monoid1 t))
 => ForallF Monoid (t (SkolemF Monoid1 t))
 => Monoid (t (SkolemF Monoid t)) (SkolemF Monoid (t (SkolemF Monoid1 t))))
 }}}

 (modulo errors, my own computer is in for repairs so I cannot test).

 The only thing that should have to be a type family here is the `SkolemF`,
 and this works perfectly with `ForallF` as a class, ''except'' for GHC's
 cycle error. Inserting a type function in the chain currently allows it to
 work, as in the current `constraints` implementation.

 > 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.

 I'm just a hobbyist Haskeller, discussing more than programming, and maybe
 my mind works differently, but I think type function superclasses may have
 severely ''underused'' potential. As far as I know, they're the only way
 to make the superclasses of a class vary "dynamically", in a way that
 sometimes gives ''much'' better type inference than just putting the
 constraints on an instance.

 I can think of twice I've been using type function superclasses for non-
 buggy reasons:

 1. Back in the #9858 discussion, I dabbled with how to express kind-aware
 `Typeable` in plain GHC 7.8 terms.  An associated type function superclass
 was essential to get reasonable type inference of `Typeable` for the parts
 of a type or kind. Which in some ways ended up ''more'' flexible than the
 implementation GHC currently has, thus #10343.

 2. I [https://github.com/ekmett/constraints/pull/17 proposed] another
 addition to `Data.Constraint.Forall`, a varargs convenience class to deal
 with the awkwardness of quantifying over several type variables
 simultaneously:

 {{{
 class ForallV' p => ForallV (p :: k)
 instance ForallV' p => ForallV p

 type family ForallV' (p :: k) :: Constraint
 type instance ForallV' (p :: Constraint) = p
 type instance ForallV' (p :: k -> Constraint) = Forall p
 type instance ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p

 class InstV (p :: k) c | k c -> p where
     instV :: ForallV p :- c

 -- Omitting instances
 }}}

 `ForallV` must be a class, otherwise the corresponding `instV` method
 cannot be type inferred. (Also, it's used as an unapplied argument in the
 last line, but ''that'' can be got around, I think, by making it more
 point-free.) `ForallV'` must be a superclass type function, because the
 implementation is genuinely branching on kind. And `ForallV` is intended
 to be used for constraints, ''including'' as a superclass. (I suppose
 ''injective'' families could do everything but the last bit.)

 ----

 It seems to me that the superclass cycle detection works fine ''without''
 `ConstraintKinds`, but with it, you immediately run into the problem:

 The superclass cycle detection seems to be designed on the assumption: "a
 class is used twice in a superclass chain" and "the superclass chain
 doesn't terminate" are equivalent.

 With `ConstraintKinds`, this assumption ''fails'', spectacularly.

 Type families exacerbate this problem, by making it much easier to express
 (and want to express) genuine terminating recursion of types, but they do
 ''not'' fundamentally cause it.

 I don't understand why a superclass "cycle" should not be handled in
 exactly the same way as ordinary instance lookup, as far as termination is
 concerned. `UndecidableInstances` could work analogously with both, by
 only triggering an error when there is an actual, ''certain'' blowup.

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