Prelude loads again

src/Cryptol/ModuleSystem/Base.hs

@@ -83,7 +83,8 @@ rename modName env m = do
     Left errs -> renamerErrors errs
 
 -- | Rename a module in the context of its imported modules.
-renameModule :: P.Module PName -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
+renameModule :: P.Module PName
+             -> ModuleM (IfaceDecls,R.NamingEnv,R.NamingEnv,P.Module Name)
 renameModule m = do
   (decls,menv) <- importIfaces (map thing (P.mImports m))
   let (es,ws) = R.checkNamingEnv menv
@@ -91,8 +92,8 @@ renameModule m = do
   renamerWarnings ws
   unless (null es) (renamerErrors es)
 
-  rm <- rename (thing (mName m)) menv (R.rename m)
-  return (decls,menv,rm)
+  (declsEnv,rm) <- rename (thing (mName m)) menv (R.renameModule m)
+  return (decls,menv,declsEnv,rm)
 
 -- | Rename declarations in the context of the focused module.
 --
@@ -363,14 +364,13 @@ checkModule path m = do
   npm <- noPat nim
 
   -- rename everything
-  (tcEnv,rnEnv,scm) <- renameModule npm
+  (tcEnv,rnEnv,declsEnv,scm) <- renameModule npm
 
   -- when generating the prim map for the typechecker, if we're checking the
   -- prelude, we have to generate the map from the renaming environment, as we
   -- don't have the interface yet.
   prims <- if thing (mName m) == preludeName
-              then do env <- liftSupply (R.namingEnv' npm)
-                      return (R.toPrimMap env)
+              then return (R.toPrimMap declsEnv)
               else getPrimMap
 
   -- typecheck

src/Cryptol/ModuleSystem/Renamer.hs

@@ -24,6 +24,7 @@ module Cryptol.ModuleSystem.Renamer (
   , RenamerWarning(..)
   , renameVar
   , renameType
+  , renameModule
   ) where
 
 import Cryptol.ModuleSystem.Name
@@ -31,7 +32,7 @@ import Cryptol.ModuleSystem.NamingEnv
 import Cryptol.Prims.Syntax
 import Cryptol.Parser.AST
 import Cryptol.Parser.Position
-import Cryptol.Utils.Ident (packIdent,packInfix)
+import Cryptol.Utils.Ident (packIdent)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.PP
 
@@ -297,6 +298,12 @@ supply m = RenameM (inBase m)
 class Rename f where
   rename :: f PName -> RenameM (f Name)
 
+renameModule :: Module PName -> RenameM (NamingEnv,Module Name)
+renameModule m =
+  do env    <- supply (namingEnv m)
+     decls' <- shadowNames env (traverse rename (mDecls m))
+     return (env,m { mDecls = decls' })
+
 instance Rename Module where
   rename m =
     do decls' <- shadowNames m (traverse rename (mDecls m))
@@ -478,7 +485,7 @@ instance Rename Type where
     go (TChar c)     = return (TChar c)
     go  TInf         = return TInf
 
-    go t@(TUser pn ps)
+    go (TUser pn ps)
       | i == packIdent "inf", null ps     = return TInf
       | i == packIdent "Bit", null ps     = return TBit
 
@@ -591,13 +598,10 @@ lookupFixity op =
     Nothing    -> (\x y -> TUser sym [x,y], Fixity NonAssoc 0)
 
   where
-  sym   = thing op
-  props = [ mkUnqual (packInfix "==")
-          , mkUnqual (packInfix ">=")
-          , mkUnqual (packInfix "<=") ]
-  lkp   = do n               <- Map.lookup (thing op) tfunNames
-             (fAssoc,fLevel) <- Map.lookup n tBinOpPrec
-             return (n,Fixity { .. })
+  sym = thing op
+  lkp = do n               <- Map.lookup (thing op) tfunNames
+           (fAssoc,fLevel) <- Map.lookup n tBinOpPrec
+           return (n,Fixity { .. })
 
 -- | Rename a binding.
 instance Rename Bind where

src/Cryptol/TypeCheck/Monad.hs

@@ -5,8 +5,9 @@
 -- Maintainer  :  cryptol@galois.com
 -- Stability   :  provisional
 -- Portability :  portable
+{-# LANGUAGE Trustworthy #-}
 
-{-# LANGUAGE RecordWildCards, CPP, Safe #-}
+{-# LANGUAGE RecordWildCards, CPP #-}
 #if __GLASGOW_HASKELL__ >= 706
 {-# LANGUAGE RecursiveDo #-}
 #else
@@ -18,7 +19,8 @@ module Cryptol.TypeCheck.Monad
   , module Cryptol.TypeCheck.InferTypes
   ) where
 
-import           Cryptol.ModuleSystem.Name (SupplyT,runSupplyT,FreshM(..),Supply)
+import           Cryptol.ModuleSystem.Name (SupplyT,runSupplyT,FreshM(..),Supply
+                      ,nameIdent,lookupPrimDecl)
 import           Cryptol.Parser.Position
 import qualified Cryptol.Parser.AST as P
 import           Cryptol.TypeCheck.AST
@@ -46,6 +48,8 @@ import Control.DeepSeq
 import           Data.Functor
 #endif
 
+import Debug.Trace
+
 -- | Information needed for type inference.
 data InferInput = InferInput
   { inpRange     :: Range             -- ^ Location of program source
@@ -475,7 +479,12 @@ lookupVar x =
          do mbNT <- lookupNewtype x
             case mbNT of
               Just nt -> return (ExtVar (newtypeConType nt))
-              Nothing -> do recordError $ UndefinedVariable x
+              Nothing -> do () <- traceShowM ("var", x)
+                            ps <- getPrimMap
+                            traceShowM ("prim", lookupPrimDecl (nameIdent x) ps)
+                            RO { .. } <- IM ask
+                            traceShowM (Map.keys iVars)
+                            recordError $ UndefinedVariable x
                             a <- newType (text "type of" <+> pp x) KType
                             return $ ExtVar $ Forall [] [] a