Opened 4 years ago
Last modified 17 months ago
#11523 new bug
Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.
Reported by: | ekmett | Owned by: | simonpj |
---|---|---|---|
Priority: | high | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.0.1-rc1 |
Keywords: | UndecidableSuperClasses | Cc: | simonpj, Iceland_jack, aaronvargo |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | polykinds/T11523 |
Blocked By: | Blocking: | ||
Related Tickets: | #11480 | Differential Rev(s): | |
Wiki Page: |
Description
There seems to be a bad interaction between UndecidableSuperClasses
and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level:
class (Foo f, Bar f) => Baz f instance (Foo f, Bar f) => Baz f
Unfortunately, there are circumstances in which you can't eliminate it, such as
class (p, q) => p & q instance (p, q) => p & q
There we can't partially apply (,) at the constraint level, but we can talk about (&) :: Constraint -> Constraint -> Constraint
and (&) (Eq a) :: Constraint -> Constraint
.
This doesn't seem to happen on simpler examples like the above, but once I modify the categories example from #11480 to move the domain and codomain of a functor into class associated types, so that they don't infect every single subclass of functor, we run into a problem. The following stripped down version of the code seems to send the compiler into an infinite loop:
{-# language KindSignatures #-} {-# language PolyKinds #-} {-# language DataKinds #-} {-# language TypeFamilies #-} {-# language RankNTypes #-} {-# language NoImplicitPrelude #-} {-# language FlexibleContexts #-} {-# language MultiParamTypeClasses #-} {-# language GADTs #-} {-# language ConstraintKinds #-} {-# language FlexibleInstances #-} {-# language TypeOperators #-} {-# language ScopedTypeVariables #-} {-# language DefaultSignatures #-} {-# language FunctionalDependencies #-} {-# language UndecidableSuperClasses #-} {-# language UndecidableInstances #-} {-# language TypeInType #-} import GHC.Types (Constraint, Type) import qualified Prelude type Cat i = i -> i -> Type newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a } class Vacuous (a :: i) instance Vacuous a class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where type Op p :: Cat i type Op p = Y p type Ob p :: i -> Constraint type Ob p = Vacuous class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where type Dom f :: Cat i type Cod f :: Cat j class (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j) instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Fun p q instance (Category p, Category q) => Functor (Nat p q) where type Dom (Nat p q) = Y (Nat p q) type Cod (Nat p q) = Nat (Nat p q) (->) instance (Category p, Category q) => Functor (Nat p q f) where type Dom (Nat p q f) = Nat p q type Cod (Nat p q f) = (->) instance Category (->) instance Functor ((->) e) where type Dom ((->) e) = (->) type Cod ((->) e) = (->) instance Functor (->) where type Dom (->) = Y (->) type Cod (->) = Nat (->) (->) instance (Category p, Op p ~ Y p) => Category (Y p) where type Op (Y p) = p instance (Category p, Op p ~ Y p) => Functor (Y p a) where type Dom (Y p a) = Y p type Cod (Y p a) = (->) instance (Category p, Op p ~ Y p) => Functor (Y p) where type Dom (Y p) = p type Cod (Y p) = Nat (Y p) (->)
Here I need the circular definition of Fun
to talk about the fact that the objects in the category of natural transformations from a category p to a category q are functors with domain p and codomain q, so to give the definition of the class-associated type Ob (Nat p q)
I need such a cyclic definition.
I can't leave the domain and codomain of Functor
in fundeps, otherwise if I go to define a subclass of Functor I'd have to include the arguments, and I have a lot of those subclasses!
Attachments (1)
Change History (33)
comment:1 Changed 4 years ago by
comment:3 Changed 4 years ago by
Version: | 7.10.3 → 8.0.1-rc1 |
---|
comment:6 Changed 4 years ago by
Status: | new → merge |
---|---|
Test Case: | → polykinds/T11523 |
I believe I've fixed this. I'm sorry I missed the RC2 bus.
Simon
Changed 4 years ago by
Attachment: | Categories.hs added |
---|
a test case that is still failing after february 8th patches
comment:8 Changed 4 years ago by
Attempting to compile the attachment I just submitted now crashes ghc
HEAD with the following rather uninformative error message:
*** Exception: No match in record selector ctev_dest
I haven't cut down the example, yet, however.
comment:9 Changed 4 years ago by
Ah, that's #11401, which Richard hasn't got to yet. So, progress of a sort.
comment:10 Changed 4 years ago by
Cc: | Iceland_jack added |
---|
comment:11 Changed 4 years ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
This was merged in aa830b1e709bb65353045e27f163ace4752da265.
comment:12 Changed 4 years ago by
Resolution: | fixed |
---|---|
Status: | closed → new |
The example I attached after the february 8th patch still doesn't compile.
The ctev_dest
crash was masking a completely different blowup.
That said, it may not be for this issue, but for something else.
comment:13 Changed 4 years ago by
Adding p ~ Op (Op p)
) to the superclass constraints of Category
in Categories.hs drastically reduces the size of the unresolved wanteds, but they never seem to go away.
comment:14 follow-up: 28 Changed 4 years ago by
The undecideable superclasses thing has the following property:
- If you have a type error (a wanted that genuinely cannot be solved)
- and you have an infinite number of superclasses
then the typechecker will diverge, or at least complain about too many iterations.
In this case, do you think that there is a finite tower of superclasses? I get
[G] Category p +-> {add superclasses} Functor p Dom p ~ Op p Cod p ~ Nat p (->) Ob (Op p) ~ Ob p +-> {add superclasse of Functor} Category (Dom p) Cateogory (Cod p)
and now we merrily go round. Adding p ~ Op (Op p)
will help, because Dom p ~ Op p
. But we are still going to get Cateogry (Cod p)
, Category (Cod (Cod p))
and so on. Is that really what you intend?
Actually we get a hand without "too many iterations", which is odd, but still I'd like to know the answer to the above.
comment:16 follow-up: 17 Changed 4 years ago by
Brought up on #ghc, are there technical reasons why (,)
cannot be partially applied with the same meaning as (&)
?
comment:17 follow-up: 18 Changed 4 years ago by
Replying to Iceland_jack:
Brought up on #ghc, are there technical reasons why
(,)
cannot be partially applied with the same meaning as(&)
?
I'm lost. What is (&)
? How is this connected with this ticket?
comment:18 Changed 4 years ago by
Replying to simonpj:
Replying to Iceland_jack:
Brought up on #ghc, are there technical reasons why
(,)
cannot be partially applied with the same meaning as(&)
?I'm lost. What is
(&)
? How is this connected with this ticket?
(&) :: Constraint -> Constraint -> Constraint
is defined by
class (p, q) => p & q instance (p, q) => p & q
at the beginning of this ticket. This would actually be solved by #11715 (per your comment ticket:11715#comment:14)
- Allow partial applications like
(,) (Eq a) :: Constraint -> Constraint
comment:19 Changed 4 years ago by
I would have thought that if we're not hitting a fixed point in the attached example, we'd have a similar breakage in the example in the description, because we'd see the same tower of Nat's there, but that stripped down version compiles just fine.
Is this something that only comes up when I use constraints like this somehow?
comment:20 Changed 4 years ago by
comment:14 explains why there is no fixed point. Did the explanation make sense? Do you think there is a fixed point? The existence or otherwise of a fixpoint should not be related to how you use constraints.
Simon
comment:21 Changed 4 years ago by
Milestone: | 8.0.1 → 8.2.1 |
---|---|
Priority: | highest → high |
I'm going to move this off the 8.0 milestone. I claim it's behaving as advertised, and no one is disputing that claim.
By all means bring it back if you disagree.
Simon
comment:22 Changed 4 years ago by
I've yet to figure out why the shorter example passes, but the longer, which doesn't seem to change the part that spins forever fails.
No objection to moving this out to 8.2 though.
comment:23 Changed 4 years ago by
I've yet to figure out why the shorter example passes, but the longer, which doesn't seem to change the part that spins forever fails.
I explain precisely this in comment:14 above. You (implicitly) claim that there is a finite number of superclasses. I claim the contrary. We can't both be right :-).
Maybe there's a bug in the example Categories.h
? That's my current belief.
comment:25 Changed 3 years ago by
Owner: | set to simonpj |
---|
comment:26 Changed 3 years ago by
Edward says "I can't check particulars right now. I can definitely say I'd like some way to attain an equivalent result, but I accept that it may not be possible with the machinery we have."
comment:27 Changed 3 years ago by
Milestone: | 8.2.1 → 8.4.1 |
---|
Regardless, this certainly won't be addressed for 8.2.
comment:28 Changed 17 months ago by
Replying to simonpj:
In this case, do you think that there is a finite tower of superclasses? I get
[G] Category p +-> {add superclasses} Functor p Dom p ~ Op p Cod p ~ Nat p (->) Ob (Op p) ~ Ob p +-> {add superclasse of Functor} Category (Dom p) Cateogory (Cod p)and now we merrily go round. Adding
p ~ Op (Op p)
will help, becauseDom p ~ Op p
. But we are still going to getCateogry (Cod p)
,Category (Cod (Cod p))
and so on. Is that really what you intend?
What if you take instances into account in considering when to terminate? Then the tower is finite, since Category (Cod p)
is a consequence of:
Category p Cod p ~ Nat p (->) instance (Category p, Category q) => Category (Nat p q) instance Category (->)
and so the fact that Category (Cod p)
is a superclass provides no new information, and thus there's no need to go any further.
This also suggests a slightly ugly work-around, which indeed seems to work (at least in this case):
-- Functor without Category (Cod f) class Category (Dom f) => Functor' (f :: i -> j) -- Functor with Category (Cod f) class (Functor' f, Category (Cod f)) => Functor f instance (Functor' f, Category (Cod f)) => Functor f -- only require Functor', since Category (Cod p) is already implied class ( Functor' p , Dom p ~ Op p , Cod p ~ Nat p (->) , Ob (Op p) ~ Ob p , Op (Op p) ~ p ) => Category (p :: Cat i)
Tangentially, there's also really no need for Op p
, since it's just equal to Dom p
, and so Category
can be simplified to:
class ( Functor' p , Cod p ~ Nat p (->) , Dom (Dom p) ~ p , Ob (Dom p) ~ Ob p ) => Category (p :: Cat i)
comment:29 Changed 17 months ago by
What if you take instances into account in considering when to terminate?
That's a very interesting point.
Currently, for each new "Given" (of which the potential superclasses are an example), GHC
- Rewrites it with currently available Given equalities, a kind of normalisation step
- And then sees if it is syntactically equal to one of the existing Givens.
You are suggesting changing Step 2 to
- See if it is completely provable from the existing Givens and top-level instances
That is an intriguing thought. I say "completely" provable from because suppose you had
instance (C a, D a) => D (T a) [G] C a
and you were about to add [G] D (T a)
. The instance declaration applies, yielding sub-goals (C a, D a)
. We have (C a)
, but not D a
. So I think we then must abandon the attempt -- even if only one out of hundreds of sub-goals fails -- and add the proposed new Given after all.
I worry a bit about solve order. In the original example, suppose we added [G] Category (Cod p)
before we added Category p
. If we were going to be solidly robust to solve order, whenever we added a new Given we'd have to check all the existing Givens to see if any of them could be proved from the new one (and the others).
But perhaps we could apply this magic only to the superclass expansion step; for "normal" Givens it's at most an optimisation.
Interesting! I wonder if there are any other compelling examples. Edward??
comment:30 Changed 17 months ago by
Are QuantifiedConstraints
another thing to consider here? The proposed magic would properly account for them as well, while the current rules presumably ignore them the same way they ignore top-level instances.
comment:31 Changed 17 months ago by
I guess so. Can you offer an example?
So far we we have precisely one example needing the magic... more examples would strengthen the case for making a change.
comment:32 Changed 17 months ago by
Cc: | aaronvargo added |
---|
(It apparently isn't infinite, the compiler eventually runs out of memory and crashes.)