From 3209e59fc57eaab844cf5ed5bafc8ead7b745dde Mon Sep 17 00:00:00 2001
From: Rob Dockins <robdockins@fastmail.fm>
Date: Mon, 16 May 2016 13:58:06 -0700
Subject: [PATCH 01/13] Back out changes that delayed applying substituions
 when composing.

Although this does reduce garbage produced when evaluating, it is a
major slowdown on some typechecking tasks (in particular, the typechecking
of large arrays of literals).
---
 src/Cryptol/TypeCheck/Subst.hs | 47 ++++++++++++----------------------
 1 file changed, 17 insertions(+), 30 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs
index 63ffdc57..3a59055b 100644
--- a/src/Cryptol/TypeCheck/Subst.hs
+++ b/src/Cryptol/TypeCheck/Subst.hs
@@ -32,7 +32,6 @@ import           Data.Maybe
 import           Data.Either (partitionEithers)
 import qualified Data.Foldable as Fold
 import qualified Data.Map.Strict as Map
-import qualified Data.Sequence as Seq
 import qualified Data.IntMap as IntMap
 import           Data.Set (Set)
 import qualified Data.Set as Set
@@ -43,36 +42,29 @@ import Cryptol.TypeCheck.TypeMap
 import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.Misc(anyJust)
 
-data Subst = S { suMap :: !(Seq.Seq (Map.Map TVar Type))
+data Subst = S { suMap :: !(Map.Map TVar Type)
                , suDefaulting :: !Bool
                }
                   deriving Show
 
 emptySubst :: Subst
-emptySubst = S { suMap = Seq.empty, suDefaulting = False }
+emptySubst = S { suMap = Map.empty, suDefaulting = False }
 
 singleSubst :: TVar -> Type -> Subst
-singleSubst x t = S { suMap = Seq.singleton (Map.singleton x t), suDefaulting = False }
+singleSubst x t = S { suMap = Map.singleton x t, suDefaulting = False }
 
 (@@) :: Subst -> Subst -> Subst
-s2 @@ s1 | Seq.null (suMap s2) =
+s2 @@ s1 | Map.null (suMap s2) =
   if (suDefaulting s1 || not (suDefaulting s2)) then
     s1
   else
     s1{ suDefaulting = True }
-
-s2 @@ s1 = S { suMap = suMap s2 Seq.>< suMap s1
+s2 @@ s1 = S { suMap = Map.map (apSubst s2) (suMap s1) `Map.union` (suMap s2)
              , suDefaulting = suDefaulting s1 || suDefaulting s2
              }
 
-flattenMaps :: Subst -> Map.Map TVar Type
-flattenMaps su = foldr combine Map.empty $ Fold.toList $ suMap su
- where
- mapsub m = su{ suMap = Seq.singleton m }
- combine m2 m1 = (Map.map (apSubst (mapsub m2)) m1) `Map.union` m2
-
 substVars :: Subst -> Set TVar
-substVars su = Set.unions $ map (fvs . Map.elems) $ Fold.toList $ suMap su
+substVars su = fvs . Map.elems $ suMap su
 
 defaultingSubst :: Subst -> Subst
 defaultingSubst s = s { suDefaulting = True }
@@ -83,23 +75,23 @@ defaultingSubst s = s { suDefaulting = True }
 listSubst :: [(TVar,Type)] -> Subst
 listSubst xs
   | null xs   = emptySubst
-  | otherwise = S { suMap = Seq.singleton (Map.fromList xs), suDefaulting = False }
+  | otherwise = S { suMap = Map.fromList xs, suDefaulting = False }
 
 isEmptySubst :: Subst -> Bool
-isEmptySubst su = all Map.null $ Fold.toList $ suMap su
+isEmptySubst su = Map.null $ suMap su
 
 -- Returns the empty set if this is a deaulting substitution
 substBinds :: Subst -> Set TVar
 substBinds su
   | suDefaulting su = Set.empty
-  | otherwise       = Set.unions $ map Map.keysSet $ Fold.toList $ suMap su
+  | otherwise       = Map.keysSet $ suMap su
 
 instance PP (WithNames Subst) where
   ppPrec _ (WithNames s mp)
     | null els  = text "(empty substitution)"
     | otherwise = text "Substitution:" $$ nest 2 (vcat (map pp1 els))
     where pp1 (x,t) = ppWithNames mp x <+> text "=" <+> ppWithNames mp t
-          els       = Map.toList (flattenMaps s)
+          els       = Map.toList (suMap s)
 
 instance PP Subst where
   ppPrec n = ppWithNamesPrec IntMap.empty n
@@ -150,17 +142,12 @@ apSubstMaybe su ty =
 
 
 applySubstToVar :: Subst -> TVar -> Maybe Type
-applySubstToVar su = go (suMap su) (suDefaulting su)
- where
- go maps defaulting x =
-  case Seq.viewr maps of
-    maps' Seq.:> m ->
-      case Map.lookup x m of
-        Just t  -> Just $! apSubst (S maps' defaulting) t
-        Nothing -> go maps' defaulting x
-    Seq.EmptyR
-      | defaulting -> Just $! defaultFreeVar x
-      | otherwise  -> Nothing
+applySubstToVar su x =
+  case Map.lookup x (suMap su) of
+    Just t  -> Just t
+    Nothing
+      | suDefaulting su -> Just $! defaultFreeVar x
+      | otherwise       -> Nothing
 
 class TVars t where
   apSubst :: Subst -> t -> t      -- ^ replaces free vars
@@ -254,7 +241,7 @@ instance TVars Schema where
     captured = Set.fromList (map tpVar xs)
                `Set.intersection`
                subVars
-    su_binds = Map.toList $ flattenMaps su
+    su_binds = Map.toList $ suMap su
     used = fvs sch
     subVars = Set.unions
                 $ map (fvs . applySubstToVar su)

From df27f577a46fc41b7f9aab9ad9533ba2731f101d Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 24 May 2016 08:21:55 -0700
Subject: [PATCH 02/13] Fix typo in comment, whitespace

---
 examples/MiniLock/prim/SHA256.cry | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/examples/MiniLock/prim/SHA256.cry b/examples/MiniLock/prim/SHA256.cry
index 22c9202c..45d20936 100644
--- a/examples/MiniLock/prim/SHA256.cry
+++ b/examples/MiniLock/prim/SHA256.cry
@@ -82,7 +82,6 @@ SHA256MessageSchedule : [16][32] -> [64][32]
 SHA256MessageSchedule M = W where
     W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ]
 
-
 SHA256Compress : [8][32] -> [64][32] -> [8][32]
 SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where
     T1 = [h + S1 e + Ch e f g  + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W]
@@ -99,7 +98,7 @@ SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4
 /*
  * The SHA256' function hashes a preprocessed sequence of blocks with the
  * compression function.  The SHA256 function hashes a sequence of bytes, and
- * is more likely the function that will be similar to those seein in an
+ * is more likely the function that will be similar to those see in in an
  * implementation to be verified.
  */
 
@@ -108,7 +107,7 @@ SHA256' blocks = hash!0 where
     hash = [H0] # [SHA256Compress h (SHA256MessageSchedule b) | h <- hash | b <- blocks]
 
 SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256]
-SHA256 msg =   join (SHA256' [ split x | x <- preprocess(join msg)])
+SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)])
 
 property katsPass = ~zero == [test == kat | (test,kat) <- kats ]
 

From e0e382aa2257b2a18c79db8a7fad949c2f440712 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 24 May 2016 08:22:28 -0700
Subject: [PATCH 03/13] Fix typo in comment

---
 src/Cryptol/TypeCheck/Depends.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs
index a0d788a2..5322e5ff 100644
--- a/src/Cryptol/TypeCheck/Depends.hs
+++ b/src/Cryptol/TypeCheck/Depends.hs
@@ -29,7 +29,7 @@ import qualified Data.Set as Set
 data TyDecl = TS (P.TySyn Name) | NT (P.Newtype Name)
 
 -- | Check for duplicate and recursive type synonyms.
--- Returns the type-synonyms in dependecy order.
+-- Returns the type-synonyms in dependency order.
 orderTyDecls :: [TyDecl] -> InferM [TyDecl]
 orderTyDecls ts =
   do vs <- getTVars

From 0393c8c54d7910848029788e574e970978063415 Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Tue, 24 May 2016 11:58:55 -0700
Subject: [PATCH 04/13] Fixes #335

The local type bindings from type annotations in patterns were not being
processed correctly, and built-in type/type-functions were getting shadowed in
binders.
---
 src/Cryptol/ModuleSystem/Renamer.hs | 116 ++++++++++++++++++++--------
 tests/issues/issue335.icry          |   2 +
 tests/issues/issue335.icry.stdout   |   3 +
 3 files changed, 90 insertions(+), 31 deletions(-)
 create mode 100644 tests/issues/issue335.icry
 create mode 100644 tests/issues/issue335.icry.stdout

diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index 751015f6..28fd9950 100644
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -77,8 +77,11 @@ data RenamerError
   | InvalidConstraint (Type PName) NameDisp
     -- ^ When it's not possible to produce a Prop from a Type.
 
-  | MalformedConstraint (Located (Type PName)) NameDisp
-    -- ^ When a constraint appears within another constraint
+  | MalformedBuiltin (Type PName) PName NameDisp
+    -- ^ When a builtin type/type-function is used incorrectly.
+
+  | BoundReservedType PName (Maybe Range) Doc NameDisp
+    -- ^ When a builtin type is named in a binder.
     deriving (Show,Generic)
 
 instance NFData RenamerError where rnf = genericRnf
@@ -125,10 +128,15 @@ instance PP RenamerError where
       hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
          4 (fsep [ pp ty, text "is not a valid constraint" ])
 
-    MalformedConstraint t disp -> fixNameDisp disp $
-      hang (text "[error] at" <+> pp (srcRange t))
-         4 (sep [ quotes (pp (thing t))
-                , text "is not a valid argument to a constraint" ])
+    MalformedBuiltin ty pn disp -> fixNameDisp disp $
+      hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) (getLoc ty))
+         4 (fsep [ text "invalid use of built-in type", pp pn
+                 , text "in type", pp ty ])
+
+    BoundReservedType n loc src disp -> fixNameDisp disp $
+      hang (text "[error]" <+> maybe empty (\r -> text "at" <+> pp r) loc)
+         4 (fsep [ text "built-in type", quotes (pp n), text "shadowed in", src ])
+
 
 -- Warnings --------------------------------------------------------------------
 
@@ -446,7 +454,12 @@ instance Rename Schema where
 -- into scope.
 renameSchema :: Schema PName -> RenameM (NamingEnv,Schema Name)
 renameSchema (Forall ps p ty loc) =
-  do env <- liftSupply (namingEnv' ps)
+  do -- check that the parameters don't shadow any built-in types
+     let reserved = filter (isReserved . getIdent . tpName) ps
+         mkErr tp = BoundReservedType (tpName tp) (tpRange tp) (text "schema")
+     unless (null reserved) (mapM_ (record . mkErr) reserved)
+
+     env <- liftSupply (namingEnv' ps)
      s'  <- shadowNames env $ Forall <$> traverse rename ps
                                      <*> traverse rename p
                                      <*> rename ty
@@ -494,6 +507,33 @@ translateProp ty = go ty
          CType <$> rename t
 
 
+
+-- | Fixed names for type functions and built-in types.
+reservedTypeNames :: Map.Map Ident ([Type Name] -> Maybe (Type Name))
+reservedTypeNames  = Map.fromList
+  [ (packIdent "inf", typeConst TInf)
+  , (packIdent "Bit", typeConst TBit)
+
+  , (packIdent "min",              arity 2 TCMin)
+  , (packIdent "max",              arity 2 TCMax)
+  , (packIdent "lengthFromThen",   arity 3 TCLenFromThen)
+  , (packIdent "lengthFromThenTo", arity 3 TCLenFromThenTo)
+  , (packIdent "width",            arity 1 TCWidth)
+  ]
+
+  where
+  typeConst c ps =
+    do guard (null ps)
+       return c
+
+  arity n op ps =
+    do guard (length ps == n)
+       return (TApp op ps)
+
+-- | Check to see if this identifier is a reserved type/type-function.
+isReserved :: Ident -> Bool
+isReserved k = Map.member k reservedTypeNames
+
 -- | Resolve fixity, then rename the resulting type.
 instance Rename Type where
   rename ty0 = go =<< resolveTypeFixity ty0
@@ -507,17 +547,12 @@ instance Rename Type where
     go  TInf         = return TInf
 
     go (TUser pn ps)
-      | i == packIdent "inf", null ps     = return TInf
-      | i == packIdent "Bit", null ps     = return TBit
-
-      | i == packIdent "min"              = TApp TCMin           <$> traverse go ps
-      | i == packIdent "max"              = TApp TCMax           <$> traverse go ps
-      | i == packIdent "lengthFromThen"   = TApp TCLenFromThen   <$> traverse go ps
-      | i == packIdent "lengthFromThenTo" = TApp TCLenFromThenTo <$> traverse go ps
-      | i == packIdent "width"            = TApp TCWidth         <$> traverse go ps
-
-      where
-      i = getIdent pn
+      | Just mk <- Map.lookup (getIdent pn) reservedTypeNames =
+        do ps' <- traverse go ps
+           case mk ps' of
+             Just ty -> return ty
+             Nothing -> do record (MalformedBuiltin ty0 pn)
+                           TUser <$> renameType pn <*> pure ps'
 
     go (TUser qn ps)   = TUser    <$> renameType qn <*> traverse go ps
     go (TApp f xs)     = TApp f   <$> traverse go xs
@@ -774,22 +809,30 @@ renamePats  = loop
     [] -> return (mempty, [])
 
 patternEnv :: Pattern PName -> RenameM NamingEnv
-patternEnv p0 = go p0
+patternEnv  = go
   where
   go (PVar Located { .. }) =
     do n <- liftSupply (mkParameter (getIdent thing) srcRange)
        return (singletonE thing n)
 
   go PWild            = return mempty
-  go (PTuple ps)      = foldMap go ps
-  go (PRecord fs)     = foldMap (foldMap go) fs
+  go (PTuple ps)      = bindVars ps
+  go (PRecord fs)     = bindVars (map value fs)
   go (PList ps)       = foldMap go ps
   go (PTyped p ty)    = go p `mappend` typeEnv ty
   go (PSplit a b)     = go a `mappend` go b
   go (PLocated p loc) = withLoc loc (go p)
 
-  typeEnv (TFun a b) = typeEnv a `mappend` typeEnv b
-  typeEnv (TSeq a b) = typeEnv a `mappend` typeEnv b
+  bindVars []     = return mempty
+  bindVars (p:ps) =
+    do env <- go p
+       shadowNames env $
+         do rest <- bindVars ps
+            return (env `mappend` rest)
+
+
+  typeEnv (TFun a b) = bindTypes [a,b]
+  typeEnv (TSeq a b) = bindTypes [a,b]
 
   typeEnv TBit       = return mempty
   typeEnv TNum{}     = return mempty
@@ -801,7 +844,7 @@ patternEnv p0 = go p0
        case mb of
 
          -- The type is already bound, don't introduce anything.
-         Just _ -> foldMap typeEnv ps
+         Just _ -> bindTypes ps
 
          Nothing
            -- The type isn't bound, and has no parameters, so it names a portion
@@ -819,13 +862,21 @@ patternEnv p0 = go p0
                 n   <- liftSupply (mkParameter (getIdent pn) loc)
                 return (singletonT pn n)
 
-  typeEnv (TApp _ ts)       = foldMap typeEnv ts
-  typeEnv (TRecord fs)      = foldMap (foldMap typeEnv) fs
-  typeEnv (TTuple ts)       = foldMap typeEnv ts
+  typeEnv (TApp _ ts)       = bindTypes ts
+  typeEnv (TRecord fs)      = bindTypes (map value fs)
+  typeEnv (TTuple ts)       = bindTypes ts
   typeEnv TWild             = return mempty
   typeEnv (TLocated ty loc) = withLoc loc (typeEnv ty)
   typeEnv (TParens ty)      = typeEnv ty
-  typeEnv (TInfix a _ _ b)  = typeEnv a `mappend` typeEnv b
+  typeEnv (TInfix a _ _ b)  = bindTypes [a,b]
+
+  bindTypes [] = return mempty
+  bindTypes (t:ts) =
+    do env' <- typeEnv t
+       shadowNames env' $
+         do res <- bindTypes ts
+            return (env' `mappend` res)
+
 
 instance Rename Match where
   rename m = case m of
@@ -834,9 +885,12 @@ instance Rename Match where
 
 instance Rename TySyn where
   rename (TySyn n ps ty) =
-     shadowNames ps $ TySyn <$> rnLocated renameType n
-                            <*> traverse rename ps
-                            <*> rename ty
+    do when (isReserved (getIdent (thing n)))
+            (record (BoundReservedType (thing n) (getLoc n) (text "type synonym")))
+
+       shadowNames ps $ TySyn <$> rnLocated renameType n
+                              <*> traverse rename ps
+                              <*> rename ty
 
 
 -- Utilities -------------------------------------------------------------------
diff --git a/tests/issues/issue335.icry b/tests/issues/issue335.icry
new file mode 100644
index 00000000..0073c38f
--- /dev/null
+++ b/tests/issues/issue335.icry
@@ -0,0 +1,2 @@
+:t \ (x: (Bit,Bit)) -> x.0
+:t \ (x:a) (y:a) -> x
diff --git a/tests/issues/issue335.icry.stdout b/tests/issues/issue335.icry.stdout
new file mode 100644
index 00000000..d51b6a39
--- /dev/null
+++ b/tests/issues/issue335.icry.stdout
@@ -0,0 +1,3 @@
+Loading module Cryptol
+\(x : (Bit, Bit)) -> x.0 : (Bit, Bit) -> Bit
+\(x : a) (y : a) -> x : {a} a -> a -> a

From 3658c0962b0f2c59e110a99eece72c9c4c229955 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Wed, 25 May 2016 13:44:51 -0700
Subject: [PATCH 05/13] Fix build with GHC 7.8

Hide an extra symbol from MonadLib.
---
 src/Cryptol/ModuleSystem/Renamer.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index 28fd9950..fb359b7a 100644
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -39,7 +39,7 @@ import Cryptol.Utils.PP
 import qualified Data.Foldable as F
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
-import           MonadLib hiding (mapM)
+import           MonadLib hiding (mapM, mapM_)
 
 import GHC.Generics (Generic)
 import Control.DeepSeq

From bfc8062c696ce06e6aefc4ebe125ecf219133273 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 27 May 2016 15:39:41 -0700
Subject: [PATCH 06/13] Avoid extra shadowing warnings when renaming
 comprehensions

Fixes #286.
---
 src/Cryptol/ModuleSystem/Renamer.hs | 8 ++++++--
 src/Cryptol/REPL/Command.hs         | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index fb359b7a..bfd9deaa 100644
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -705,7 +705,9 @@ instance Rename Expr where
     EInfFrom a b  -> EInfFrom<$> rename a  <*> traverse rename b
     EComp e' bs   -> do arms' <- traverse renameArm bs
                         let (envs,bs') = unzip arms'
-                        shadowNames envs (EComp <$> rename e' <*> pure bs')
+                        -- NOTE: renameArm will generate shadowing warnings; we only
+                        -- need to check for repeated names across multiple arms
+                        shadowNames' CheckOverlap envs (EComp <$> rename e' <*> pure bs')
     EApp f x      -> EApp    <$> rename f  <*> rename x
     EAppT f ti    -> EAppT   <$> rename f  <*> traverse rename ti
     EIf b t f     -> EIf     <$> rename b  <*> rename t  <*> rename f
@@ -767,7 +769,9 @@ renameArm :: [Match PName] -> RenameM (NamingEnv,[Match Name])
 
 renameArm (m:ms) =
   do (me,m') <- renameMatch m
-     shadowNames me $
+     -- NOTE: renameMatch will generate warnings, so we don't
+     -- need to duplicate them here
+     shadowNames' CheckNone me $
        do (env,rest) <- renameArm ms
 
           -- NOTE: the inner environment shadows the outer one, for examples
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index e3994b73..65364c16 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -844,7 +844,7 @@ moduleCmdResult (res,ws0) = do
           ys -> Just (M.TypeCheckWarnings ys)
       filterDefaults w = Just w
 
-      isShadowWarn (M.SymbolShadowed _ _ _) = True
+      isShadowWarn (M.SymbolShadowed {}) = True
 
       filterShadowing w | warnShadowing = Just w
       filterShadowing (M.RenamerWarnings xs) =

From d7b117a8cec8293926b6616b216900e5e41cdc41 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 27 May 2016 16:00:59 -0700
Subject: [PATCH 07/13] Use a type-appropriate function argument name

---
 src/Cryptol/REPL/Command.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index 65364c16..ca04a9b8 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -397,7 +397,7 @@ cmdProveSat isSat "" =
                      then rPutStr $ ":sat "   ++ str ++ "\n\t"
                      else rPutStr $ ":prove " ++ str ++ "\n\t"
                   cmdProveSat isSat str
-cmdProveSat isSat expr = do
+cmdProveSat isSat str = do
   let cexStr | isSat = "satisfying assignment"
              | otherwise = "counterexample"
   EnvString proverName <- getUser "prover"
@@ -405,7 +405,7 @@ cmdProveSat isSat expr = do
   let mfile = if fileName == "-" then Nothing else Just fileName
   case proverName of
     "offline" -> do
-      result <- offlineProveSat isSat expr mfile
+      result <- offlineProveSat isSat str mfile
       case result of
         Left msg -> rPutStrLn msg
         Right smtlib -> do
@@ -421,7 +421,7 @@ cmdProveSat isSat expr = do
             Just path -> io $ writeFile path smtlib
             Nothing -> rPutStr smtlib
     _ -> do
-      result <- onlineProveSat isSat expr mfile
+      result <- onlineProveSat isSat str mfile
       ppOpts <- getPPValOpts
       case result of
         Symbolic.EmptyResult         ->
@@ -435,7 +435,7 @@ cmdProveSat isSat expr = do
           let tess = map (map $ \(t,e,_) -> (t,e)) tevss
               vss  = map (map $ \(_,_,v) -> v)     tevss
               ppvs vs = do
-                parseExpr <- replParseExpr expr
+                parseExpr <- replParseExpr str
                 let docs = map (pp . E.WithBase ppOpts) vs
                     -- function application has precedence 3
                     doc = ppPrec 3 parseExpr

From f6a246230655ff969e08e1fa96667c8993a49d12 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 27 May 2016 16:01:55 -0700
Subject: [PATCH 08/13] :t prints un-renamed parsed AST. Fixes #336.

---
 src/Cryptol/REPL/Command.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index ca04a9b8..7f9220e2 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -545,13 +545,14 @@ typeOfCmd :: String -> REPL ()
 typeOfCmd str = do
 
   expr         <- replParseExpr str
-  (re,def,sig) <- replCheckExpr expr
+  (_re,def,sig) <- replCheckExpr expr
 
   -- XXX need more warnings from the module system
   --io (mapM_ printWarning ws)
   whenDebug (rPutStrLn (dump def))
   (_,_,names) <- getFocusedEnv
-  rPrint $ runDoc names $ pp re <+> text ":" <+> pp sig
+  -- type annotation ':' has precedence 2
+  rPrint $ runDoc names $ ppPrec 2 expr <+> text ":" <+> pp sig
 
 readFileCmd :: FilePath -> REPL ()
 readFileCmd fp = do

From c6144bd33228c4abed4fa5f25133760a1156ee81 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 27 May 2016 16:25:14 -0700
Subject: [PATCH 09/13] Update output for tests 256 and 335

The :t command now parenthesizes the term when needed.
---
 tests/issues/issue256.icry.stdout | 6 +++---
 tests/issues/issue335.icry.stdout | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/issues/issue256.icry.stdout b/tests/issues/issue256.icry.stdout
index 0be3818a..ba0feb42 100644
--- a/tests/issues/issue256.icry.stdout
+++ b/tests/issues/issue256.icry.stdout
@@ -1,4 +1,4 @@
 Loading module Cryptol
-[True] == [False] : Bit
-\x -> True != x : Bit -> Bit
-\x -> True && x : Bit -> Bit
+([True] == [False]) : Bit
+(\x -> True != x) : Bit -> Bit
+(\x -> True && x) : Bit -> Bit
diff --git a/tests/issues/issue335.icry.stdout b/tests/issues/issue335.icry.stdout
index d51b6a39..45c624e9 100644
--- a/tests/issues/issue335.icry.stdout
+++ b/tests/issues/issue335.icry.stdout
@@ -1,3 +1,3 @@
 Loading module Cryptol
-\(x : (Bit, Bit)) -> x.0 : (Bit, Bit) -> Bit
-\(x : a) (y : a) -> x : {a} a -> a -> a
+(\(x : (Bit, Bit)) -> x.0) : (Bit, Bit) -> Bit
+(\(x : a) (y : a) -> x) : {a} a -> a -> a

From 2f21dd509aa4ff3c3a42ec60dea70aaabe95c80a Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Fri, 27 May 2016 17:05:16 -0700
Subject: [PATCH 10/13] Remove the generic-trie dependency

---
 cryptol.cabal                          | 3 ---
 src/Cryptol/TypeCheck/Solver/InfNat.hs | 3 ---
 2 files changed, 6 deletions(-)

diff --git a/cryptol.cabal b/cryptol.cabal
index 080ba089..ffbad88f 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -51,7 +51,6 @@ library
                        directory         >= 1.2,
                        filepath          >= 1.3,
                        gitrev            >= 1.0,
-                       generic-trie      >= 0.3.0.1,
                        GraphSCC          >= 1.0.4,
                        heredoc           >= 0.2,
                        monad-control     >= 1.0,
@@ -168,8 +167,6 @@ library
                        GitRev
 
   GHC-options:         -Wall -O2 -fsimpl-tick-factor=140
-  -- the `fsimpl-tick-factor` is needed to finish optimizing the
-  -- generic trie.
   ghc-prof-options:    -fprof-auto -prof
 
   if flag(relocatable)
diff --git a/src/Cryptol/TypeCheck/Solver/InfNat.hs b/src/Cryptol/TypeCheck/Solver/InfNat.hs
index c43663be..79869dd5 100644
--- a/src/Cryptol/TypeCheck/Solver/InfNat.hs
+++ b/src/Cryptol/TypeCheck/Solver/InfNat.hs
@@ -16,15 +16,12 @@ module Cryptol.TypeCheck.Solver.InfNat where
 import Data.Bits
 import Cryptol.Utils.Panic
 
-import Data.GenericTrie(TrieKey)
 import GHC.Generics(Generic)
 
 -- | Natural numbers with an infinity element
 data Nat' = Nat Integer | Inf
             deriving (Show,Eq,Ord,Generic)
 
-instance TrieKey Nat'
-
 fromNat :: Nat' -> Maybe Integer
 fromNat n' =
   case n' of

From a490600df51a5ba8dcbef977f99f5d02390d292f Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Fri, 27 May 2016 18:37:57 -0700
Subject: [PATCH 11/13] Fix overlap errors in the renamer

* The MultipleSyms error should only show up when the import environment
  contains duplicate symbols, and should be triggered lazily.
* Environments that have had errors reported should be rewritten to no longer
  produce those errors during renameVar/renameType

Fixes #337
---
 src/Cryptol/ModuleSystem/Base.hs    |  5 ----
 src/Cryptol/ModuleSystem/Renamer.hs | 37 ++++++++++++++++-------------
 2 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 51fbbfbe..91eb95e5 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -82,11 +82,6 @@ renameModule :: P.Module PName
              -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
 renameModule m = do
   (decls,menv) <- importIfaces (map thing (P.mImports m))
-  let (es,ws) = R.checkNamingEnv menv
-
-  renamerWarnings ws
-  unless (null es) (renamerErrors es)
-
   (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m)
   return (decls,declsEnv,rm)
 
diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs
index bfd9deaa..65cc12a9 100644
--- a/src/Cryptol/ModuleSystem/Renamer.hs
+++ b/src/Cryptol/ModuleSystem/Renamer.hs
@@ -275,8 +275,8 @@ shadowNames' check names m = do
   do env <- liftSupply (namingEnv' names)
      RenameM $
        do ro  <- ask
-          sets_ (checkEnv (roDisp ro) check env (roNames ro))
-          let ro' = ro { roNames = env `shadowing` roNames ro }
+          env' <- sets (checkEnv (roDisp ro) check env (roNames ro))
+          let ro' = ro { roNames = env' `shadowing` roNames ro }
           local ro' (unRenameM m)
 
 shadowNamesNS :: BindsNames (InModule env) => env -> RenameM a -> RenameM a
@@ -288,25 +288,30 @@ shadowNamesNS names m =
 -- | Generate warnings when the left environment shadows things defined in
 -- the right.  Additionally, generate errors when two names overlap in the
 -- left environment.
-checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> RW -> RW
-checkEnv _    CheckNone _ _ rw = rw
-checkEnv disp check     l r rw = rw''
+checkEnv :: NameDisp -> EnvCheck -> NamingEnv -> NamingEnv -> RW -> (NamingEnv,RW)
+checkEnv disp check l r rw
+  | check == CheckNone = (l',rw)
+  | otherwise          = (l',rw'')
 
   where
 
-  rw'  = Map.foldlWithKey (step neExprs) rw (neExprs l)
-  rw'' = Map.foldlWithKey (step neTypes) rw' (neTypes l)
+  l' = l { neExprs = es, neTypes = ts }
 
-  step prj acc k ns = acc
-    { rwWarnings =
-        if check == CheckAll
-           then case Map.lookup k (prj r) of
-                  Nothing -> rwWarnings acc
-                  Just os -> rwWarnings acc Seq.|> SymbolShadowed (head ns) os disp
+  (rw',es)  = Map.mapAccumWithKey (step neExprs) rw  (neExprs l)
+  (rw'',ts) = Map.mapAccumWithKey (step neTypes) rw' (neTypes l)
 
-           else rwWarnings acc
-    , rwErrors   = rwErrors acc Seq.>< containsOverlap disp ns
-    }
+  step prj acc k ns = (acc', [head ns])
+    where
+    acc' = acc
+      { rwWarnings =
+          if check == CheckAll
+             then case Map.lookup k (prj r) of
+                    Nothing -> rwWarnings acc
+                    Just os -> rwWarnings acc Seq.|> SymbolShadowed (head ns) os disp
+
+             else rwWarnings acc
+      , rwErrors   = rwErrors acc Seq.>< containsOverlap disp ns
+      }
 
 -- | Check the RHS of a single name rewrite for conflicting sources.
 containsOverlap :: NameDisp -> [Name] -> Seq.Seq RenamerError

From 7976026789b71833baa291a50d36f7c4b94e6ed3 Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Fri, 27 May 2016 18:49:56 -0700
Subject: [PATCH 12/13] Update test output renamer errors

---
 tests/renamer/comp02.icry.stdout | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/tests/renamer/comp02.icry.stdout b/tests/renamer/comp02.icry.stdout
index d084e9b6..d0447baa 100644
--- a/tests/renamer/comp02.icry.stdout
+++ b/tests/renamer/comp02.icry.stdout
@@ -6,7 +6,3 @@ Loading module comp02
     Overlapping symbols defined:
     (at ./comp02.cry:4:12--4:13, a)
     (at ./comp02.cry:5:12--5:13, a)
-[error] at ./comp02.cry:4:8--4:9
-    Multiple definitions for symbol: a
-    (at ./comp02.cry:4:12--4:13, a)
-    (at ./comp02.cry:5:12--5:13, a)

From a139c4e1d1cf2670eb4cfe28e97c84e37d98f7bd Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Fri, 27 May 2016 22:00:43 -0700
Subject: [PATCH 13/13] Fixes #304

---
 tests/issues/issue304.cry         | 5 +++++
 tests/issues/issue304.icry        | 4 ++++
 tests/issues/issue304.icry.stdout | 6 ++++++
 3 files changed, 15 insertions(+)
 create mode 100644 tests/issues/issue304.cry
 create mode 100644 tests/issues/issue304.icry
 create mode 100644 tests/issues/issue304.icry.stdout

diff --git a/tests/issues/issue304.cry b/tests/issues/issue304.cry
new file mode 100644
index 00000000..bb6b1e65
--- /dev/null
+++ b/tests/issues/issue304.cry
@@ -0,0 +1,5 @@
+x : [64]
+x = 10
+
+a : [16]
+a # b = x
diff --git a/tests/issues/issue304.icry b/tests/issues/issue304.icry
new file mode 100644
index 00000000..34da359b
--- /dev/null
+++ b/tests/issues/issue304.icry
@@ -0,0 +1,4 @@
+:l issue304.cry
+:t x
+:t a
+:t b
diff --git a/tests/issues/issue304.icry.stdout b/tests/issues/issue304.icry.stdout
new file mode 100644
index 00000000..872d02a0
--- /dev/null
+++ b/tests/issues/issue304.icry.stdout
@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+x : [64]
+a : [16]
+b : [48]