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 bgamari)

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 adamgundry

Cc: adamgundry added

Somewhat surprisingly, this appears to be a valid workaround:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}

type family Scalar x

type family FieldScalar x where FieldScalar x = Field (Scalar x)

class FieldScalar x => Vector x

class Vector x => Field x

I suspect the "Cycle in class declaration (via superclasses)" error is a little bit too conservative.

comment:2 Changed 4 years ago by MikeIzbicki

Thanks! That workaround solves my immediate problem :)

comment:3 Changed 4 years ago by simonpj

See also #10318

comment:4 Changed 4 years ago by simonpj

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 MikeIzbicki

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 simonpj

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 MikeIzbicki

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:8 Changed 4 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:9 Changed 4 years ago by simonpj

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 bgamari

Description: modified (diff)

comment:11 Changed 4 years ago by bgamari

Status: newinfoneeded

comment:12 Changed 4 years ago by MikeIzbicki

Awesome! I have two comments:

  1. 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.
  1. 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 MikeIzbicki

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 simonpj

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 has Boolean (Logic a) as a superclass
  • Boolean a ultimately has Eq 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:15 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In ff752a1a/ghc:

tcCheckSatisfiability: less aggressive superclass expansion

In the pattern-match check we are looking for a proof of
*unsatisfiablity* among a bunch of givens.  The unsat-ness might be
hidden in the superclasses, so we must expand them.  But in the common
case where the constraints are satisfiable, we don't want to expand
a recursive superclass forever.

This is all a bit arbitrary, but then the whole question is
undecidable anyway.

The bug in Trac #10592 comment:12 was that I expanded superclasses
forever.  This patch fixes it.

comment:16 Changed 4 years ago by simonpj

MikeIzbicki: OK can you try again now?

comment:17 Changed 4 years ago by MikeIzbicki

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 simonpj

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 thomie

Milestone: 8.0.1
Resolution: fixed
Status: infoneededclosed
Test Case: typecheck/should_compile/T10592
Note: See TracTickets for help on using tickets.