[commit: ghc] master: pmcheck: Comments about undecidability of literal equality (406444b)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/406444b5f4173c20567abc3a3577a58a8ade10d4/ghc

>---------------------------------------------------------------

commit 406444b5f4173c20567abc3a3577a58a8ade10d4
Author: George Karachalias <george.karachalias at gmail.com>
Date:   Sat Dec 5 01:52:58 2015 +0100

    pmcheck: Comments about undecidability of literal equality


>---------------------------------------------------------------

406444b5f4173c20567abc3a3577a58a8ade10d4
 compiler/deSugar/Check.hs    |  3 ++
 compiler/deSugar/PmExpr.hs   | 75 +++++++++++++++++++++++++++++++++++++++-----
 compiler/deSugar/TmOracle.hs |  2 ++
 3 files changed, 73 insertions(+), 7 deletions(-)

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 25b8480..386652a 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -1048,6 +1048,7 @@ cMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- CLitLit
 cMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
+  -- See Note [Undecidable Equality for Overloaded Literals]
   True  -> VA va `mkCons` covered us gvsa ps vsa -- match
   False -> Empty                                 -- mismatch
 
@@ -1101,6 +1102,7 @@ uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- ULitLit
 uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
+  -- See Note [Undecidable Equality for Overloaded Literals]
   True  -> VA va `mkCons` uncovered us gvsa ps vsa -- match
   False -> VA va `mkCons` vsa                      -- mismatch
 
@@ -1161,6 +1163,7 @@ dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
 
 -- DLitLit
 dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
+  -- See Note [Undecidable Equality for Overloaded Literals]
   True  -> VA va `mkCons` divergent us gvsa ps vsa -- match
   False -> Empty                                   -- mismatch
 
diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs
index 78a51e6..16528d4 100644
--- a/compiler/deSugar/PmExpr.hs
+++ b/compiler/deSugar/PmExpr.hs
@@ -62,18 +62,79 @@ data PmExpr = PmExprVar   Id
 data PmLit = PmSLit HsLit                                    -- simple
            | PmOLit Bool {- is it negated? -} (HsOverLit Id) -- overloaded
 
--- | PmLit equality. If both literals are overloaded, the equality check may be
--- inconclusive. Since an overloaded PmLit represents a function application
--- (e.g.  fromInteger 5), if two literals look the same they are the same but
--- if they don't, whether they are depends on the implementation of the
--- from-function. Yet, for the purposes of the check, we check syntactically
--- only (it is safe anyway, since literals always need a catch-all to be
--- considered to be exhaustive).
+-- | Equality between literals for pattern match checking.
 eqPmLit :: PmLit -> PmLit -> Bool
 eqPmLit (PmSLit    l1) (PmSLit    l2) = l1 == l2
 eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
+  -- See Note [Undecidable Equality for Overloaded Literals]
 eqPmLit _              _              = False
 
+{- Note [Undecidable Equality for Overloaded Literals]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Equality on overloaded literals is undecidable in the general case. Consider
+the following example:
+
+  instance Num Bool where
+    ...
+    fromInteger 0 = False -- C-like representation of booleans
+    fromInteger _ = True
+
+    f :: Bool -> ()
+    f 1 = ()        -- Clause A
+    f 2 = ()        -- Clause B
+
+Clause B is redundant but to detect this, we should be able to solve the
+constraint: False ~ (fromInteger 2 ~ fromInteger 1) which means that we
+have to look through function `fromInteger`, whose implementation could
+be anything. This poses difficulties for:
+
+1. The expressive power of the check.
+   We cannot expect a reasonable implementation of pattern matching to detect
+   that fromInteger 2 ~ fromInteger 1 is True, unless we unfold function
+   fromInteger. This puts termination at risk and is undecidable in the
+   general case.
+
+2. Performance.
+   Having an unresolved constraint False ~ (fromInteger 2 ~ fromInteger 1)
+   lying around could become expensive really fast. Ticket #11161 illustrates
+   how heavy use of overloaded literals can generate plenty of those
+   constraints, effectively undermining the term oracle's performance.
+
+3. Error nessages/Warnings.
+   What should our message for `f` above be? A reasonable approach would be
+   to issue:
+
+     Pattern matches are (potentially) redundant:
+       f 2 = ...    under the assumption that 1 == 2
+
+   but seems to complex and confusing for the user.
+
+We choose to treat overloaded literals that look different as different. The
+impact of this is the following:
+
+  * Redundancy checking is rather conservative, since it cannot see that clause
+    B above is redundant.
+
+  * We have instant equality check for overloaded literals (we do not rely on
+    the term oracle which is rather expensive, both in terms of performance and
+    memory). This significantly improves the performance of functions `covered`
+    `uncovered` and `divergent` in deSugar/Check.hs and effectively addresses
+    #11161.
+
+  * The warnings issued are simpler.
+
+  * We do not play on the safe side, strictly speaking. The assumption that
+    1 /= 2 makes the redundancy check more conservative but at the same time
+    makes its dual (exhaustiveness check) unsafe. This we can live with, mainly
+    for two reasons:
+    1. At the moment we do not use the results of the check during compilation
+       where this would be a disaster (could result in runtime errors even if
+       our function was deemed exhaustive).
+    2. Pattern matcing on literals can never be considered exhaustive unless we
+       have a catch-all clause. Hence, this assumption affects mainly the
+       appearance of the warnings and is, in practice safe.
+-}
+
 nubPmLit :: [PmLit] -> [PmLit]
 nubPmLit = nubBy eqPmLit
 
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 9224336..5d7a61a 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -105,6 +105,7 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
   (_,PmExprOther _)            -> Just (standby, (True, env))
 
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
+    -- See Note [Undecidable Equality for Overloaded Literals]
     True  -> Just solver_state
     False -> Nothing
 
@@ -165,6 +166,7 @@ simplifyEqExpr e1 e2 = case (e1, e2) of
 
   -- Literals
   (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
+    -- See Note [Undecidable Equality for Overloaded Literals]
     True  -> (truePmExpr,  True)
     False -> (falsePmExpr, True)