Re: [GHC] #816: Weird fundep behavior (with -fallow-undecidable-instances)

#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@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs