Spurious superclass cycle error with type equalities
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’