Opened 2 years ago
Closed 22 months 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 )
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
Cc: | oerjan added |
---|
comment:2 Changed 2 years ago by
comment:3 Changed 2 years ago by
Component: | Compiler → Compiler (Type checker) |
---|---|
Milestone: | → 8.0.1 |
comment:4 Changed 2 years ago by
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
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
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.
comment:6 Changed 2 years ago by
Description: | modified (diff) |
---|
Your example seemed to be missing a FlexibleContexts
pragma, so I added it.
comment:8 follow-up: 9 Changed 23 months ago by
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 Changed 23 months ago by
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 awould be illegal if
F
is a type function. Howeverclass D (F ty) => C awould 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:
- 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 ofTypeable
for the parts of a type or kind. Which in some ways ended up more flexible than the implementation GHC currently has, thus #10343.
- 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 22 months ago by
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 follow-up: 13 Changed 22 months ago by
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 22 months ago by
Differential Rev(s): | → Phab:D1594 |
---|
comment:13 Changed 22 months ago by
Replying to simonpj:
Can I ask: does
wip/T11067
make it easier? It's pretty simple: withUndecidableSuperClasses
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 22 months ago by
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.
comment:16 Changed 22 months ago by
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 22 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
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.