#10195: GHC forgets constraints when matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): Interesting. One problem with this code is that it sports some overlapping instances. Your local `Bar m m'` constraint overlaps with the global `Bar m m'` instance. It's not terribly surprising to me that GHC gets confused here. This is a dark corner of `FlexibleInstances`. Part of the problem is that it's hard for GHC to know what the type of `magic $ scinv * b` should be. Due to the GADT pattern-match, it doesn't want to guess that the type should be `Foo m zp (c m' zq)`, as that choice might be ignoring some information gained in the pattern-match. My guess is that some of your deltas cause GHC to deduce that no equalities are learned in the pattern-match, and thus that result type inference is safe. In any case, I don't think GHC is "forgetting" anything here. It's just choosing one seemingly-viable route toward a solution (the global instance) instead of another, the local constraint. I do agree that this behavior is somewhat disconcerting, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler