Update renamer errors to clarify some funny situations

This tries to address #125 by making the errors from the renamer a little bit
more clear.

Squashed commit of the following:

commit 8afd3d7961b58df042fe801c3c5e1b9787f813bc
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:33:59 2014 -0800

    Update tests for new renamer errors

commit 7cac01836d8943cf3b08d6715ac328e3b6658cef
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:33:49 2014 -0800

    Add `at` on errors and warnings to be more consistent

commit 308908ba318a4cdc839710f66f1a487543f8c07e
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 19:06:57 2014 -0800

    More consistent renamer warnings

commit be8100a78e9eaba6d554591121c24ed5dcd3c780
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 18:56:53 2014 -0800

    More consistent error formatting from the renamer

commit 26c45c3b51e0bdbcf6a1431cab8e1eb8760ea0bb
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 18:56:36 2014 -0800

    Remove an un-triggerable error

commit ccdb93e036ba1e111ccd977c8b3b35523f3c1bf0
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 16:38:44 2014 -0800

    Try to give better errors for unbound identifiers

commit eb5784145985bb55c761088eaba27c67d08c1326
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 16:38:23 2014 -0800

    Remove old TODOs about located errors

commit b984bb5f451f3aa7b4fc8f15167483c5142ee9a3
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 14:37:34 2014 -0800

    Differentiate missing type and expression symbols

commit b9e6f13856db6765dced3cb9565cdc8387a7976d
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Dec 3 14:36:52 2014 -0800

    Remove a shadowing warning

src/Cryptol/ModuleSystem/Renamer.hs

@@ -36,49 +36,80 @@ import qualified Data.Map as Map
 
 -- Errors ----------------------------------------------------------------------
 
--- XXX make these located
 data RenamerError
   = MultipleSyms (Located QName) [NameOrigin]
     -- ^ Multiple imported symbols contain this name
-  | UnboundSym (Located QName)
-    -- ^ Symbol is not bound to any definition
+
+  | UnboundExpr (Located QName)
+    -- ^ Expression name is not bound to any definition
+
+  | UnboundType (Located QName)
+    -- ^ Type name is not bound to any definition
+
   | OverlappingSyms [NameOrigin]
     -- ^ An environment has produced multiple overlapping symbols
 
-  | BuiltInTypeDecl QName
-    -- ^ This is a built-in type name, and user may not shadow it.
+  | ExpectedValue (Located QName)
+    -- ^ When a value is expected from the naming environment, but one or more
+    -- types exist instead.
+
+  | ExpectedType (Located QName)
+    -- ^ When a type is missing from the naming environment, but one or more
+    -- values exist with the same name.
     deriving (Show)
 
 instance PP RenamerError where
   ppPrec _ e = case e of
 
     MultipleSyms lqn qns ->
-      hang (text "[error] Multiple definitions for symbol:" <+> pp lqn)
-         4 (vcat (map pp qns))
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 $ (text "Multiple definitions for symbol:" <+> pp (thing lqn))
+          $$ vcat (map pp qns)
 
-    UnboundSym lqn ->
-      text "[error] unbound symbol:" <+> pp lqn
+    UnboundExpr lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (text "Value not in scope:" <+> pp (thing lqn))
+
+    UnboundType lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (text "Type not in scope:" <+> pp (thing lqn))
 
-    -- XXX these really need to be located
     OverlappingSyms qns ->
-      hang (text "[error] Overlapping symbols defined:")
-         4 (vcat (map pp qns))
+      hang (text "[error]")
+         4 $ text "Overlapping symbols defined:"
+          $$ vcat (map pp qns)
 
-    BuiltInTypeDecl q ->
-      hang (text "[error] Built-in type name may not be shadowed:")
-         4 (pp q)
+    ExpectedValue lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (fsep [ text "Expected a value named", quotes (pp (thing lqn))
+                 , text "but found a type instead"
+                 , text "Did you mean `(" <> pp (thing lqn) <> text")?" ])
+
+    ExpectedType lqn ->
+      hang (text "[error] at" <+> pp (srcRange lqn))
+         4 (fsep [ text "Expected a type named", quotes (pp (thing lqn))
+                 , text "but found a value instead" ])
 
 -- Warnings --------------------------------------------------------------------
 
 data RenamerWarning
-  = SymbolShadowed [NameOrigin] [NameOrigin]
+  = SymbolShadowed NameOrigin [NameOrigin]
     deriving (Show)
 
 instance PP RenamerWarning where
-  ppPrec _ (SymbolShadowed original new) =
-    hang (text "[warning] This binding for" <+> commaSep (map pp original)
-              <+> text "shadows the existing binding")
-       4 (vcat (map pp new))
+  ppPrec _ (SymbolShadowed new originals) =
+    hang (text "[warning] at" <+> loc)
+       4 $ fsep [ text "This binding for" <+> sym
+                , text "shadows the existing binding" <> plural <+> text "from" ]
+        $$ vcat (map pp originals)
+
+    where
+    plural | length originals > 1 = char 's'
+           | otherwise            = empty
+
+    (loc,sym) = case new of
+                  Local lqn   -> (pp (srcRange lqn), pp (thing lqn))
+                  Imported qn -> (empty, pp qn)
 
 
 -- Renaming Monad --------------------------------------------------------------
@@ -158,37 +189,35 @@ shadowNames names m = RenameM $ do
   let ro' = ro { roNames = env `shadowing` roNames ro }
   local ro' (unRenameM m)
 
--- | Generate warnings when the the left environment shadows things defined in
+-- | Generate warnings when the left environment shadows things defined in
 -- the right.  Additionally, generate errors when two names overlap in the
 -- left environment.
 checkEnv :: NamingEnv -> NamingEnv -> Out
-checkEnv l r = Map.foldlWithKey (step False neExprs) mempty (neExprs l)
-     `mappend` Map.foldlWithKey (step True neTypes) mempty (neTypes l)
+checkEnv l r = Map.foldlWithKey (step neExprs) mempty (neExprs l)
+     `mappend` Map.foldlWithKey (step neTypes) mempty (neTypes l)
   where
 
-  step isType prj acc k ns = acc `mappend` Out
+  step prj acc k ns = acc `mappend` mempty
     { oWarnings = case Map.lookup k (prj r) of
         Nothing -> []
-        Just os -> [SymbolShadowed (map origin os) (map origin ns)]
+        Just os -> [SymbolShadowed (origin (head ns)) (map origin os)]
     , oErrors   = containsOverlap ns
-    } `mappend`
-      checkValidDecl isType k
-
-  containsOverlap ns = case ns of
-    [_] -> []
-    []  -> panic "Renamer" ["Invalid naming environment"]
-    _   -> [OverlappingSyms (map origin ns)]
-
-  checkValidDecl True nm@(QName _ (Name "width")) =
-    mempty { oErrors = [BuiltInTypeDecl nm] }
-  checkValidDecl _ _ = mempty
+    }
 
+-- | Check the RHS of a single name rewrite for conflicting sources.
+containsOverlap :: HasQName a => [a] -> [RenamerError]
+containsOverlap [_] = []
+containsOverlap []  = panic "Renamer" ["Invalid naming environment"]
+containsOverlap ns  = [OverlappingSyms (map origin ns)]
 
 -- | Throw errors for any names that overlap in a rewrite environment.
 checkNamingEnv :: NamingEnv -> ([RenamerError],[RenamerWarning])
-checkNamingEnv env = (oErrors out, oWarnings out)
+checkNamingEnv env = (out, [])
   where
-  out = checkEnv env mempty
+  out    = Map.foldr check outTys (neExprs env)
+  outTys = Map.foldr check mempty (neTypes env)
+
+  check ns acc = containsOverlap ns ++ acc
 
 
 -- Renaming --------------------------------------------------------------------
@@ -258,7 +287,13 @@ renameExpr qn = do
          return qn
     Nothing   ->
       do n <- located qn
-         record (UnboundSym n)
+
+         case Map.lookup qn (neTypes (roNames ro)) of
+           -- types existed with the name of the value expected
+           Just _ -> record (ExpectedValue n)
+
+           -- the value is just missing
+           Nothing -> record (UnboundExpr n)
          return qn
 
 renameType :: QName -> RenameM QName
@@ -273,7 +308,15 @@ renameType qn = do
          return qn
     Nothing   ->
       do n <- located qn
-         record (UnboundSym n)
+
+         case Map.lookup qn (neExprs (roNames ro)) of
+
+           -- values exist with the same name, so throw a different error
+           Just _ -> record (ExpectedType n)
+
+           -- no terms with the same name, so the type is just unbound
+           Nothing -> record (UnboundType n)
+
          return qn
 
 -- | Rename a schema, assuming that none of its type variables are already in
@@ -377,7 +420,7 @@ instance Rename Expr where
     ESel e' s     -> ESel    <$> rename e' <*> pure s
     EList es      -> EList   <$> rename es
     EFromTo s n e'-> EFromTo <$> rename s  <*> rename n  <*> rename e'
-    EInfFrom e e' -> EInfFrom<$> rename e  <*> rename e'
+    EInfFrom a b  -> EInfFrom<$> rename a  <*> rename b
     EComp e' bs   -> do bs' <- mapM renameMatch bs
                         shadowNames (namingEnv bs')
                             (EComp <$> rename e' <*> pure bs')

tests/regression/check09.icry.stdout

@@ -1,14 +1,18 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] This binding for (at check09.cry:4:1--4:6, Main::initL) shadows the existing binding
-    (at check09.cry:22:5--22:10, initL)
-[warning] This binding for (at check09.cry:3:1--3:6, Main::initS) shadows the existing binding
-    (at check09.cry:21:5--21:10, initS)
-[warning] This binding for (at check09.cry:8:1--8:3, Main::ls) shadows the existing binding
-    (at check09.cry:27:5--27:7, ls)
-[warning] This binding for (at check09.cry:5:1--5:3, Main::ss) shadows the existing binding
-    (at check09.cry:23:5--23:7, ss)
+[warning] at check09.cry:22:5--22:10
+    This binding for initL shadows the existing binding from
+    (at check09.cry:4:1--4:6, Main::initL)
+[warning] at check09.cry:21:5--21:10
+    This binding for initS shadows the existing binding from
+    (at check09.cry:3:1--3:6, Main::initS)
+[warning] at check09.cry:27:5--27:7
+    This binding for ls shadows the existing binding from
+    (at check09.cry:8:1--8:3, Main::ls)
+[warning] at check09.cry:23:5--23:7
+    This binding for ss shadows the existing binding from
+    (at check09.cry:5:1--5:3, Main::ss)
 [warning] at check09.cry:17:1--30:54:
   Defaulting 4th type parameter
              of expression (@@)

tests/regression/check25.icry.stdout

@@ -1,8 +1,9 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module check25
-[warning] This binding for (at check25.cry:3:1--3:3, check25::tz) shadows the existing binding
-    (at check25.cry:6:9--6:11, tz)
+[warning] at check25.cry:6:9--6:11
+    This binding for tz shadows the existing binding from
+    (at check25.cry:3:1--3:3, check25::tz)
 [warning] at check25.cry:1:1--8:19:
   Defaulting 1st type parameter
              of expression check25::tx

tests/renamer/comp02.icry.stdout

@@ -2,9 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module comp02
 
-[error] Overlapping symbols defined:
+[error]
+    Overlapping symbols defined:
     (at comp02.cry:4:12--4:13, a)
     (at comp02.cry:5:12--5:13, a)
-[error] Multiple definitions for symbol: (at comp02.cry:4:8--4:9, 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)