#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): I'm perhaps abusing the term "overlap". What I mean here is that GHC has two routes with which to satisfy a `Bar m m'` constraint. Let's rename variables in the global instance for clarity: `instance (BarFamily b b' ~ 'True) => Bar b b'`. During type inference, GHC has to solve a `Bar p q` constraint, for some `p` and some `q`. If, at this point during inference, it knows `p ~ m` and `q ~ m'`, GHC will prefer the local constraint `Bar m m'`. Otherwise, if we don't yet know enough about `p` and `q`, it will use the global instance and then require `BarFamily p q ~ 'True`. Even if we later learn that `p ~ m` and `q ~ m'`, it's too late to use the `Bar m m'` constraint. I do know that GHC "tries hard" to resolve equality constraints before class constraints, but ''guaranteeing'' that this happens may be impossible. So, you'll end up with situations like these. I'd be quite curious for Simon's input here. He's on holiday at the moment, but I'm sure he'll chime in ere too long. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler