Add the mono-binds flag

When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.

The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.

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

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