[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