[GHC] #11067: Spurious superclass cycle error with type equalities

[GHC]

#11067: Spurious superclass cycle error with type equalities
-------------------------------------+-------------------------------------
        Reporter:  oerjan            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.10.2
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Old description:

> 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):
> {{{#!haskell
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE ConstraintKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE TypeFamilies #-}
>
> 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’
> }}}

New description:

 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):
 {{{#!haskell
 {-# 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’
 }}}

--

Comment (by thomie):

 Your example seemed to be missing a `FlexibleContexts` pragma, so I added
 it.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11067#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler