Opened 2 years ago

Closed 2 years ago

#11067 closed bug (fixed)

Spurious superclass cycle error with type equalities

Reported by: oerjan Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.2
Keywords: Cc: oerjan, kylcarte@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_compile/T11067
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1594
Wiki Page:

Description (last modified by thomie)

Some of us today had an idea how to repair Edward Kmett's regrettably unsound Data.Constraint.Forall module. The method works fine in some cases, but seems to occasionally trigger a spurious superclass cycle error.

In the cases I've seen so far, it seems to happen when a class is defined with a Forall superclass, where that Forall itself has as parameter another class, that itself has a type equality superclass.

Example file (a bit larger than necessary to show how a similar example without a type equality doesn't give an error):

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.Monoid
import GHC.Exts (Constraint)

type family Skolem (p :: k -> Constraint) :: k
type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1

-- | A quantified constraint
type Forall (p :: k -> Constraint) = p (Skolem p)
type ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) = p (f (SkolemF p f))

-- These work
class ForallF Monoid t => Monoid1 t
instance ForallF Monoid t => Monoid1 t

class ForallF Monoid1 t => Monoid2 t
instance ForallF Monoid1 t => Monoid2 t

-- Changing f a ~ g a to, (Ord (f a), Ord (g a)), say, removes the error
class (f a ~ g a) => H f g a
instance (f a ~ g a) => H f g a

-- This one gives a superclass cycle error.
class Forall (H f g) => H1 f g
instance Forall (H f g) => H1 f g

And the resulting error:

Test.hs:31:1:
    Cycle in class declaration (via superclasses):
      H1 -> Forall -> H -> H
    In the class declaration for ‘H1’

Test.hs:31:1:
    Cycle in class declaration (via superclasses):
      H1 -> Forall -> H -> H
    In the class declaration for ‘H1’

Change History (17)

comment:1 Changed 2 years ago by oerjan

Cc: oerjan added

comment:2 Changed 2 years ago by oerjan

András Kovács found a workaround for our use case: The error disappears if Forall etc. are made type synonym families rather than plain synonyms.

comment:3 Changed 2 years ago by dfeuer

Component: CompilerCompiler (Type checker)
Milestone: 8.0.1

comment:4 Changed 2 years ago by oerjan

To prevent the Skolem from leaking via pattern matching, I had to change Forall to use a type class instead. I first tried

class p (Skolem p) => Forall (p :: k -> Constraint)
instance p (Skolem p) => Forall (p :: k -> Constraint)

etc., but this made the cycle errors come back, even more widespread than before (Monoid2 no longer worked). However, adding a closed type family in the right spot again worked to soothe GHC:

type family Forall (p :: k -> Constraint) where
    Forall p = Forall_ p
class p (Skolem p) => Forall_ (p :: k -> Constraint)
instance p (Skolem p) => Forall_ (p :: k -> Constraint)

This seems a bit silly :P

(Also, the last instance above should have a Forall_, but the _ is invisible, at least in preview...)

comment:5 Changed 2 years ago by oerjan

After meditating on the 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 Skolems 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.

comment:6 Changed 2 years ago by thomie

Description: modified (diff)

Your example seemed to be missing a FlexibleContexts pragma, so I added it.

comment:7 Changed 2 years ago by simonpj

See also #10592, #10318.

comment:8 Changed 2 years ago 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.

comment:9 in reply to:  8 Changed 2 years ago by oerjan

Replying to 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 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.
  1. I 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.

comment:10 Changed 2 years ago by oerjan

I just learned that the author of the type-combinators package has found the "design pattern" of associated type family superclasses very useful.

comment:11 Changed 2 years ago by simonpj

Cc: kylcarte@… added

Can I ask: does wip/T11067 make it easier? It's pretty simple: with UndecidableSuperClasses the whole superclass restriction is lifted.

Adding kylcarte@… in cc, who is the author of type-combinators

Simon

comment:12 Changed 2 years ago by bgamari

Differential Rev(s): Phab:D1594

comment:13 in reply to:  11 Changed 2 years ago by oerjan

Replying to simonpj:

Can I ask: does wip/T11067 make it easier? It's pretty simple: with UndecidableSuperClasses the whole superclass restriction is lifted.

From reading the notes, that sounds promising (although I think I found an error, will try to comment on that in Phab).

I do have a hunch there's a bit of a potential annoyance, though: With something like UndecidableInstances, only the module declaring the instance needs to enable the extension. But the cycle check for superclasses is not locally restricted to the declaration "responsible" for the rule violation. If I'm understanding the notes correctly, if a class requires the extension, then any other class using it as a superclass also will.

So a module such as Data.Constraint.Forall cannot just itself use UndecidableSuperClasses and thereby free the users from having to mention it.

E.g. I suspect users would have to enable the extension explicitly in their own code to use a ForallV superclass (because ForallV has a type family superclass) or a nested ForallF superclass (because that would recurse on the ForallF, although in this case the "blame" might be more shared.)

comment:14 Changed 2 years ago by simonpj

OK good. I think I'll commit as-is (time is pressing), and leave a potential relaxation along the lines of comment:13 for later. By all means make a concrete proposal.

An improvement along the same lines would be to have a per-class pragma (like instance overlap) rather than a per-module language extension.

Last edited 2 years ago by simonpj (previous) (diff)

comment:15 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In 6eabb6d/ghc:

Allow recursive (undecidable) superclasses

This patch fulfils the request in Trac #11067, #10318, and #10592,
by lifting the conservative restrictions on superclass constraints.

These restrictions are there (and have been since Haskell was born) to
ensure that the transitive superclasses of a class constraint is a finite
set.  However (a) this restriction is conservative, and can be annoying
when there really is no recursion, and (b) sometimes genuinely recursive
superclasses are useful (see the tickets).

Dimitrios and I worked out that there is actually a relatively simple way
to do the job. It’s described in some detail in

   Note [The superclass story] in TcCanonical
   Note [Expanding superclasses] in TcType

In brief, the idea is to expand superclasses only finitely, but to
iterate (using a loop that already existed) if there are more
superclasses to explore.

Other small things

- I improved grouping of error messages a bit in TcErrors

- I re-centred the haddock.compiler test, which was at 9.8%
  above the norm, and which this patch pushed slightly over

comment:16 Changed 2 years ago by simonpj

Test Case: indexed-types/should_compile/T11067

Ok this is done! I'd love you to try it out to check that it works.

Simon

comment:17 Changed 2 years ago by bgamari

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.