[GHC] #10195: GHC forgets constraints when matching on GADTs

[GHC]

#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