Opened 4 years ago
Closed 4 years ago
#10592 closed feature request (fixed)
Allow cycles in class declarations
Reported by: | MikeIzbicki | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.0.1 |
Component: | Compiler (Type checker) | Version: | 7.10.1 |
Keywords: | Cc: | adamgundry | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T10592 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
In particular, I would like to have a class hierarchy that looks like:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} type family Scalar x class Field (Scalar x) => Vector x class Vector x => Field x
It is the case that every field is a vector, and the scalar associated with every vector is a field. But we can't currently enforce that.
Change History (19)
comment:1 Changed 4 years ago by
Cc: | adamgundry added |
---|
comment:4 Changed 4 years ago by
Hmm. I think it'd be easy to send GHC into an infinite loop using this; i.e. the current implementation is over-liberal.
type instance FieldScalar x = Field x
Is it true that you expect Scalar (Scalar a) ~ Scalar a)
(cf #10318). If so, you could make it better behaved by saying
class (Scalar (Scalar a) ~ Scalar a, Field (Scalar a)) => Vector a class Vector x => Field x
This still isn't accepted but could be under comment:6 of #10318
comment:5 Changed 4 years ago by
I actually tried the technique on my current code base and it did appear GHC went into an infinite loop. I didn't report it here though because I wasn't sure exactly what was going on and I haven't had a chance to look into it more fully.
I'm not sure what you mean by this could be accepted with regards to comment:6 of #10318. There's a lot going on in that thread, and it's hard for me to get a good grasp of what's relevant. I basically know nothing about how type inference actually works, I'm just a big fan of using it :)
comment:6 Changed 4 years ago by
The stuff in #10318 is speculation about a possible feature. But the question remains: in your application If
class (Scalar (Scalar a) ~ Scalar a, Field (Scalar a)) => Vector a class Vector x => Field x
was accepted by GHC, would it serve your purpose? That means that in any instance of Vector t
, GHC will need to prove that Scalar (Scalar t) ~ Scalar t
. Will that be true, in your application?
If so, that makes the speculation in #10318 more persuasive.
comment:7 Changed 4 years ago by
My current implementation has constraints that look exactly like this, plus a lot more related to other aspects of the class hierarchy. So supporting this would be a necessary condition for me cyclic class declarations for me, but I can't say for sure if it would be sufficient (but my guess is probably).
comment:9 Changed 4 years ago by
MikeIzbicki: OK so this is implemented!
Could you give a test case, perhaps that can run? Simply accepting the above code isn't really a good test :-).
Simon
comment:10 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:11 Changed 4 years ago by
Status: | new → infoneeded |
---|
comment:12 Changed 4 years ago by
Awesome! I have two comments:
- One of my use cases is very similar to the code attached below, which causes GHC to loop. The code provides an alternate class hierarchy for comparisons. One of the features of the hierarchy is that
(||)
and(&&)
can be used directly on functions. Unfortunately, the instances for(->)
cause GHC to loop. The instances seem like they should work to me. I'm not sure if my reasoning is faulty or if there's a bug in the implementation.
- I believe there is an incorrect error message. If you take the code below and comment out the line
instance Boolean b => Boolean (a -> b)
, then GHC gives the error message:[1 of 1] Compiling ClassCycles ( ClassCycles.hs, ClassCycles.o ) ClassCycles.hs:1:1: error: solveWanteds: too many iterations (limit = 4) Set limit with -fsolver-iterations=n; n=0 for no limit WC {wc_simple = [W] $dBoolean_a1KZ :: Boolean (a -> fsk_a1KH) (CDictCan) [D] _ :: Boolean (a -> fsk_a1Ll) (CDictCan)}
But when I try to set the limit to something different, GHC complains that the flag doesn't exist:
$ ~/proj/ghc/inplace/bin/ghc-stage2 ClassCycles.hs -fsolver-iterations=10 ghc-stage2: unrecognised flag: -fsolver-iterations=10 Usage: For basic information, try the `--help' option
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableSuperClasses #-} module ClassCycles where import Prelude (Bool(True,False),Integer,Ordering) import qualified Prelude -------------------- -- class hierarchy class Boolean (Logic a) => Eq a where type Logic a :: * (==) :: a -> a -> Logic a class Eq a => POrd a where inf :: a -> a -> a class POrd a => MinBound a where minBound :: a class POrd a => Lattice a where sup :: a -> a -> a class (Lattice a, MinBound a) => Bounded a where maxBound :: a class Bounded a => Complemented a where not :: a -> a class Bounded a => Heyting a where infixr 3 ==> (==>) :: a -> a -> a class (Complemented a, Heyting a) => Boolean a (||) :: Boolean a => a -> a -> a (||) = sup (&&) :: Boolean a => a -> a -> a (&&) = inf -------------------- -- Bool instances -- (these work fine) instance Eq Bool where type Logic Bool = Bool (==) = (Prelude.==) instance POrd Bool where inf True True = True inf _ _ = False instance MinBound Bool where minBound = False instance Lattice Bool where sup False False = False sup _ _ = True instance Bounded Bool where maxBound = True instance Complemented Bool where not True = False not False = True instance Heyting Bool where False ==> _ = True True ==> a = a instance Boolean Bool -------------------- -- Integer instances -- (these work fine) instance Eq Integer where type Logic Integer = Bool (==) = (Prelude.==) instance POrd Integer where inf = Prelude.min instance Lattice Integer where sup = Prelude.max -------------------- -- function instances -- (these cause GHC to loop) instance Eq b => Eq (a -> b) where type Logic (a -> b) = a -> Logic b f==g = \a -> f a == g a instance POrd b => POrd (a -> b) where inf f g = \a -> inf (f a) (g a) instance MinBound b => MinBound (a -> b) where minBound = \_ -> minBound instance Lattice b => Lattice (a -> b) where sup f g = \a -> sup (f a) (g a) instance Bounded b => Bounded (a -> b) where maxBound = \_ -> maxBound instance Complemented b => Complemented (a -> b) where not f = \a -> not (f a) instance Heyting b => Heyting (a -> b) where f ==> g = \a -> f a ==> g a instance Boolean b => Boolean (a -> b)
comment:13 Changed 4 years ago by
I've found another suspicious edge case. GHC will loop if you use the same code above, but add the (/=)
function to the Eq
class as follows:
class Boolean (Logic a) => Eq a where type Logic a :: * (==) :: a -> a -> Logic a (/=) :: a -> a -> Logic a a/=b = not (a==b)
comment:14 Changed 4 years ago by
OK I've got it. Patch coming.
Your example differs from Edward's in #10318, because you really do have an infinite stack of superclasses.
Eq a
hasBoolean (Logic a)
as a superclassBoolean a
ultimately hasEq a
as a superclass
So we get Eq (Logic a)
, Eq (Logic (Logic a))
, etc forever.
Do you really mean that. Edward cut this off by adding a constraint
Frac (Frac a) ~ Frac a
Can you do something like that for Logic
?
If you really really do have infinitely many superclasses then unsolved constraints will indeed hit the iteration limit as you found... GHC keeps adding superclasses in the hope of finding one that works, but there are infinitely many of them (I fixed the error message to give the right flag name, but it doesn't solve the problem). I don't see any way to solve this without you giving GHC some way to bound the tower as Edward did.
comment:17 Changed 4 years ago by
Okay, I understand the limitations a bit better now. Adding the Logic a ~ Logic (Logic a)
constraint makes it work for me.
comment:18 Changed 4 years ago by
Well, you only want to add that constraint if it's actually true -- that is, if you intend that Logic
is idempotent.
But hurrah anyway.
Simon
comment:19 Changed 4 years ago by
Milestone: | → 8.0.1 |
---|---|
Resolution: | → fixed |
Status: | infoneeded → closed |
Test Case: | → typecheck/should_compile/T10592 |
Somewhat surprisingly, this appears to be a valid workaround:
I suspect the
"Cycle in class declaration (via superclasses)"
error is a little bit too conservative.