#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 simonpj): I understand what is going on here. We get this constraint from the call to `magic`: {{{ forall[2] c m m' zp. Bar m m' => forall[3]. Num (c m zp) => Bar meta[2] m', meta[2]~m }}} The [2] and [3] are the "untouchable" levels, and `meta[2]` is a level-2 unification variable. When checking whether we can safely fire the top- level instance `(Bar b b')`, we try to ''unify'' the given `Bar m m'` with `Bar meta[2] m'`. The unification variable `meta[2]` is untouchable, so we wrongly made it behave like a skolem in this unification, so the unification failed, and so we fired the top-level instance. But the `(meta[2] ~ m)` constraint, if allowed to float out and then fire, will make the `Bar meta[2] m'` turn into `Bar m m'`, which can then be discharged by the given `Bar m m'`. So the mistake here is being a bit too eager when asking "is the top-level instance the only one that could apply?". The fix is easy. But of course it means that fewer top-level instances will fire, so it's possible that it will break other examples that currently "work". But rightly so, I think. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10195#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler