Factor out new function listParamSubst.

src/Cryptol/ModuleSystem/InstantiateModule.hs

@@ -14,7 +14,7 @@ import Cryptol.Parser.Position(Located(..))
 import Cryptol.ModuleSystem.Name
 import Cryptol.ModuleSystem.Exports(ExportSpec(..))
 import Cryptol.TypeCheck.AST
-import Cryptol.TypeCheck.Subst(listSubst, apSubst)
+import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
 import Cryptol.Utils.Ident(ModName,modParamIdent)
 
 {-
@@ -51,8 +51,7 @@ instantiateModule func newName tpMap vpMap =
            renamedTySyns   = rnMp tsName (mTySyns func)
            renamedNewtypes = rnMp ntName (mNewtypes func)
 
-           su = listSubst
-                  [ (TVBound tp, t) | (tp,t) <- Map.toList (tyParamMap env) ]
+           su = listParamSubst (Map.toList (tyParamMap env))
 
            goals = map (fmap (apSubst su)) (mParamConstraints func)
            -- Constraints to discharge about the type instances

src/Cryptol/REPL/Command.hs

@@ -1200,7 +1200,7 @@ replEvalExpr expr =
           Nothing -> raise (EvalPolyError sig)
           Just (tys,def1) ->
             do warnDefaults tys
-               let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
+               let su = T.listParamSubst tys
                return (def1, T.apSubst su (T.sType sig))
 
      val <- liftModuleCmd (rethrowEvalError . M.evalExpr def1)

src/Cryptol/Transform/Specialize.hs

@@ -320,7 +320,7 @@ instantiateSchema ts n (Forall params props ty)
   | length params /= length ts = fail "instantiateSchema: wrong number of type arguments"
   | length props /= n          = fail "instantiateSchema: wrong number of prop arguments"
   | otherwise                  = return $ Forall [] [] (apSubst sub ty)
-  where sub = listSubst [ (tpVar p, t) | (p, t) <- zip params ts ]
+  where sub = listParamSubst (zip params ts)
 
 -- | Reduce `length ts` outermost type abstractions and `n` proof abstractions.
 instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr

src/Cryptol/TypeCheck/CheckModuleInstance.hs

@@ -138,7 +138,7 @@ checkValParams func tMap inst =
   defByParam = [ (nameIdent x, (x, mvpType s)) |
                                     (x,s) <- Map.toList (mParamFuns inst) ]
 
-  su = listSubst [ (TVBound x, t) | (x,t) <- Map.toList tMap ]
+  su = listParamSubst (Map.toList tMap)
 
   checkParam pr =
     let x = mvpName pr

src/Cryptol/TypeCheck/Instantiate.hs

@@ -11,7 +11,7 @@ module Cryptol.TypeCheck.Instantiate (instantiateWith) where
 import Cryptol.ModuleSystem.Name (nameIdent)
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Monad
-import Cryptol.TypeCheck.Subst (listSubst,apSubst)
+import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
 import Cryptol.TypeCheck.Error
 import Cryptol.Parser.Position (Located(..))
 import Cryptol.Utils.Ident (Ident)
@@ -147,7 +147,7 @@ instantiateWithNames nm e (Forall as ps t) xs =
 
 doInst :: [(TParam, Type)] -> Expr -> [Prop] -> Type -> InferM (Expr,Type)
 doInst su' e ps t =
-  do let su = listSubst [ (tpVar tp, ty) | (tp, ty) <- su' ]
+  do let su = listParamSubst su'
      newGoals (CtInst e) (map (apSubst su) ps)
      let t1 = apSubst su t
 

src/Cryptol/TypeCheck/Monad.hs

@@ -894,9 +894,9 @@ kExistTVar :: Name -> Kind -> KindM Type
 kExistTVar x k = kInInferM $ existVar x k
 
 -- | Replace the given bound variables with concrete types.
-kInstantiateT :: Type -> [(TParam,Type)] -> KindM Type
+kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
 kInstantiateT t as = return (apSubst su t)
-  where su = listSubst [ (tpVar x, t1) | (x,t1) <- as ]
+  where su = listParamSubst as
 
 {- | Record the kind for a local type variable.
 This assumes that we already checked that there was no other valid

src/Cryptol/TypeCheck/Solve.hs

@@ -28,7 +28,7 @@ import           Cryptol.TypeCheck.SimpType(tWidth)
 import           Cryptol.TypeCheck.Error(Error(..),Warning(..))
 import           Cryptol.TypeCheck.Subst
                     (apSubst, isEmptySubst, substToList,
-                          emptySubst,Subst,(@@), Subst, listSubst)
+                          emptySubst,Subst,(@@), Subst, listParamSubst)
 import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
 import           Cryptol.TypeCheck.Solver.Types
 import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
@@ -171,7 +171,7 @@ defaultReplExpr sol expr sch =
 
   where
   validate binds =
-    let su = listSubst [ (tpVar x, t) | (x,t) <- binds ]
+    let su = listParamSubst binds
     in null (concatMap pSplitAnd (apSubst su (sProps sch)))
 
   (numVs,otherVs) = partition (kindIs KNum) (sVars sch)

src/Cryptol/TypeCheck/Solver/Selector.hs

@@ -14,7 +14,7 @@ import Cryptol.TypeCheck.Monad( InferM, unify, newGoals, lookupNewtype
                               , newType, applySubst, solveHasGoal
                               , newParamName
                               )
-import Cryptol.TypeCheck.Subst(listSubst,apSubst)
+import Cryptol.TypeCheck.Subst (listParamSubst, apSubst)
 import Cryptol.Utils.Ident (Ident, packIdent)
 import Cryptol.Utils.Panic(panic)
 
@@ -75,7 +75,7 @@ solveSelector sel outerT =
                  case lookup l (ntFields nt) of
                    Nothing -> return Nothing
                    Just t  ->
-                     do let su = listSubst (zip (map tpVar (ntParams nt)) ts)
+                     do let su = listParamSubst (zip (ntParams nt) ts)
                         newGoals (CtPartialTypeFun $ UserTyFun x)
                           $ apSubst su $ ntConstraints nt
                         return $ Just $ apSubst su t

src/Cryptol/TypeCheck/Subst.hs

@@ -18,6 +18,7 @@ module Cryptol.TypeCheck.Subst
   , (@@)
   , defaultingSubst
   , listSubst
+  , listParamSubst
   , isEmptySubst
   , FVS(..)
   , apSubstMaybe
@@ -114,6 +115,18 @@ listSubst xs
         TVFree i _ _ _ -> Left (i, x)
         TVBound tp -> Right (tpUnique tp, x)
 
+-- | Makes a substitution out of a list.
+-- WARNING: We do not validate the list in any way, so the caller should
+-- ensure that we end up with a valid (e.g., idempotent) substitution.
+listParamSubst :: [(TParam, Type)] -> Subst
+listParamSubst xs
+  | null xs   = emptySubst
+  | otherwise = S { suFreeMap = IntMap.empty
+                  , suBoundMap = IntMap.fromList bounds
+                  , suDefaulting = False }
+  where
+    bounds = [ (tpUnique tp, (TVBound tp, t)) | (tp, t) <- xs ]
+
 isEmptySubst :: Subst -> Bool
 isEmptySubst su = IntMap.null (suFreeMap su) && IntMap.null (suBoundMap su)