Cyclic Type Class Hierarchy Produces <<loop>>

[jun0]

If there is a cyclic class hierarchy like

    class B a => Semigroup a                  where ...[[BR]]
    class Semigroup (Additive a) => Ring a    where ...[[BR]]
    instance Ring a => Semigroup (Additive a) where ...[[BR]]

then uses of B's methods on (Additive a) in the method implementations of the third declaration instance Ring a => Semigroup (Additive a) will:

1. be accepted by the compiler even in cases where B (Additive a) is not derivable.
2. result in <<loop>>.

The attached program prints <<loop>> when compiled with GHC-7.2.1 or newer but prints 1234567890 when compiled with GHC-7.0.4 or older. I haven't had time to try out any revisions in between those two, but I did check that HEAD produces <<loop>> as well.

[simonpj]

Thanks. I think this is another example of #5751. I know how to fix it but am hoping to wait until after the Haskell Symposium deadline (2 June). How much of a problem is it for you?

[jun0]

That sure looks like the same problem. This is just some test code for a library we're writing, so it can wait. We'll just not run this test till the problem gets fixed.

[igloo]

I'm getting a core lint failure for this test:

=====> T6117(normal) 69 of 69 [0, 0, 0]
cd . && '/home/ian/ghc/git/ghc/inplace/bin/ghc-stage2' -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-package-db -rtsopts -fno-ghci-history -o T6117 T6117.hs    >T6117.comp.stderr 2>&1
Compile failed (status 256) errors were:
[1 of 1] Compiling Main             ( T6117.hs, T6117.o )
*** Core Lint errors : in result of Simplifier ***
{-# LINE 37 "T6117.hs #-}: Warning:
    [RHS of Main.$fBAdditive :: forall a_ahu.
                                Main.B a_ahu =>
                                Main.B (Main.Additive a_ahu)]
    Bad axiom application (check_ki2)
      Main.NTCo:B (Sym (Main.NTCo:B (Main.NTCo:Additive <a_XhN>)))
*** Offending Program ***
[...]

[monoidal]

In fact, the core lint error is on much simpler:

class B a where
    b :: a

newtype Additive a = Additive a

instance B a => B (Additive a) where
   b = Additive b

main = undefined

This is a bit worrisome, since this is a rather natural program.

[simonpj]

You should not worry about this. In GHC we have kind * and kind Constraint. They are really the same kind, so far as System FC is concerned. But they are distinct in the following sense: given a type

 f :: t1 -> t2 -> t3

where

   t1 :: Constraint
   t2 :: *
   t3 :: *

the type inference engine will auto-instantiate a constraint for t1, but not for t2. Also it'll display the type as

  f :: t1 => t2 -> t3

What I need to so is to make the distinctions in only the right places, and it's not quite right now.

In short, don't lose sleep.

[simonpj]

I've opened a new ticket #7451 for this, since the new topic is nothing to do with the original subject of this ticket.