Merge remote-tracking branch 'origin/master' into wip/cs

Makefile

@@ -1,7 +1,7 @@
 UNAME   := $(shell uname -s)
 ARCH    := $(shell uname -m)
 
-TESTS ?= issues regression renamer
+TESTS ?= issues regression renamer mono-binds
 TEST_DIFF ?= meld
 
 CABAL_FLAGS ?= -j
@@ -70,7 +70,7 @@ src/GitRev.hs:
 
 
 CRYPTOL_DEPS := \
-  $(shell find src cryptol \( -name \*.hs -or -name \*.x -or -name \*.y \) -print) \
+  $(shell find src cryptol \( -name \*.hs -or -name \*.x -or -name \*.y \) -and \( -not -name \*\#\* \) -print) \
   $(shell find lib -name \*.cry)
 
 print-%:

cryptol/REPL/Command.hs

@@ -241,6 +241,8 @@ evalCmd str = do
       ppOpts <- getPPValOpts
       io $ rethrowEvalError $ print $ pp $ E.WithBase ppOpts val
     P.LetInput decl -> do
+      -- explicitly make this a top-level declaration, so that it will
+      -- be generalized if mono-binds is enabled
       replEvalDecl decl
 
 data QCMode = QCRandom | QCExhaust deriving (Eq, Show)
@@ -498,7 +500,7 @@ loadCmd path
         , lPath = path
         }
 
-      m <- moduleCmdResult =<< io (M.loadModuleByPath path)
+      m <- liftModuleCmd (M.loadModuleByPath path)
       whenDebug (io (putStrLn (dump m)))
       setLoadedMod LoadedModule
         { lName = Just (T.mName m)
@@ -675,6 +677,7 @@ moduleCmdResult (res,ws0) = do
 replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
 replCheckExpr e = liftModuleCmd $ M.checkExpr e
 
+-- | Check declarations as though they were defined at the top-level.
 replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
 replCheckDecls ds = do
   npds <- liftModuleCmd $ M.noPat ds
@@ -688,7 +691,8 @@ replCheckDecls ds = do
         setDynEnv denv
         raise exn
   setDynEnv denv'
-  catch (liftModuleCmd $ M.checkDecls npds) undo
+  let topDecls = [ P.Decl (P.TopLevel P.Public d) | d <- npds ]
+  catch (liftModuleCmd $ M.checkDecls topDecls) undo
 
 replSpecExpr :: T.Expr -> REPL T.Expr
 replSpecExpr e = liftModuleCmd $ S.specialize e

cryptol/REPL/Monad.hs

@@ -8,6 +8,8 @@
 
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE LambdaCase #-}
 
 module REPL.Monad (
     -- * REPL Monad
@@ -388,9 +390,11 @@ setUser name val = case lookupTrie name userOptions of
         writeEnv (EnvBool False)
       | otherwise ->
         io (putStrLn ("Failed to parse boolean for field, `" ++ name ++ "`"))
+    where
 
-  writeEnv ev =
-    modifyRW_ (\rw -> rw { eUserEnv = Map.insert name ev (eUserEnv rw) })
+    writeEnv ev =
+      do optEff opt ev
+         modifyRW_ (\rw -> rw { eUserEnv = Map.insert name ev (eUserEnv rw) })
 
 -- | Get a user option, using Maybe for failure.
 tryGetUser :: String -> REPL (Maybe EnvVal)
@@ -421,28 +425,39 @@ data OptionDescr = OptionDescr
   , optDefault :: EnvVal
   , optCheck   :: EnvVal -> IO (Maybe String)
   , optHelp    :: String
+  , optEff     :: EnvVal -> REPL ()
   }
 
+simpleOpt :: String -> EnvVal -> (EnvVal -> IO (Maybe String)) -> String
+          -> OptionDescr
+simpleOpt optName optDefault optCheck optHelp =
+  OptionDescr { optEff = \ _ -> return (), .. }
+
 userOptions :: OptionMap
 userOptions  = mkOptionMap
-  [ OptionDescr "base" (EnvNum 16) checkBase
+  [ simpleOpt "base" (EnvNum 16) checkBase
     "the base to display words at"
-  , OptionDescr "debug" (EnvBool False) (const $ return Nothing)
+  , simpleOpt "debug" (EnvBool False) (const $ return Nothing)
     "enable debugging output"
-  , OptionDescr "ascii" (EnvBool False) (const $ return Nothing)
+  , simpleOpt "ascii" (EnvBool False) (const $ return Nothing)
     "display 7- or 8-bit words using ASCII notation."
-  , OptionDescr "infLength" (EnvNum 5) checkInfLength
+  , simpleOpt "infLength" (EnvNum 5) checkInfLength
     "The number of elements to display for infinite sequences."
-  , OptionDescr "tests" (EnvNum 100) (const $ return Nothing)
+  , simpleOpt "tests" (EnvNum 100) (const $ return Nothing)
     "The number of random tests to try."
-  , OptionDescr "prover" (EnvString "cvc4") checkProver $
+  , simpleOpt "prover" (EnvString "cvc4") checkProver $
     "The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
-  , OptionDescr "iteSolver" (EnvBool False) (const $ return Nothing)
+  , simpleOpt "iteSolver" (EnvBool False) (const $ return Nothing)
     "Use smt solver to filter conditional branches in proofs."
-  , OptionDescr "warnDefaulting" (EnvBool True) (const $ return Nothing)
+  , simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
     "Choose if we should display warnings when defaulting."
-  , OptionDescr "smtfile" (EnvString "-") (const $ return Nothing)
+  , simpleOpt "smtfile" (EnvString "-") (const $ return Nothing)
     "The file to use for SMT-Lib scripts (for debugging or offline proving)"
+  , OptionDescr "mono-binds" (EnvBool True) (const $ return Nothing)
+    "Whether or not to generalize bindings in a where-clause" $
+    \case EnvBool b -> do me <- getModuleEnv
+                          setModuleEnv me { M.meMonoBinds = b }
+          _         -> return ()
   ]
 
 -- | Check the value to the `base` option.

docs/ProgrammingCryptol/appendices/Syntax.tex

@@ -333,6 +333,10 @@ f p1 p2 = e              // Function definition
 e where ds
 \end{verbatim}
 
+Note that by default, any local declarations without type signatures
+are monomorphized. If you need a local declaration to be polymorphic,
+use an explicit type signature.
+
 \section{Explicit Type Instantiation}\label{explicit-type-instantiation}
 
 If \texttt{f} is a polymorphic value with type:

docs/Syntax.md

@@ -296,6 +296,10 @@ Local Declarations
 
     e where ds
 
+Note that by default, any local declarations without type signatures
+are monomorphized. If you need a local declaration to be polymorphic,
+use an explicit type signature.
+
 Explicit Type Instantiation
 ===========================
 

src/Cryptol/ModuleSystem.hs

@@ -31,10 +31,13 @@ import qualified Cryptol.Eval.Value        as E
 import           Cryptol.ModuleSystem.Env
 import           Cryptol.ModuleSystem.Interface
 import           Cryptol.ModuleSystem.Monad
+import           Cryptol.ModuleSystem.Renamer (Rename)
 import qualified Cryptol.ModuleSystem.Base as Base
 import qualified Cryptol.Parser.AST        as P
 import           Cryptol.Parser.NoPat (RemovePatterns)
+import           Cryptol.Parser.Position (HasLoc)
 import qualified Cryptol.TypeCheck.AST     as T
+import qualified Cryptol.TypeCheck.Depends as T
 
 
 -- Public Interface ------------------------------------------------------------
@@ -48,13 +51,11 @@ findModule :: P.ModName -> ModuleCmd FilePath
 findModule n env = runModuleM env (Base.findModule n)
 
 -- | Load the module contained in the given file.
-loadModuleByPath :: FilePath -> IO (ModuleRes T.Module)
-loadModuleByPath path = do
-  env <- initialModuleEnv
-  runModuleM env $ do
-    m <- Base.loadModuleByPath path
-    setFocusedModule (T.mName m)
-    return m
+loadModuleByPath :: FilePath -> ModuleCmd T.Module
+loadModuleByPath path env = runModuleM (resetModuleEnv env) $ do
+  m <- Base.loadModuleByPath path
+  setFocusedModule (T.mName m)
+  return m
 
 -- | Load the given parsed module.
 loadModule :: FilePath -> P.Module -> ModuleCmd T.Module
@@ -79,7 +80,7 @@ evalExpr :: T.Expr -> ModuleCmd E.Value
 evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
 -- | Typecheck declarations.
-checkDecls :: [P.Decl] -> ModuleCmd [T.DeclGroup]
+checkDecls :: (HasLoc d, Rename d, T.FromDecl d) => [d] -> ModuleCmd [T.DeclGroup]
 checkDecls ds env = runModuleM env (interactive (Base.checkDecls ds))
 
 -- | Evaluate declarations and add them to the extended environment.

src/Cryptol/ModuleSystem/Base.hs

@@ -23,6 +23,7 @@ import Cryptol.Parser.NoInclude (removeIncludesModule)
 import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
 import qualified Cryptol.TypeCheck     as T
 import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.TypeCheck.Depends as T
 import Cryptol.Utils.PP (pretty)
 
 import Cryptol.Transform.MonoValues
@@ -72,7 +73,7 @@ renameExpr e = do
   rename (deNames denv `R.shadowing` R.namingEnv env) e
 
 -- | Rename declarations in the context of the focused module.
-renameDecls :: [P.Decl] -> ModuleM [P.Decl]
+renameDecls :: (R.Rename d, T.FromDecl d) => [d] -> ModuleM [d]
 renameDecls ds = do
   env <- getFocusedEnv
   denv <- getDynEnv
@@ -246,7 +247,7 @@ checkExpr e = do
   typecheck T.tcExpr re env'
 
 -- | Typecheck a group of declarations.
-checkDecls :: [P.Decl] -> ModuleM [T.DeclGroup]
+checkDecls :: (HasLoc d, R.Rename d, T.FromDecl d) => [d] -> ModuleM [T.DeclGroup]
 checkDecls ds = do
   -- nopat must already be run
   rds <- renameDecls ds
@@ -308,6 +309,7 @@ importIfacesTc is =
 genInferInput :: Range -> IfaceDecls -> ModuleM T.InferInput
 genInferInput r env = do
   seeds <- getNameSeeds
+  monoBinds <- getMonoBinds
 
   -- TODO: include the environment needed by the module
   return T.InferInput
@@ -316,6 +318,7 @@ genInferInput r env = do
     , T.inpTSyns     =                    filterEnv ifTySyns
     , T.inpNewtypes  =                    filterEnv ifNewtypes
     , T.inpNameSeeds = seeds
+    , T.inpMonoBinds = monoBinds
     }
   where
   -- at this point, the names used in the aggregate interface should be

src/Cryptol/ModuleSystem/Env.hs

@@ -37,6 +37,16 @@ data ModuleEnv = ModuleEnv
   , meFocusedModule :: Maybe ModName
   , meSearchPath    :: [FilePath]
   , meDynEnv        :: DynamicEnv
+  , meMonoBinds     :: !Bool
+  }
+
+resetModuleEnv :: ModuleEnv -> ModuleEnv
+resetModuleEnv env = env
+  { meLoadedModules = mempty
+  , meNameSeeds     = T.nameSeeds
+  , meEvalEnv       = mempty
+  , meFocusedModule = Nothing
+  , meDynEnv        = mempty
   }
 
 initialModuleEnv :: IO ModuleEnv
@@ -56,6 +66,7 @@ initialModuleEnv  = do
     , meFocusedModule = Nothing
     , meSearchPath    = [dataDir </> "lib", instDir1 </> "lib", instDir2 </> "lib", "."]
     , meDynEnv        = mempty
+    , meMonoBinds     = True
     }
 
 -- | Try to focus a loaded module in the module environment.

src/Cryptol/ModuleSystem/Monad.hs

@@ -305,6 +305,14 @@ getIface mn = ModuleT $ do
 getNameSeeds :: ModuleM T.NameSeeds
 getNameSeeds  = ModuleT (meNameSeeds `fmap` get)
 
+getMonoBinds :: ModuleM Bool
+getMonoBinds  = ModuleT (meMonoBinds `fmap` get)
+
+setMonoBinds :: Bool -> ModuleM ()
+setMonoBinds b = ModuleT $ do
+  env <- get
+  set $! env { meMonoBinds = b }
+
 setNameSeeds :: T.NameSeeds -> ModuleM ()
 setNameSeeds seeds = ModuleT $ do
   env <- get

src/Cryptol/TypeCheck.hs

@@ -65,7 +65,7 @@ tcExpr e0 inp = runInferM inp
                              , show e'
                              , show t
                              ]
-      _ -> do res <- inferBinds False
+      _ -> do res <- inferBinds True False
                 [ P.Bind
                     { P.bName      = P.Located (inpRange inp)
                                    $ mkUnqual (P.Name "(expression)")

src/Cryptol/TypeCheck/Depends.hs

@@ -81,6 +81,7 @@ orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses)
 class FromDecl d where
   toBind    :: d -> Maybe P.Bind
   toTyDecl  :: d -> Maybe TyDecl
+  isTopDecl :: d -> Bool
 
 instance FromDecl P.TopDecl where
   toBind (P.Decl x)         = toBind (P.tlValue x)
@@ -90,6 +91,8 @@ instance FromDecl P.TopDecl where
   toTyDecl (P.Decl x)       = toTyDecl (P.tlValue x)
   toTyDecl _                = Nothing
 
+  isTopDecl _               = True
+
 instance FromDecl P.Decl where
   toBind (P.DLocated d _) = toBind d
   toBind (P.DBind b)      = return b
@@ -99,6 +102,8 @@ instance FromDecl P.Decl where
   toTyDecl (P.DType x)      = Just (TS x)
   toTyDecl _                = Nothing
 
+  isTopDecl _               = False
+
 {- | Given a list of declarations, annoted with (i) the names that they
 define, and (ii) the names that they use, we compute a list of strongly
 connected components of the declarations.  The SCCs are in dependency order. -}

src/Cryptol/TypeCheck/Infer.hs

@@ -43,7 +43,7 @@ import qualified Data.Map as Map
 import           Data.Map (Map)
 import qualified Data.Set as Set
 import           Data.Either(partitionEithers)
-import           Data.Maybe(mapMaybe)
+import           Data.Maybe(mapMaybe,isJust)
 import           Data.List(partition)
 import           Data.Graph(SCC(..))
 import           Data.Traversable(forM)
@@ -419,9 +419,14 @@ inferCArm armNum (m : ms) =
      newGoals CtComprehension [ sz =#= (n .*. n') ]
      return (m1 : ms', Map.insertWith (\_ old -> old) x t ds, sz)
 
-
-inferBinds :: Bool -> [P.Bind] -> InferM [Decl]
-inferBinds isRec binds =
+-- | @inferBinds isTopLevel isRec binds@ performs inference for a
+-- strongly-connected component of 'P.Bind's. If @isTopLevel@ is true,
+-- any bindings without type signatures will be generalized. If it is
+-- false, and the mono-binds flag is enabled, no bindings without type
+-- signatures will be generalized, but bindings with signatures will
+-- be unaffected.
+inferBinds :: Bool -> Bool -> [P.Bind] -> InferM [Decl]
+inferBinds isTopLevel isRec binds =
   mdo let exprMap = Map.fromList [ (x,inst (EVar x) (dDefinition b))
                                  | b <- genBs, let x = dName b ] -- REC.
 
@@ -429,7 +434,14 @@ inferBinds isRec binds =
           inst e (EProofAbs _ e1) = inst (EProofApp e) e1
           inst e _                = e
 
+      -- when mono-binds is enabled, and we're not checking top-level
+      -- declarations, mark all bindings lacking signatures as monomorphic
+      monoBinds <- getMonoBinds
+      let binds' | monoBinds && not isTopLevel = sigs ++ monos
+                 | otherwise                   = binds
 
+          (sigs,noSigs) = partition (isJust . P.bSignature) binds
+          monos         = [ b { P.bMono = True } | b <- noSigs ]
 
 
       ((doneBs, genCandidates), cs) <-
@@ -438,7 +450,7 @@ inferBinds isRec binds =
         {- Guess type is here, because while we check user supplied signatures
            we may generate additional constraints. For example, `x - y` would
            generate an additional constraint `x >= y`. -}
-        do (newEnv,todos) <- unzip `fmap` mapM (guessType exprMap) binds
+        do (newEnv,todos) <- unzip `fmap` mapM (guessType exprMap) binds'
            let extEnv = if isRec then withVarTypes newEnv else id
 
            extEnv $
@@ -643,6 +655,8 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
 inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
 inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
   where
+  isTopLevel = isTopDecl (head ds)
+
   checkTyDecls (TS t : ts) =
     do t1 <- checkTySyn t
        withTySyn t1 (checkTyDecls ts)
@@ -656,13 +670,13 @@ inferDs ds continue = checkTyDecls =<< orderTyDecls (mapMaybe toTyDecl ds)
 
 
   checkBinds decls (CyclicSCC bs : more) =
-     do bs1 <- inferBinds True bs
+     do bs1 <- inferBinds isTopLevel True bs
         foldr (\b m -> withVar (dName b) (dSignature b) m)
               (checkBinds (Recursive bs1 : decls) more)
               bs1
 
   checkBinds decls (AcyclicSCC c : more) =
-    do [b] <- inferBinds False [c]
+    do [b] <- inferBinds isTopLevel False [c]
        withVar (dName b) (dSignature b) $
          checkBinds (NonRecursive b : decls) more
 

src/Cryptol/TypeCheck/Monad.hs

@@ -44,6 +44,8 @@ data InferInput = InferInput
   , inpTSyns     :: Map QName TySyn   -- ^ Type synonyms that are in scope
   , inpNewtypes  :: Map QName Newtype -- ^ Newtypes in scope
   , inpNameSeeds :: NameSeeds         -- ^ Private state of type-checker
+  , inpMonoBinds :: Bool              -- ^ Should local bindings without
+                                      --   signatures be monomorphized?
   } deriving Show
 
 
@@ -77,6 +79,7 @@ runInferM info (IM m) =
                      , iTSyns         = fmap mkExternal (inpTSyns info)
                      , iNewtypes      = fmap mkExternal (inpNewtypes info)
                      , iSolvedHasLazy = iSolvedHas finalRW     -- RECURSION
+                     , iMonoBinds     = inpMonoBinds info
                      }
 
          (result, finalRW) <- runStateT rw $ runReaderT ro m  -- RECURSION
@@ -145,6 +148,11 @@ data RO = RO
     -- together through recursion.  The field is here so that we can
     -- look thing up before they are defined, which is OK because we
     -- don't need to know the results until everything is done.
+
+  , iMonoBinds :: Bool
+    -- ^ When this flag is set to true, bindings that lack signatures
+    -- in where-blocks will never be generalized. Bindings with type
+    -- signatures, and all bindings at top level are unaffected.
   }
 
 -- | Read-write component of the monad.
@@ -468,6 +476,10 @@ getTVars = IM $ asks $ Set.fromList . mapMaybe tpName . iTVars
 getBoundInScope :: InferM (Set TVar)
 getBoundInScope = IM $ asks $ Set.fromList . map tpVar . iTVars
 
+-- | Retrieve the value of the `mono-binds` option.
+getMonoBinds :: InferM Bool
+getMonoBinds  = IM (asks iMonoBinds)
+
 {- | We disallow shadowing between type synonyms and type variables
 because it is confusing.  As a bonus, in the implementation we don't
 need to worry about where we lookup things (i.e., in the variable or

src/Cryptol/TypeCheck/Subst.hs

@@ -140,31 +140,34 @@ instance TVars a => TVars (TypeMap a) where
 
 -- | Apply the substitution to the keys of a type map.
 apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
-apSubstTypeMapKeys su = go
+apSubstTypeMapKeys su = go id
   where
 
-  go :: TypeMap a -> TypeMap a
-  go TM { .. } = foldl addKey tm' tys
+  go :: (a -> a) -> TypeMap a -> TypeMap a
+  go atNode TM { .. } = foldl addKey tm' tys
     where
 
     addKey tm (ty,a) = insertTM ty a tm
 
     tm' = TM { tvar = Map.fromList   vars
-             , tcon = fmap lgo tcon
-             , trec = fmap lgo trec
+             , tcon = fmap (lgo atNode) tcon
+             , trec = fmap (lgo atNode) trec
              }
 
     -- partition out variables that have been replaced with more specific types
     (vars,tys) = partitionEithers
                  [ case Map.lookup v (suMap su) of
-                     Just ty -> Right (ty,a)
-                     Nothing -> Left  (v,a)
+                     Just ty -> Right (ty,a')
+                     Nothing -> Left  (v, a')
 
                  | (v,a) <- Map.toList tvar
+                 , let a' = atNode a
                  ]
 
-  lgo :: List TypeMap a -> List TypeMap a
-  lgo k = k { cons = go (cons k) }
+  lgo :: (a -> a) -> List TypeMap a -> List TypeMap a
+  lgo atNode k = k { nil  = fmap atNode (nil k)
+                   , cons = go (lgo atNode) (cons k)
+                   }
 
 
 {- | WARNING: This instance assumes that the quantified variables in the

tests/issues/issue198.icry.stdout

@@ -1,19 +1,19 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at simon.cry2:83:16--92:15:
-  Defaulting 3rd type parameter
-             of expression (@)
-             at simon.cry2:89:29--89:30
-  to max (width (a`432 - 1)) (max 6 (width a`431))
-[warning] at simon.cry2:85:16--90:49:
-  Defaulting 3rd type parameter
-             of expression (@)
-             at simon.cry2:90:27--90:28
-  to width a`433
-[warning] at simon.cry2:85:16--90:49:
+[warning] at simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at simon.cry2:87:28--87:30
   to max 3 (width a`431)
+[warning] at simon.cry2:83:1--92:15:
+  Defaulting 3rd type parameter
+             of expression (@)
+             at simon.cry2:90:27--90:28
+  to width a`433
+[warning] at simon.cry2:83:1--92:15:
+  Defaulting 3rd type parameter
+             of expression (@)
+             at simon.cry2:89:29--89:30
+  to max 6 (max (width (a`432 - 1)) (width a`431))
 True

tests/issues/issue225.icry

@@ -1 +1,4 @@
+:set mono-binds=on
+:l issue225.cry
+:set mono-binds=off
 :l issue225.cry

tests/issues/issue225.icry.fails

@@ -1 +0,0 @@
-Known problem, see ticket #5.

tests/issues/issue225.icry.stdout

@@ -1,3 +1,46 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module EnigmaBroke
+Loading module Cryptol
+Loading module EnigmaBroke
+
+[error] at issue225.cry:12:1--12:11:
+  Failed to validate user-specified signature.
+    In the definition of 'EnigmaBroke::joinRotors', at issue225.cry:12:1--12:11:
+      for any type n
+        fin n
+      =>
+      fin (min n ?a8)
+        arising from
+        use of expression __p14
+        at issue225.cry:22:21--22:22
+      fin (min n ?u7)
+        arising from
+        use of expression __p14
+        at issue225.cry:22:9--22:19
+      fin (min n ?o7)
+        arising from
+        use of expression __p14
+        at issue225.cry:22:6--22:7
+      ?a8 == 1 + min n ?a8
+        arising from
+        use of expression __p14
+        at issue225.cry:22:21--22:22
+      ?u7 == 1 + min n ?u7
+        arising from
+        use of expression __p14
+        at issue225.cry:22:9--22:19
+      ?o7 == 1 + min n ?o7
+        arising from
+        use of expression __p14
+        at issue225.cry:22:6--22:7
+  where
+  ?o7 is 1st type parameter
+         of expression __p14
+         at issue225.cry:22:6--22:7
+  ?u7 is 1st type parameter
+         of expression __p14
+         at issue225.cry:22:9--22:19
+  ?a8 is 1st type parameter
+         of expression __p14
+         at issue225.cry:22:21--22:22

tests/mono-binds/test01.cry

@@ -0,0 +1,5 @@
+module test01 where
+
+a x = f x
+  where
+  f y = x # y

tests/mono-binds/test01.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test01.cry
+:set mono-binds=on
+:l test01.cry

tests/mono-binds/test01.icry.stdout

@@ -0,0 +1,33 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test01
+module test01
+import Cryptol
+/* Not recursive */
+test01::a : {a, b} (fin b) => [b]a -> [2 * b]a
+test01::a = \{a, b} (fin b) ->
+            (\ (x : [b]a) ->
+             f b x
+             where
+               /* Not recursive */
+               f : {c} [c]a -> [b + c]a
+               f = \{c} (y : [c]a) -> (#) b c a <> x y
+               
+             ) : [b]a -> [2 * b]a
+
+Loading module Cryptol
+Loading module test01
+module test01
+import Cryptol
+/* Not recursive */
+test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
+test01::a = \{a, b} (fin a) ->
+            (\ (x : [a]b) ->
+             f x
+             where
+               /* Not recursive */
+               f : [a]b -> [a + a]b
+               f = \ (y : [a]b) -> (#) a a b <> x y
+               
+             ) : [a]b -> [2 * a]b
+

tests/mono-binds/test02.cry

@@ -0,0 +1,6 @@
+module test02 where
+
+test a = f a
+  where
+  f x = g a
+  g x = f x

tests/mono-binds/test02.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test02.cry
+:set mono-binds=on
+:l test02.cry

tests/mono-binds/test02.icry.stdout

@@ -0,0 +1,35 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test02
+module test02
+import Cryptol
+/* Not recursive */
+test02::test : {a, b} a -> b
+test02::test = \{a, b} (a : a) ->
+               f b a
+               where
+                 /* Recursive */
+                 f : {c} a -> c
+                 f = \{c} (x : a) -> g c a
+                 g : {c} a -> c
+                 g = \{c} (x : a) -> f c x
+                 
+               
+
+Loading module Cryptol
+Loading module test02
+module test02
+import Cryptol
+/* Not recursive */
+test02::test : {a, b} a -> b
+test02::test = \{a, b} (a : a) ->
+               f a
+               where
+                 /* Recursive */
+                 f : a -> b
+                 f = \ (x : a) -> g a
+                 g : a -> b
+                 g = \ (x : a) -> f x
+                 
+               
+

tests/mono-binds/test03.cry

@@ -0,0 +1,9 @@
+module test03 where
+
+// expression with a free type variable. Since mono-binds
+// monomorphizes everything rather than using fancy rules to generalize
+// some local binds, this test probably isn't relevant anymore
+test : {a} (fin a, a >= width a) => [a]
+test = foo
+  where
+  foo = `(a)

tests/mono-binds/test03.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test03.cry
+:set mono-binds=on
+:l test03.cry

tests/mono-binds/test03.icry.stdout

@@ -0,0 +1,31 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test03
+module test03
+import Cryptol
+/* Not recursive */
+test03::test : {a} (fin a, a >= width a) => [a]
+test03::test = \{a} (fin a, a >= width a) ->
+               foo a <> <>
+               where
+                 /* Not recursive */
+                 foo : {b} (fin b, b >= width a) => [b]
+                 foo = \{b} (fin b, b >= width a) -> demote a b <> <> <>
+                 
+               
+
+Loading module Cryptol
+Loading module test03
+module test03
+import Cryptol
+/* Not recursive */
+test03::test : {a} (fin a, a >= width a) => [a]
+test03::test = \{a} (fin a, a >= width a) ->
+               foo
+               where
+                 /* Not recursive */
+                 foo : [a]
+                 foo = demote a a <> <> <>
+                 
+               
+

tests/mono-binds/test04.cry

@@ -0,0 +1,5 @@
+module test04 where
+
+test a = (f (), f 10)
+  where
+  f x = (a,x)

tests/mono-binds/test04.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test04.cry
+:set mono-binds=on
+:l test04.cry

tests/mono-binds/test04.icry.stdout

@@ -0,0 +1,32 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test04
+module test04
+import Cryptol
+/* Not recursive */
+test04::test : {a, b} (b >= 4, fin b) => a -> ((a, ()), (a, [b]))
+test04::test = \{a, b} (b >= 4, fin b) (a : a) ->
+               (f () (), f [b] (demote 10 b <> <> <>))
+               where
+                 /* Not recursive */
+                 f : {c} c -> (a, c)
+                 f = \{c} (x : c) -> (a, x)
+                 
+               
+
+Loading module Cryptol
+Loading module test04
+[warning] at test04.cry:1:1--5:14:
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at test04.cry:3:19--3:21
+  to 4
+
+[error] at test04.cry:3:17--3:21:
+  Type mismatch:
+    Expected type: [?b3]
+    Inferred type: ()
+  where
+  ?b3 is type parameter 'bits'
+         of literal or demoted expression
+         at test04.cry:3:19--3:21

tests/mono-binds/test05.cry

@@ -0,0 +1,14 @@
+module test05 where
+
+foo : [10]
+foo = 10
+
+test a = 10
+  where
+  foo : [10]
+  foo = 10
+
+  f = bar
+    where
+    foo = a
+    bar = zero # foo

tests/mono-binds/test05.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test05.cry
+:set mono-binds=on
+:l test05.cry

tests/mono-binds/test05.icry.stdout

@@ -0,0 +1,85 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test05
+[warning] at test05.cry:9:3--9:6
+    This binding for foo shadows the existing binding from
+    (at test05.cry:4:1--4:4, test05::foo)
+[warning] at test05.cry:13:5--13:8
+    This binding for foo shadows the existing binding from
+    (at test05.cry:9:3--9:6, foo)
+module test05
+import Cryptol
+/* Not recursive */
+test05::foo : [10]
+test05::foo = demote 10 10 <> <> <>
+
+/* Not recursive */
+test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
+test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
+               demote 10 c <> <> <>
+               where
+                 /* Not recursive */
+                 foo : [10]
+                 foo = demote 10 10 <> <> <>
+                 
+                 /* Not recursive */
+                 f : {d} (fin d) => [a + d]b
+                 f = \{d} (fin d) ->
+                     (bar d <>
+                      where
+                        /* Not recursive */
+                        foo : [a]b
+                        foo = a
+                        
+                        /* Not recursive */
+                        bar : {e} (fin e) => [e + a]b
+                        bar = \{e} (fin e) -> (#) e a b <> (zero ([e]b)) foo
+                        
+                      ) : [a + d]b
+                 
+               
+
+Loading module Cryptol
+Loading module test05
+[warning] at test05.cry:9:3--9:6
+    This binding for foo shadows the existing binding from
+    (at test05.cry:4:1--4:4, test05::foo)
+[warning] at test05.cry:13:5--13:8
+    This binding for foo shadows the existing binding from
+    (at test05.cry:9:3--9:6, foo)
+[warning] at test05.cry:1:1--14:21:
+  Defaulting 1st type parameter
+             of expression (#)
+             at test05.cry:14:16--14:17
+  to 0
+module test05
+import Cryptol
+/* Not recursive */
+test05::foo : [10]
+test05::foo = demote 10 10 <> <> <>
+
+/* Not recursive */
+test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
+test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
+               demote 10 c <> <> <>
+               where
+                 /* Not recursive */
+                 foo : [10]
+                 foo = demote 10 10 <> <> <>
+                 
+                 /* Not recursive */
+                 f : [0 + a]b
+                 f = bar
+                     where
+                       /* Not recursive */
+                       foo : [a]b
+                       foo = a
+                       
+                       /* Not recursive */
+                       bar : [0 + a]b
+                       bar = (#) 0 a b <> (zero ([0]b)) foo
+                       
+                     
+                 
+               
+

tests/mono-binds/test06.cry

@@ -0,0 +1,9 @@
+module test06 where
+
+test : {a} a -> a
+test a = bar
+  where
+  foo : a
+  foo = zero
+
+  bar = foo

tests/mono-binds/test06.icry

@@ -0,0 +1,5 @@
+:set debug=on
+:set mono-binds=off
+:l test06.cry
+:set mono-binds=on
+:l test06.cry

tests/mono-binds/test06.icry.stdout

@@ -0,0 +1,39 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module test06
+module test06
+import Cryptol
+/* Not recursive */
+test06::test : {a} a -> a
+test06::test = \{a} (a : a) ->
+               bar
+               where
+                 /* Not recursive */
+                 foo : a
+                 foo = zero a
+                 
+                 /* Not recursive */
+                 bar : a
+                 bar = foo
+                 
+               
+
+Loading module Cryptol
+Loading module test06
+module test06
+import Cryptol
+/* Not recursive */
+test06::test : {a} a -> a
+test06::test = \{a} (a : a) ->
+               bar
+               where
+                 /* Not recursive */
+                 foo : a
+                 foo = zero a
+                 
+                 /* Not recursive */
+                 bar : a
+                 bar = foo
+                 
+               
+

tests/regression/AES.icry.stdout

@@ -11,7 +11,7 @@ Loading module AES
              of expression (@)
              at AES.cry:147:58--147:59
   to 4
-[warning] at AES.cry:124:26--129:31:
+[warning] at AES.cry:124:1--124:9:
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at AES.cry:127:26--127:29

tests/regression/check11.icry.stdout

@@ -2,11 +2,11 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at :1:1--5:25:
-  Defaulting 1st type parameter
-             of expression zz
-             at check11.cry:1:11--1:13
+  Defaulting type parameter 'bits'
+             of finite enumeration
+             at check11.cry:3:10--3:19
   to 7
-[warning] at check11.cry:1:11--5:25:
+[warning] at :1:1--5:25:
   Defaulting 4th type parameter
              of expression (@@)
              at check11.cry:5:13--5:15

tests/regression/check25.icry.stdout

@@ -9,4 +9,9 @@ Loading module check25
              of expression check25::tx
              at check25.cry:8:11--8:13
   to 4
+[warning] at check25.cry:1:1--8:19:
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at check25.cry:6:14--6:16
+  to 5
 True

tests/regression/layout01.icry.stdout

@@ -7,36 +7,16 @@ Assuming a = 1
 Assuming b = 2
 {x = 0x1, y = 0x2}
 [warning] at <interactive>:1:1--1:22:
-  Defaulting 2nd type parameter
-             of expression __p0
-             at <interactive>:1:10--1:11
-  to 2
-[warning] at <interactive>:1:1--1:22:
-  Defaulting 1st type parameter
-             of expression __p0
-             at <interactive>:1:12--1:13
-  to 1
-[warning] at <interactive>:1:1--1:22:
-  Defaulting 2nd type parameter
-             of expression __p0
-             at <interactive>:1:12--1:13
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:20--1:21
   to 2
 Assuming a = 1
 0x1
 [warning] at <interactive>:1:1--1:46:
-  Defaulting 2nd type parameter
-             of expression __p0
-             at <interactive>:1:15--1:16
-  to 5
-[warning] at <interactive>:1:1--1:46:
-  Defaulting 1st type parameter
-             of expression __p0
-             at <interactive>:1:22--1:23
-  to 4
-[warning] at <interactive>:1:1--1:46:
-  Defaulting 2nd type parameter
-             of expression __p0
-             at <interactive>:1:22--1:23
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:42--1:44
   to 5
 Assuming a = 4
 0xa

tests/regression/r01.icry.stdout

@@ -2,26 +2,26 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 [warning] at <interactive>:1:1--1:42:
-  Defaulting 1st type parameter
-             of expression ltTen
-             at <interactive>:1:5--1:10
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:40--1:42
   to 4
 True
 [warning] at <interactive>:1:1--1:43:
-  Defaulting 1st type parameter
-             of expression ltTen
-             at <interactive>:1:5--1:10
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:41--1:43
   to 4
 False
 [warning] at <interactive>:1:1--1:48:
-  Defaulting 1st type parameter
-             of expression ltTen
-             at <interactive>:1:5--1:10
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:46--1:48
   to 7
 False
 [warning] at <interactive>:1:1--1:47:
-  Defaulting 1st type parameter
-             of expression ltTen
-             at <interactive>:1:5--1:10
+  Defaulting type parameter 'bits'
+             of literal or demoted expression
+             at <interactive>:1:45--1:47
   to 7
 True