#816: Weird fundep behavior (with -fallow-undecidable-instances)
--------------------------------------+-------------------------------------
Reporter: nibro | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.4.2
Severity: normal | Resolution:
Keywords: | Os: Unknown
Difficulty: Unknown | Architecture: Unknown
--------------------------------------+-------------------------------------
Changes (by simonpj):
* owner: => simonpj
Old description:
> I encounter a strange behavior with functional dependencies. Assume we
> have a class defined as
>
> class Foo x y | x -> y where
> foo :: x -> y
>
> and another class
>
> class Bar x y where
> bar :: x -> y -> Int
>
> and I want to write the instance declaration
>
> 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:
> <error>
> 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'
> </error>
>
> 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.
New description:
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.
Comment:
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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/816>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
