#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