[commit: ghc] wip/gadtpm: some more simplification & comments about overloaded literals (850905a)
git at git.haskell.org
git at git.haskell.org
Wed Dec 2 17:07:24 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/gadtpm
Link : http://ghc.haskell.org/trac/ghc/changeset/850905ab3f2e87d5d3def01dfd2ad63dd012937a/ghc
>---------------------------------------------------------------
commit 850905ab3f2e87d5d3def01dfd2ad63dd012937a
Author: George Karachalias <george.karachalias at gmail.com>
Date: Wed Dec 2 17:54:16 2015 +0100
some more simplification & comments about overloaded literals
>---------------------------------------------------------------
850905ab3f2e87d5d3def01dfd2ad63dd012937a
compiler/deSugar/Check.hs | 14 +++-------
compiler/deSugar/TmOracle.hs | 61 ++++++++++++++++++++++++++++++--------------
2 files changed, 45 insertions(+), 30 deletions(-)
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 0287803..5b33167 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -876,14 +876,9 @@ pruneVSABound n v = pruneVSABound' n init_cs emptylist v
-- Have another go at the term oracle state, for strange
-- equalities between overloaded literals. See
-- Note [Undecidable Equality on Overloaded Literals] in TmOracle
- case tryLitEqs tm_env of
- -- An equality (l1 ~ l2) is in the residual constraints. This
- -- means that the whole subtree makes the assumption that
- -- from l1 ~ from l2. We do not want to print such warnings.
- Just True -> return []
- -- No strange constraints (l1 ~ l2) are present. Proceed with
- -- the type oracle.
- Just False -> do
+ if containsEqLits tm_env
+ then return [] -- not on the safe side
+ else do
-- TODO: Provide an incremental interface for the type oracle
sat <- tyOracle (listToBag ty_cs)
return $ case sat of
@@ -891,9 +886,6 @@ pruneVSABound n v = pruneVSABound' n init_cs emptylist v
vector = substInValVecAbs subst (toList vec)
in [(vector, residual_eqs)]
False -> []
- -- Literal constraints (l1 ~ l2) were present and exploiting them
- -- detected an inconsistency.
- Nothing -> return []
Constraint cs vsa -> case splitConstraints cs of
(new_ty_cs, new_tm_cs, new_bot_ct) ->
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index 39b61b6..d69ffdb 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -14,7 +14,7 @@ module TmOracle (
pprPmExprWithParens, lhsExprToPmExpr, hsExprToPmExpr,
-- the term oracle
- tmOracle, TmState, initialTmState, tryLitEqs,
+ tmOracle, TmState, initialTmState, containsEqLits,
-- misc.
exprDeepLookup, pmLitType, flattenPmVarEnv
@@ -149,6 +149,7 @@ simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
-- | Simplify an expression. The boolean indicates if there has been any
-- simplification or if the operation was a no-op.
simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
+-- See Note [Deep equalities]
simplifyPmExpr e = case e of
PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
(ts', bs) -> (PmExprCon c ts', or bs)
@@ -157,6 +158,7 @@ simplifyPmExpr e = case e of
-- | Simplify an equality expression. The equality is given in parts.
simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
+-- See Note [Deep equalities]
simplifyEqExpr e1 e2 = case (e1, e2) of
-- Varables
(PmExprVar x, PmExprVar y)
@@ -322,9 +324,9 @@ cannot detect that constraint:
False ~ (l1 ~ l3), False ~ (l2 ~ l4), l1 ~ l3
-is inconsistent. That's what function @tryLitEqs@ tries to do: use the equality
-l1 ~ l3 to replace False ~ (l1 ~ l3) with False ~ (l1 ~ l1) and expose the
-inconsistency.
+is inconsistent. That's what function @tryLitEqs@ (in comments) tries to do:
+use the equality l1 ~ l3 to replace False ~ (l1 ~ l3) with False ~ (l1 ~ l1)
+and expose the inconsistency.
PROBLEM 2:
~~~~~~~~~~
@@ -354,16 +356,33 @@ issue a warning like:
In an equation for f:
Patterns not matched:
...
- l1 y where y not one of {l2, l4} -- (*)
+ l1 y where y not one of {l2, l4}
under the assumption that l1 ~ l3
It may be more complex but I would prefer to play on the safe side and (safely)
issue all warnings and leave it up to the user to decide whether the assumption
holds or not.
--}
+At the moment, we use @containsEqLits@ and consider all constraints that
+include literal equalities inconsistent. We could achieve the same by replacing
+this clause of @eqPmLit@:
+
+ eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
+ | b1 == b2 && l1 == l2 = Just True
+ | otherwise = Nothing
+
+with this:
+ eqPmLit (PmOLit b1 l1) (PmOLit b2 l2)
+ | b1 == b2 && l1 == l2 = Just True
+ | otherwise = Just False
+which approximates on the unsafe side. Hopefully, literals always need a
+catch-all case to be considered exhaustive so in practice it makes small
+difference. I hate this but it gives the warnings the users are used to.
+-}
+
+{- Not Enabled at the moment
-- | Check whether overloaded literal constraints exist in the state and if
-- they can be used to detect further inconsistencies.
@@ -402,19 +421,6 @@ exploitLitEqs tm_state = case tm_state of
replaceLitSimplifyComplexEq l1 l2 (e1,e2) =
simplifyComplexEq (replaceLit l1 l2 e1, replaceLit l1 l2 e2)
-exists :: (a -> Maybe b) -> [a] -> Maybe (b, [a])
-exists _ [] = Nothing
-exists p (x:xs) = case p x of
- Just y -> Just (y, xs)
- Nothing -> do
- (y, ys) <- exists p xs
- return (y, x:ys)
-
--- | Check whether a complex equality refers to literals only
-isLitEq_mb :: ComplexEq -> Maybe (PmLit, PmLit)
-isLitEq_mb (PmExprLit l1, PmExprLit l2) = Just (l1, l2)
-isLitEq_mb _other_eq = Nothing
-
-- | Replace a literal with another in an expression
-- See Note [Undecidable Equality on Overloaded Literals]
replaceLit :: PmLit -> PmLit -> PmExpr -> PmExpr
@@ -427,5 +433,22 @@ replaceLit l1 l2 e = case e of
Nothing -> e
PmExprEq e1 e2 -> PmExprEq (replaceLit l1 l2 e1) (replaceLit l1 l2 e2)
PmExprOther {} -> e -- do nothing
+-}
+-- | Check whether the term oracle state
+-- contains any equalities between literals.
+containsEqLits :: TmState -> Bool
+containsEqLits (stb, _) = isJust (exists isLitEq_mb stb)
+
+exists :: (a -> Maybe b) -> [a] -> Maybe (b, [a])
+exists _ [] = Nothing
+exists p (x:xs) = case p x of
+ Just y -> Just (y, xs)
+ Nothing -> do
+ (y, ys) <- exists p xs
+ return (y, x:ys)
+-- | Check whether a complex equality refers to literals only
+isLitEq_mb :: ComplexEq -> Maybe (PmLit, PmLit)
+isLitEq_mb (PmExprLit l1, PmExprLit l2) = Just (l1, l2)
+isLitEq_mb _other_eq = Nothing
More information about the ghc-commits
mailing list