Weird fundep behavior (with -fallow-undecidable-instances)

[nibro]

I encounter a strange behavior with functional dependencies. Consider this program

class Foo x y | x -> y where
 foo :: x -> y

class Bar x y where
 bar :: x -> y -> Int

instance (Foo x y, Bar y z) => Bar x z where
 bar x z = bar (foo x) z

Compiling (with 6.4.2, -fallow-undecidable-instances and -fglasgow-exts) I get the following error message:

Foo.hs:12:0:
    Context reduction stack overflow; size = 21
    Use -fcontext-stack20 to increase stack size to (e.g.) 20
        `$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
        [... same thing 20 times ...]
        `$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
        `bar :: {bar at [y z]}' arising from use of `bar' at Foo.hs:13:11-13
    When trying to generalise the type inferred for `bar'
      Signature type:     forall x y z. (Foo x y, Bar y z) => x -> z -> Int
      Type to generalise: x -> z -> Int
    In the instance declaration for `Bar x z'

The declaration requires undecidable instances, but I doubt that the problem comes from that. What makes it even more weird is that I can get this to compile, and behave as expected, if I do one of a) declare an instance of Bar for any type, or b) add an explicit type signature (foo x :: y) in the definition of Bar. The first seems weird since how could a different, unrelated instance affect the typeability of the second instance? The second, b), is weird since by the FD x -> y we should already know that foo x :: y.

Same behavior in GHC 6.4.1. Hugs (with -98 +O) accepts the code.

[simonpj]

Great report. This is a nice simple example of something that has only shown up in complicated programs so far.

Here's what happens. In the instance decl

instance (Foo x y, Bar y z) => Bar x z where
 bar x z = bar (foo x) z

Ghc solves the following problem:

   HAS: (Foo x y, Bar y z)
   WANTS: (Foo x y', Bar y' z)

The (Foo x y') arises from the call to foo, and the (Bar y' z) from the call to bar.

Now, if we did improvement now, we'd see that y'=y. But GHC doesn't. For historical reasons, it alternates constraint simplification with improvement. So it sees (Bar y' z). Yes! That matches an instance declaration! So it removes tha constraint and adds (Foo x y, Bar y z). And then it does that repeatedly.

The solution is to do improvement more eagerly, which will form part of my upcoming house-cleaning operation on constraint solving.

Short term: you are stuck. But this bug report makes sure I'll fix it in a while.

Simon

[simonpj]

I doubt I'll ever fix this, because we have a better way. With indexed type families we'll write

class Foo x  where
 type Y x
 foo :: x -> Y x

class Bar x y where
 bar :: x -> y -> Int

instance (Foo x y, Bar y z) => Bar x z where
 bar x z = bar (foo x) z

So now the inference problem becomes

   GIVEN: (Foo x, Bar (Y x) z)
   WANTED: (Foo x, Bar (Y x) z)

which is trivially solvable.

Simon

[igloo]

This example now compiles in 6.12.

[simonpj]

Reopening, because this is failing again with the new type inference engine. It's a very delicate case, and I'm not losing sleep over it.

Simon