Commit 406444b5 authored by Georgios Karachalias's avatar Georgios Karachalias
Browse files

pmcheck: Comments about undecidability of literal equality

parent 81cf2009
......@@ -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
......
......@@ -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
......
......@@ -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)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment