From 5cb3d80ed0eef83e396dad95c3c1f1c2e075941c Mon Sep 17 00:00:00 2001
From: Eric Seidel <gridaphobe@gmail.com>
Date: Mon, 13 Jul 2015 14:32:31 -0700
Subject: [PATCH] re-add unsorted equality to type of unpackCString

---
 include/GHC/CString.spec                    |  2 +-
 src/Language/Haskell/Liquid/ANFTransform.hs | 12 ++++++++----
 src/Language/Haskell/Liquid/CoreToLogic.hs  |  1 +
 3 files changed, 10 insertions(+), 5 deletions(-)

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