[GHC] #11984: Pattern match incompleteness / inaccessibility discrepancy

[GHC]

#11984: Pattern match incompleteness / inaccessibility discrepancy
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14098            |  Differential Rev(s):  Phab:D4434
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Thanks Ryan. You've nailed the problem.

 I think your fix will work.  And your long Note is great.

 But the particular solution smells wrong.

 I think the real bug is in the "ConCon" case of `pmcheckHd`, which looks
 like this
 {{{
 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
           (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva
 delta)
   | c1 /= c2  =
     return (usimple [ValVec (va:vva) delta])
   | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
                 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva)
 delta)
 }}}
 Notice that it ''totally ignores'' the existential `pm_con_tvs` of the two
 arguments.
 If the two aren't ''identical'' we'll get failure in precisely the way you
 diagnosed.

 I think your fix arranges that they are always identical.  But even if we
 adopt
 your approach, we should add an ASSERT (with explanation) on the "ConCon"
 case.

 More fundamentally, how can we be sure that the assertion holds?  I'm not
 sure.
 An alternative (and more solid) approach would be to fix the bug in
 ConCon.  How?
 Well, looking back at the paper, if we have
 {{{
 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_tvs = tvs1, pm_con_args =
 args1})) ps guards
           (va@(PmCon {pm_con_con = c2, pm_con_tvs = tvs2, pm_con_args =
 args2})) (ValVec vva delta)
 }}}
 then we want to add equalities to `Delta` that say `tvs1 = tvs2`.  And
 that should be dead easy to do.

 If a corresponding pair `tv1` and `tv2` are already equal, no need to
 geneate the equality.

 Now the `mkOneCOnFull` fix turns into mere optimisation, one that makes it
 more likely that the equalities will hold.

 Does that makes sense?

 I'd be content with the ASSERT; that's the shortest path to a fix.  But at
 least
 refer to this comment if so.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11984#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler