[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 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