#7766 closed bug (invalid)

equality constraints exposed by patterns mess up constraint inference

Reported by: heisenbug Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

When patterns bring (equality) constraints into scope, the inference mechanism for other (unrelated) constraints breaks down.

This is a new problem that appeared between

  • ghc-7.7.20121025 and
  • ghc-7.7.20121114

I can try to track down the commit if that helps.

Testcase against HEAD attached.

Attachments (1)

pr7766.hs (1.0 KB) - added by heisenbug 13 months ago.
repro test case

Download all attachments as: .zip

Change History (2)

Changed 13 months ago by heisenbug

repro test case

comment:1 Changed 13 months ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to invalid
  • Status changed from new to closed

This is by design. Type inference in the presence of GADTs is tricky!

If you give the signature main :: IO () it works fine. But here you are asking GHC to infer the type of main. (Remember, Haskell doesn't insist on IO (); the main function can have type IO Char.)

Becuase you are pattern matching against GADTs there are equalities in scope, so GHC declines to contrain the type of main. In this particular case there is only one answer, but that's very hard to figure out, so we fail conservatively.

Bottom line: use type signatures when pattern matching on GADTs.

Simon

Note: See TracTickets for help on using tickets.