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

 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