Opened 8 years ago

Last modified 3 months ago

#816 new bug

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

Reported by: nibro Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 6.4.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: typecheck/should_compile/tc216, indexed-types/should_compile/Gentle Blocked By:
Blocking: Related Tickets:

Description (last modified by simonpj)

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.

Change History (14)

comment:1 Changed 8 years ago by simonpj

  • Description modified (diff)
  • Owner set to 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

comment:2 Changed 8 years ago by simonpj

  • Milestone set to 6.8

comment:3 Changed 7 years ago by igloo

  • Test Case set to tc216

comment:4 Changed 7 years ago by guest

comment:5 Changed 7 years ago by 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

comment:6 Changed 6 years ago by simonpj

  • Milestone changed from 6.8 branch to _|_

comment:7 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:8 Changed 6 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:9 Changed 4 years ago by igloo

  • Resolution set to fixed
  • Status changed from new to closed
  • Type of failure set to None/Unknown

This example now compiles in 6.12.

comment:10 Changed 4 years ago by simonpj

  • Owner simonpj deleted
  • Resolution fixed deleted
  • Status changed from closed to new

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

comment:11 Changed 4 years ago by simonpj

  • Blocked By 4232 added

comment:12 Changed 4 years ago by simonpj

  • Test Case changed from tc216 to typecheck/should_compile/tc216, indexed-types/should_compile/Gentle

comment:13 Changed 4 years ago by igloo

  • Blocked By 4232 removed

comment:14 Changed 3 months ago by Ian Lynagh <igloo@…>

In 9218ce88678ebb16913fbc32462bdb57f7774799/ghc:

Add test tc216 for trac #816 (fundep undecidable-instances typechecking loop)
Note: See TracTickets for help on using tickets.