diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec index e308167fe3..191f3c7dd6 100644 --- a/include/GHC/CString.spec +++ b/include/GHC/CString.spec @@ -4,4 +4,4 @@ import GHC.Prim GHC.CString.unpackCString# :: x:GHC.Prim.Addr# - -> {v:String | len v == strLen x} + -> {v:[Char] | v ~~ x && len v == strLen x} diff --git a/src/Language/Haskell/Liquid/ANFTransform.hs b/src/Language/Haskell/Liquid/ANFTransform.hs index 4601b3e250..dab4cf908d 100644 --- a/src/Language/Haskell/Liquid/ANFTransform.hs +++ b/src/Language/Haskell/Liquid/ANFTransform.hs @@ -125,11 +125,11 @@ normalizeName :: VarEnv Id -> CoreExpr -> DsMW CoreExpr -- normalizeNameDebug γ e -- = liftM (tracePpr ("normalizeName" ++ showPpr e)) $ normalizeName γ e -normalizeName _ e@(Lit _) - = normalizeLiteral e - -normalizeName _ e@(Tick _ (Lit _)) +normalizeName _ e@(Lit l) + | shouldNormalize l = normalizeLiteral e + | otherwise + = return e normalizeName γ (Var x) = return $ Var (lookupWithDefaultVarEnv γ x x) @@ -152,6 +152,10 @@ normalizeName γ e add [NonRec x e'] return $ Var x +shouldNormalize l = case l of + LitInteger _ _ -> True + MachStr _ -> True + _ -> False add :: [CoreBind] -> DsMW () add w = modify $ \s -> s{st_binds = st_binds s++w} diff --git a/src/Language/Haskell/Liquid/CoreToLogic.hs b/src/Language/Haskell/Liquid/CoreToLogic.hs index 4f097a9e39..93b079e0a7 100644 --- a/src/Language/Haskell/Liquid/CoreToLogic.hs +++ b/src/Language/Haskell/Liquid/CoreToLogic.hs @@ -388,6 +388,7 @@ isUndefined (_, _, e) = isUndefinedExpr e where -- auto generated undefined case: (\_ -> (patError @type "error message")) void isUndefinedExpr (C.App (C.Var x) _) | (show x) `elem` perrors = True + isUndefinedExpr (C.Let _ e) = isUndefinedExpr e -- otherwise isUndefinedExpr _ = False