16 files changed, 149 insertions, 243 deletions

diff --git a/src/interp/astr.boot b/src/interp/astr.boot
index 32f656fb..9597e934 100644
--- a/src/interp/astr.boot
+++ b/src/interp/astr.boot
@@ -35,9 +35,9 @@ import vmlisp
 namespace BOOT
 module astr where
   ncTag: %Thing -> %Symbol
-  ncAlist: %Thing -> %List
-  ncEltQ: (%List,%Thing) -> %Thing
-  ncPutQ: (%List,%Thing,%Thing) -> %Thing
+  ncAlist: %Thing -> %List %Thing
+  ncEltQ: (%List %Thing,%Thing) -> %Thing
+  ncPutQ: (%List %Thing,%Thing,%Thing) -> %Thing
 
 --% Attributed Structures (astr)
 -- For objects which are pairs where the first field is either just a tag
diff --git a/src/interp/c-util.boot b/src/interp/c-util.boot
index 619555d0..9cd39a91 100644
--- a/src/interp/c-util.boot
+++ b/src/interp/c-util.boot
@@ -39,7 +39,7 @@ namespace BOOT
 module c_-util where
   clearReplacement: %Symbol -> %Thing
   replaceSimpleFunctions: %Form -> %Form
-  foldExportedFunctionReferences: %List -> %List
+  foldExportedFunctionReferences: %List %Form -> %List %Form
   diagnoseUnknownType: (%Mode,%Env) -> %Form
   declareUnusedParameters: %Code -> %Code
   registerFunctionReplacement: (%Symbol,%Form) -> %Thing
@@ -143,7 +143,7 @@ isTupleInstance t ==
 
 ++ Returns true if the signature `sig' describes a function that can
 ++ accept a homogeneous variable length argument list.
-isHomoegenousVarargSignature: %Signature -> %Boolean
+isHomoegenousVarargSignature: %Sig -> %Boolean
 isHomoegenousVarargSignature sig ==
   #sig = 1 and isTupleInstance first sig
 
@@ -151,13 +151,13 @@ isHomoegenousVarargSignature sig ==
 ++ parameter type list `sig'.  This means that either the number
 ++ of arguments is exactly the number of parameters, or that the
 ++ signature describes a homogeneous vararg operation.
-enoughArguments: (%List,%Signature) -> %Boolean
+enoughArguments: (%List %Form,%Sig) -> %Boolean
 enoughArguments(args,sig) ==
   #args = #sig or isHomoegenousVarargSignature sig
 
 ++ Returns true if the operation described by the signature `sig'
 ++ wants its arguments as a Tuple object.
-wantArgumentsAsTuple: (%List,%Signature) -> %Boolean
+wantArgumentsAsTuple: (%List %Form,%Sig) -> %Boolean
 wantArgumentsAsTuple(args,sig) ==
   isHomoegenousVarargSignature sig and #args ~= #sig
 
@@ -1129,11 +1129,11 @@ clearReplacement name ==
 registerFunctionReplacement(name,body) ==
   LAM_,EVALANDFILEACTQ ["PUT",MKQ name,MKQ "SPADreplace",quoteMinimally body]
 
-eqSubstAndCopy: (%List, %List, %Form) -> %Form
+eqSubstAndCopy: (%List %Form, %List %Symbol, %Form) -> %Form
 eqSubstAndCopy(args,parms,body) ==
   SUBLIS(pairList(parms,args),body,KEYWORD::TEST,function EQ)
 
-eqSubst: (%List, %List, %Form) -> %Form
+eqSubst: (%List %Form, %List %Symbol, %Form) -> %Form
 eqSubst(args,parms,body) ==
   NSUBLIS(pairList(parms,args),body,KEYWORD::TEST,function EQ)
 
@@ -1319,7 +1319,7 @@ proclaimCapsuleFunction(op,sig) ==
         [first d, :[normalize(first args,false) for args in tails rest d]]
 
 ++ Lisp back end compiler for ILAM with `name', formal `args', and `body'.
-backendCompileILAM: (%Symbol,%List, %Code) -> %Symbol
+backendCompileILAM: (%Symbol,%List %Symbol, %Code) -> %Symbol
 backendCompileILAM(name,args,body) ==
   args' := NLIST(#args, ["GENSYM"])
   body' := eqSubst(args',args,body)
@@ -1351,7 +1351,7 @@ backendCompileNEWNAM x ==
 ++ its values are cached, so that equal lists of argument values
 ++ yield equal values.  The arguments-value pairs are stored
 ++ as alists.
-backendCompileSLAM: (%Symbol,%List,%Code) -> %Symbol
+backendCompileSLAM: (%Symbol,%List %Symbol,%Code) -> %Symbol
 backendCompileSLAM(name,args,body) ==
   al := mkCacheName name        -- name of the cache alist.
   auxfn := INTERNL(name,'";")   -- name of the worker function.
@@ -1383,7 +1383,7 @@ backendCompileSLAM(name,args,body) ==
 
 ++ Same as backendCompileSLAM, except that the cache is a hash
 ++ table.  This backend compiler is used to compile constructors.
-backendCompileSPADSLAM: (%Symbol,%List,%Code) -> %Symbol
+backendCompileSPADSLAM: (%Symbol,%List %Symbol,%Code) -> %Symbol
 backendCompileSPADSLAM(name,args,body) ==
   al := mkCacheName name       -- name of the cache hash table.
   auxfn := INTERNL(name,'";")  -- name of the worker function.
@@ -1450,7 +1450,7 @@ $SpecialVars := []
 
 
 ++ push `x' into the list of local variables.
-pushLocalVariable: %Symbol -> %List
+pushLocalVariable: %Symbol -> %List %Symbol
 pushLocalVariable x ==
   p := symbolName x
   x ~= "$" and stringChar(p,0) = char "$" and
@@ -1519,21 +1519,21 @@ massageBackendCode x ==
   massageBackendCode rest x
 
 
-skipDeclarations: %List -> %List
+skipDeclarations: %List %Code -> %List %Code
 skipDeclarations form ==
   while first form is ["DECLARE",:.] repeat
     form := rest form
   form
 
 ++ return the last node containing a declaration in form, otherwise nil.
-lastDeclarationNode: %List -> %List
+lastDeclarationNode: %List %Code -> %List %Code
 lastDeclarationNode form ==
   while second form is ["DECLARE",:.] repeat
      form := rest form
   first form is ["DECLARE",:.] => form
   nil
 
-declareGlobalVariables: %List -> %List
+declareGlobalVariables: %List %Symbol -> %Code
 declareGlobalVariables vars ==
   ["DECLARE",["SPECIAL",:vars]]
 
diff --git a/src/interp/category.boot b/src/interp/category.boot
index c562a43c..07447181 100644
--- a/src/interp/category.boot
+++ b/src/interp/category.boot
@@ -82,12 +82,12 @@ CategoryPrint(D,$e) ==
     atom first u => SAY("Alternate View corresponding to: ",u)
     PRETTYPRINT u
 
-++ Returns a fresly built category object for a domain or package
+++ Returns a freshly built category object for a domain or package
 ++ (as indicated by `domainOrPackage'), with signature list
 ++ designated by `sigList', attribute list designated by `attList',
 ++ used domains list designated by `domList', and a princical ancestor
 ++ category object designated by `PrincipalAncestor'.
-mkCategory: (%Symbol,%List,%List,%List, %Maybe %Shell) -> %Shell
+mkCategory: (%ConstructorKind,%List %Sig,%List %Form,%List %Instantiation, %Maybe %Shell) -> %Shell
 mkCategory(domainOrPackage,sigList,attList,domList,PrincipalAncestor) ==
   NSigList := nil
   -- Unless extending a principal ancestor (from the end), start
@@ -102,10 +102,12 @@ mkCategory(domainOrPackage,sigList,attList,domList,PrincipalAncestor) ==
          -- ??? Should we not check for predicate subsumption too?
          or/[x is [[ =sig,.,:impl],:num] for x in NSigList] => [sig,pred,:impl]
                  --only needed for multiple copies of sig
-         num:= if domainOrPackage="domain" then count else count-5
-         nsig:= mkOperatorEntry(sig,pred,num)
-         NSigList:= [[nsig,:count],:NSigList]
-         count:= count+1
+         num :=
+           domainOrPackage is "domain" => count
+           count-5
+         nsig := mkOperatorEntry(sig,pred,num)
+         NSigList := [[nsig,:count],:NSigList]
+         count := count+1
          nsig
      else s for s in sigList]
   NewLocals:= nil
@@ -361,7 +363,7 @@ CatEval x ==
 --               --remove the slot pointers
 --  [x for x in l | not AncestorP(x.0,leaves)]
  
-AncestorP: (%Form, %List) -> %Form
+AncestorP: (%Form, %List %Instantiation) -> %Form
 AncestorP(xname,leaves) ==
   -- checks for being a principal ancestor of one of the leaves
   listMember?(xname,leaves) => xname
diff --git a/src/interp/compiler.boot b/src/interp/compiler.boot
index df6c4848..60d1e521 100644
--- a/src/interp/compiler.boot
+++ b/src/interp/compiler.boot
@@ -44,13 +44,13 @@ module compiler where
   comp: (%Form,%Mode,%Env) -> %Maybe %Triple
   compOrCroak: (%Form,%Mode,%Env) -> %Maybe %Triple
   compCompilerPredicate: (%Form,%Env) -> %Maybe %Triple
-  checkCallingConvention: (%List,%Short) -> %SimpleArray %Short
+  checkCallingConvention: (%List %Sig,%Short) -> %SimpleArray %Short
 
 
 --% 
 compUniquely: (%Form,%Mode,%Env) -> %Maybe %Triple
 compNoStacking: (%Form,%Mode,%Env) -> %Maybe %Triple
-compNoStacking1: (%Form,%Mode,%Env,%List) -> %Maybe %Triple
+compNoStacking1: (%Form,%Mode,%Env,%List %Thing) -> %Maybe %Triple
 compOrCroak1: (%Form,%Mode,%Env,%Thing) -> %Maybe %Triple
 comp2: (%Form,%Mode,%Env) -> %Maybe %Triple
 comp3: (%Form,%Mode,%Env) -> %Maybe %Triple
@@ -60,22 +60,22 @@ compSymbol: (%Form,%Mode,%Env) -> %Maybe %Triple
 compTypeOf: (%Form,%Mode,%Env) -> %Maybe %Triple
 compForm: (%Form,%Mode,%Env) -> %Maybe %Triple
 compForm1: (%Form,%Mode,%Env) -> %Maybe %Triple
-compForm2: (%Form,%Mode,%Env,%List) -> %Maybe %Triple
-compForm3: (%Form,%Mode,%Env,%List) -> %Maybe %Triple
+compForm2: (%Form,%Mode,%Env,%List %Modemap) -> %Maybe %Triple
+compForm3: (%Form,%Mode,%Env,%List %Modemap) -> %Maybe %Triple
 compArgumentsAndTryAgain: (%Form,%Mode,%Env) -> %Maybe %Triple
-compWithMappingMode: (%Form,%Mode,%List) -> %List
-compFormMatch: (%Modemap,%List) -> %Boolean
+compWithMappingMode: (%Form,%Mode,%Env) -> %Maybe %Triple
+compFormMatch: (%Modemap,%List %Mode) -> %Boolean
 compFormWithModemap: (%Form,%Mode,%Env,%Modemap) -> %Maybe %Triple
-compToApply: (%Form,%List,%Mode,%Env) -> %Maybe %Triple
-compApplication: (%Form,%List,%Mode,%Triple) -> %Maybe %Triple
+compToApply: (%Form,%List %Form,%Mode,%Env) -> %Maybe %Triple
+compApplication: (%Form,%List %Form,%Mode,%Triple) -> %Maybe %Triple
 
-primitiveType: %Thing -> %Mode
+primitiveType: %Form -> %Mode
 modeEqual: (%Form,%Form) -> %Boolean
 hasUniqueCaseView: (%Form,%Mode,%Env) -> %Boolean
 convertOrCroak: (%Triple,%Mode) -> %Maybe %Triple
-getFormModemaps: (%Form,%Env) -> %List
-reshapeArgumentList: (%Form,%Signature) -> %Form
-applyMapping: (%Form,%Mode,%Env,%List) -> %Maybe %Triple
+getFormModemaps: (%Form,%Env) -> %List %Modemap
+reshapeArgumentList: (%Form,%Sig) -> %Form
+applyMapping: (%Form,%Mode,%Env,%List %Mode) -> %Maybe %Triple
 
 
 ++ A list of routines for diagnostic reports.  These functions, in an
@@ -208,7 +208,7 @@ compTypeOf(x:=[op,:argl],m,e) ==
 ++ We just determined that `op' is called with argument list `args', where
 ++  `op' is either a local capsule function, or an external function 
 ++ with a local signature-import declaration.  Emit insn for the call.
-emitLocalCallInsn: (%Symbol,%List,%Env) -> %Code
+emitLocalCallInsn: (%Symbol,%List %Code,%Env) -> %Code
 emitLocalCallInsn(op,args,e) ==
   op' :=          -- Find out the linkage name for `op'.
     get(op,"%Link",e) or encodeLocalFunctionName op
@@ -382,7 +382,7 @@ compExpression(x,m,e) ==
 
 ++ Subroutine of compAtom.
 ++ Elaborate use of an overloaded constant.
-compAtomWithModemap: (%Symbol,%Mode,%Env,%List) -> %Maybe %Triple
+compAtomWithModemap: (%Symbol,%Mode,%Env,%List %Modemap) -> %Maybe %Triple
 compAtomWithModemap(x,m,e,mmList) ==
   -- 1. Get out of here f `x' cannot possibly be a constant.
   mmList := [mm for mm in mmList | mm.mmImplementation is ['CONST,:.]]
@@ -772,8 +772,8 @@ compCons1(["CONS",x,y],m,e) ==
 
 --% SETQ
 
-compSetq: (%List,%Thing,%List) -> %List
-compSetq1: (%Form,%Thing,%Mode,%List) -> %List
+compSetq: (%Instantiation,%Mode,%Env) -> %Maybe %Triple
+compSetq1: (%Form,%Form,%Mode,%Env) -> %Maybe %Triple
 
 compSetq(["%LET",form,val],m,E) == 
   compSetq1(form,val,m,E)
@@ -901,7 +901,7 @@ setqMultipleExplicit(nameList,valList,m,e) ==
 ++ ??? based on the meta operator, e.g. (DEF ...) would be a
 ++ DefinitionAst, etc.  That however requires that we have a full
 ++ fledged AST algebra -- which we don't have yet in mainstream.
-compileQuasiquote: (%List,%Thing,%List) -> %List
+compileQuasiquote: (%Instantiation,%Mode,%Env) -> %Maybe %Triple
 compileQuasiquote(["[||]",:form],m,e) ==
   null form => nil
   coerce([["QUOTE", :form],$Syntax,e], m)
@@ -1012,8 +1012,8 @@ compMacro(form,m,e) ==
 --% SEQ
 
 compSeq: (%Form,%Mode,%Env) -> %Maybe %Triple
-compSeq1: (%Form,%List,%Env) -> %Maybe %Triple
-compSeqItem: (%Thing,%Thing,%List) -> %List
+compSeq1: (%Form,%List %Thing,%Env) -> %Maybe %Triple
+compSeqItem: (%Form,%Mode,%Env) -> %Maybe %Triple
 
 compSeq(["SEQ",:l],m,e) == 
   compSeq1(l,[m,:$exitModeStack],e)
@@ -1231,7 +1231,7 @@ compHasFormat (pred is ["has",olda,b]) ==
 --% IF
 
 compIf: (%Form,%Mode,%Env) -> %Maybe %Triple
-compPredicate: (%Form,%Env) -> %List
+compPredicate: (%Form,%Env) -> %Code
 compFromIf: (%Form,%Mode,%Env) -> %Maybe %Triple
 
 compIf(["IF",a,b,c],m,E) ==
@@ -1935,7 +1935,7 @@ compMapCond'(cexpr,dc) ==
   stackMessage('"not known that %1pb has %2pb",[dc,cexpr])
   false
 
-compMapCond: (%Mode,%List) -> %Code
+compMapCond: (%Mode,%List %Code) -> %Code
 compMapCond(dc,[cexpr,fnexpr]) ==
   compMapCond'(cexpr,dc) => fnexpr
   stackMessage('"not known that %1pb has %2pb",[dc,cexpr])
diff --git a/src/interp/database.boot b/src/interp/database.boot
index 487f85e7..05a3e845 100644
--- a/src/interp/database.boot
+++ b/src/interp/database.boot
@@ -57,109 +57,109 @@ pathToDatabase name ==
 
 --%
 
-getConstructorAbbreviationFromDB: %Symbol -> %Symbol
+getConstructorAbbreviationFromDB: %Constructor -> %Symbol
 getConstructorAbbreviationFromDB ctor ==
   GETDATABASE(ctor,"ABBREVIATION")
 
-getConstructorCategoryFromDB: %Symbol -> %Form
+getConstructorCategoryFromDB: %Constructor -> %Form
 getConstructorCategoryFromDB ctor ==
   GETDATABASE(ctor,"CONSTRUCTORCATEGORY")
 
-getConstructorKindFromDB: %Symbol -> %Maybe %ConstructorKind
+getConstructorKindFromDB: %Constructor -> %Maybe %ConstructorKind
 getConstructorKindFromDB ctor ==
   GETDATABASE(ctor,"CONSTRUCTORKIND")
 
-getConstructorAncestorsFromDB: %Symbol -> %List
+getConstructorAncestorsFromDB: %Constructor -> %List %Constructor
 getConstructorAncestorsFromDB ctor ==
   GETDATABASE(ctor,"ANCESTORS")
 
 ++ return the modemap of the constructor or the instantiation
 ++ of the constructor `form'. 
-getConstructorModemapFromDB: %Symbol -> %Mode
+getConstructorModemapFromDB: %Constructor -> %Mode
 getConstructorModemapFromDB form ==
   GETDATABASE(opOf form, 'CONSTRUCTORMODEMAP)
  
-getConstructorFormFromDB: %Symbol -> %Form
+getConstructorFormFromDB: %Constructor -> %Form
 getConstructorFormFromDB ctor ==
   GETDATABASE(ctor,"CONSTRUCTORFORM")
 
-getConstructorSourceFileFromDB: %Symbol -> %Maybe %String
+getConstructorSourceFileFromDB: %Constructor -> %Maybe %String
 getConstructorSourceFileFromDB ctor ==
   GETDATABASE(ctor,"SOURCEFILE")
 
-getConstructorModuleFromDB: %Symbol -> %Maybe %String
+getConstructorModuleFromDB: %Constructor -> %Maybe %String
 getConstructorModuleFromDB ctor ==
   GETDATABASE(ctor,"OBJECT")
 
-getConstructorDocumentationFromDB: %Symbol -> %List
+getConstructorDocumentationFromDB: %Constructor -> %List %Form
 getConstructorDocumentationFromDB ctor ==
   GETDATABASE(ctor,"DOCUMENTATION")
 
-getConstructorOperationsFromDB: %Symbol -> %List
+getConstructorOperationsFromDB: %Constructor -> %List %List %Form
 getConstructorOperationsFromDB ctor ==
   GETDATABASE(ctor,"OPERATIONALIST")
 
-getConstructorFullNameFromDB: %Symbol -> %Symbol
+getConstructorFullNameFromDB: %Symbol -> %Constructor
 getConstructorFullNameFromDB ctor ==
   GETDATABASE(ctor,"CONSTRUCTOR")
 
-getConstructorArgsFromDB: %Symbol -> %List
+getConstructorArgsFromDB: %Constructor -> %List %Symbol
 getConstructorArgsFromDB ctor ==
   GETDATABASE(ctor,"CONSTRUCTORARGS")
 
 ++ returns a list of Boolean values indicating whether the 
 ++ parameter type at the corresponding position is a category.
-getDualSignatureFromDB: %Symbol -> %Form
+getDualSignatureFromDB: %Constructor -> %Form
 getDualSignatureFromDB ctor ==
   GETDATABASE(ctor,"COSIG")
 
-getConstructorPredicatesFromDB: %Symbol -> %Thing
+getConstructorPredicatesFromDB: %Constructor -> %Thing
 getConstructorPredicatesFromDB ctor ==
   GETDATABASE(ctor,"PREDICATES")
 
-getConstructorParentsFromDB: %Symbol -> %List
+getConstructorParentsFromDB: %Constructor -> %List %Constructor
 getConstructorParentsFromDB ctor ==
   GETDATABASE(ctor,"PARENTS")
 
-getSuperDomainFromDB: %Symbol -> %Form
+getSuperDomainFromDB: %Constructor -> %Form
 getSuperDomainFromDB ctor ==
   GETDATABASE(ctor,"SUPERDOMAIN")
 
-getConstructorAttributesFromDB: %Symbol -> %Form
+getConstructorAttributesFromDB: %Constructor -> %Form
 getConstructorAttributesFromDB ctor ==
   GETDATABASE(ctor,"ATTRIBUTES")
 
-niladicConstructorFromDB: %Symbol -> %Boolean
+niladicConstructorFromDB: %Constructor -> %Boolean
 niladicConstructorFromDB ctor ==
   GETDATABASE(ctor,"NILADIC")
 
-asharpConstructorFromDB: %Symbol -> %Maybe %Symbol
+asharpConstructorFromDB: %Constructor -> %Maybe %Symbol
 asharpConstructorFromDB ctor ==
   GETDATABASE(ctor,"ASHARP?")
 
-constructorHasCategoryFromDB: %Pair -> %Thing
+constructorHasCategoryFromDB: %Pair(%Thing,%Thing) -> %List %Code
 constructorHasCategoryFromDB p ==
   GETDATABASE(p,"HASCATEGORY")
 
-getConstructorDefaultFromDB: %Symbol -> %Maybe %Symbol
+getConstructorDefaultFromDB: %Constructor -> %Maybe %Symbol
 getConstructorDefaultFromDB ctor ==
   GETDATABASE(ctor,"DEFAULTDOMAIN")
 
-getOperationFromDB: %Symbol -> %List
+getOperationFromDB: %Symbol -> %List %Sig
 getOperationFromDB op ==
   GETDATABASE(op,"OPERATION")
 
-getOperationModemapsFromDB: %Symbol -> %List
+getOperationModemapsFromDB: %Symbol -> %List %Modemap
 getOperationModemapsFromDB op ==
   GETDATABASE(op,"MODEMAPS")
 
 
-getConstructorArity: %Symbol -> %Short
+getConstructorArity: %Constructor -> %Short
 getConstructorArity ctor ==
   sig := getConstructorSignature ctor => #rest sig
   -1
 
-getConstructorKind: %Symbol -> %Maybe %ConstructorKind
+getConstructorKind: %Constructor -> %Maybe %ConstructorKind
 getConstructorKind ctor ==
   kind := getConstructorKindFromDB ctor =>
     kind = "domain" and isDefaultPackageName ctor => "package"
@@ -785,12 +785,12 @@ displayHiddenConstructors() ==
 
 ++ Return the list of modemaps exported by the category object `c'.
 ++ The format of modemap is as found in category objects.
-getCategoryExports: %Shell -> %List
+getCategoryExports: %Shell -> %List %Modemap
 getCategoryExports c == c.1
 
 ++ Return the list of category attribute info for the category object `c'.
 ++ A category attribute info is pair of attribute-predicate.
-getCategoryAttributes: %Shell -> %List
+getCategoryAttributes: %Shell -> %List %Form
 getCategoryAttributes c == c.2
 
 
@@ -800,7 +800,7 @@ getCategoryParents c == c.4.1
 
 
 --%
-squeezeAll: %List -> %List
+squeezeAll: %List %Code -> %List %Code
 squeezeAll x ==
   [SQUEEZE t for t in x]
 
diff --git a/src/interp/define.boot b/src/interp/define.boot
index acca5b76..9b1cb4ed 100644
--- a/src/interp/define.boot
+++ b/src/interp/define.boot
@@ -109,8 +109,8 @@ $subdomain := false
 
 --%
 
-compDefineAddSignature: (%Form,%Signature,%Env) -> %Env
-DomainSubstitutionFunction: (%List,%Form) -> %Form 
+compDefineAddSignature: (%Form,%Sig,%Env) -> %Env
+DomainSubstitutionFunction: (%List %Symbol,%Form) -> %Form 
 
 
 --%
@@ -473,7 +473,7 @@ compDefine(form,m,e) ==
 ++     per: Rep -> %
 ++     rep: % -> Rep
 ++ as local inline functions.
-checkRepresentation: (%Form,%List,%Env) -> %Env
+checkRepresentation: (%Form,%List %Form,%Env) -> %Env
 checkRepresentation(addForm,body,env) ==
   domainRep := nil
   hasAssignRep := false        -- assume code does not assign to Rep.
@@ -853,7 +853,7 @@ compMakeCategoryObject(c,$e) ==
   u:= mkEvalableCategoryForm c => [eval u,$Category,$e]
   nil
 
-predicatesFromAttributes: %List -> %List
+predicatesFromAttributes: %List %Form -> %List %Form
 predicatesFromAttributes attrList ==
   removeDuplicates [second x for x in attrList]
 
@@ -1155,7 +1155,7 @@ genDomainView(viewName,originalName,c,viewSelector) ==
           $getDomainCode:= [cd,:$getDomainCode]
   viewName
 
-genDomainViewList: (%Symbol,%List) -> %List 
+genDomainViewList: (%Symbol,%List %Form) -> %List %Code
 genDomainViewList(id,catlist) ==
   [genDomainView(id,id,cat,"getDomainView") 
      for cat in catlist | isCategoryForm(cat,$EmptyEnvironment)]
@@ -1928,7 +1928,7 @@ mustInstantiate D ==
   D is [fn,:.] and 
     not (symbolMember?(fn,$DummyFunctorNames) or GET(fn,"makeFunctionList"))
 
-wrapDomainSub: (%List, %Form) -> %Form 
+wrapDomainSub: (%List %Form, %Form) -> %Form 
 wrapDomainSub(parameters,x) ==
    ["DomainSubstitutionMacro",parameters,x]
  
diff --git a/src/interp/g-util.boot b/src/interp/g-util.boot
index 1880e41e..6f04fea8 100644
--- a/src/interp/g-util.boot
+++ b/src/interp/g-util.boot
@@ -40,8 +40,8 @@ namespace BOOT
 module g_-util where
   atomic?: %Thing -> %Boolean
   getTypeOfSyntax: %Form -> %Mode
-  pairList: (%List,%List) -> %List
-  mkList: %List -> %List
+  pairList: (%List %Form,%List %Form) -> %List %Pair(%Form.%Form)
+  mkList: %List %Form -> %Form
   isSubDomain: (%Mode,%Mode) -> %Form
   usedSymbol?: (%Symbol,%Code) -> %Boolean
   isDefaultPackageName: %Symbol -> %Boolean
@@ -212,9 +212,9 @@ ScanOrPairVec(f, ob) ==
 
 
 ++ Query properties for an entity in a given environment.
-get: (%Thing,%Symbol,%List) -> %Thing
-get0: (%Thing,%Symbol,%List) -> %Thing
-get1: (%Thing,%Symbol,%List) -> %Thing
+get: (%Thing,%Symbol,%Env) -> %Thing
+get0: (%Thing,%Symbol,%Env) -> %Thing
+get1: (%Thing,%Symbol,%Env) -> %Thing
 get2: (%Thing,%Symbol) -> %Thing
 
 get(x,prop,e) ==
@@ -244,13 +244,13 @@ get2(x,prop) ==
 
 ++ Update properties of an entity in an environment.
 put: (%Thing,%Symbol,%Thing,%Env) -> %Env
-addBinding: (%Thing,%List,%Env) -> %Env
-addBindingInteractive: (%Thing, %List, %Env) -> %Env
-augProplistOf: (%Thing,%Symbol,%Thing,%Env) -> %List
-augProplist: (%List,%Symbol,%Thing) -> %List
-augProplistInteractive: (%List,%Symbol,%Thing) -> %List
+addBinding: (%Thing,%List %Thing,%Env) -> %Env
+addBindingInteractive: (%Thing, %List %Thing, %Env) -> %Env
+augProplistOf: (%Thing,%Symbol,%Thing,%Env) -> %List %Thing
+augProplist: (%List %Thing,%Symbol,%Thing) -> %List %Thing
+augProplistInteractive: (%List %Thing,%Symbol,%Thing) -> %List %Thing
 putIntSymTab: (%Thing,%Symbol,%Form,%Env) -> %Env
-addIntSymTabBinding: (%Thing,%List,%Env) -> %Env
+addIntSymTabBinding: (%Thing,%List %Thing,%Env) -> %Env
 
 put(x,prop,val,e) ==
   $InteractiveMode and not sameObject?(e,$CategoryFrame) =>
@@ -672,10 +672,10 @@ opOf x ==
   cons? x => x.op
   x
 
-getProplist: (%Thing,%Env) -> %List
-search: (%Thing,%Env) -> %List
-searchCurrentEnv: (%Thing,%List) -> %List
-searchTailEnv: (%Thing,%Env) -> %List
+getProplist: (%Thing,%Env) -> %List %Thing
+search: (%Thing,%Env) -> %List %Thing
+searchCurrentEnv: (%Thing,%List %Thing) -> %List %Thing
+searchTailEnv: (%Thing,%Env) -> %List %Thing
 
 getProplist(x,E) ==
   cons? x => getProplist(first x,E)
diff --git a/src/interp/i-analy.boot b/src/interp/i-analy.boot
index 718897ec..7a404c41 100644
--- a/src/interp/i-analy.boot
+++ b/src/interp/i-analy.boot
@@ -705,7 +705,7 @@ sayIntelligentMessageAboutOpAvailability(opName, nArgs) ==
 ++ Returns the `conceptual' type of `type', e.g., the type of type in
 ++ the abstract semantics, not necessarily the one from implementation
 ++ point of view.
-conceptualType: %Thing -> %List
+conceptualType: %Thing -> %Mode
 conceptualType type ==
   isPartialMode type => $Mode
   member(type,[$Mode,$Domain,$Category]) => $Type
diff --git a/src/interp/lisplib.boot b/src/interp/lisplib.boot
index 3fc01131..2f34523b 100644
--- a/src/interp/lisplib.boot
+++ b/src/interp/lisplib.boot
@@ -809,7 +809,7 @@ getIndexPathname: %String -> %String
 getIndexPathname dir ==
   strconc(ensureTrailingSlash dir, $IndexFilename)
 
-getAllIndexPathnames: %String -> %List
+getAllIndexPathnames: %String -> %List %Form
 getAllIndexPathnames dir ==
   -- GCL's semantics of Common Lisp's `DIRECTORY *' differs from the
   -- rest of everybody else' semantics.  Namely, GCL would return a
@@ -822,7 +822,7 @@ getAllIndexPathnames dir ==
 )endif
   
 
-getAllAldorObjectFiles: %String -> %List
+getAllAldorObjectFiles: %String -> %List %Form
 getAllAldorObjectFiles dir ==
   asys := DIRECTORY strconc(dir,'"*.asy")
   asos := DIRECTORY strconc(dir,'"*.ao")
diff --git a/src/interp/modemap.boot b/src/interp/modemap.boot
index 75662d27..5197dfae 100644
--- a/src/interp/modemap.boot
+++ b/src/interp/modemap.boot
@@ -505,9 +505,9 @@ knownInfo pred ==
   pred is ["or",:l] => or/[knownInfo u for u in l]
   pred is ["and",:l] => and/[knownInfo u for u in l]
   pred is ["ATTRIBUTE",name,attr] =>
-    v:= compForMode(name,$EmptyMode,$e) or return
+    v := compForMode(name,$EmptyMode,$e) or return
           stackAndThrow('"can't find category of %1pb",[name])
-    [vv,.,.]:= compMakeCategoryObject(second v,$e) or return
+    [vv,.,.] := compMakeCategoryObject(v.mode,$e) or return
                  stackAndThrow('"can't make category of %1pb",[name])
     listMember?(attr,vv.2) => true
     x := assoc(attr,vv.2) => knownInfo second x
@@ -517,7 +517,7 @@ knownInfo pred ==
     cat is ["ATTRIBUTE",:a] => knownInfo ["ATTRIBUTE",name,:a]
     cat is ["SIGNATURE",:a] => knownInfo ["SIGNATURE",name,:a]
     -- unnamed category expressions imply structural checks.
-    cat is ["Join",:.] => and/[knownInfo ["has",name,c] for c in rest cat]
+    cat is ["Join",:.] => and/[knownInfo ["has",name,c] for c in cat.args]
     cat is ["CATEGORY",.,:atts] =>
       and/[knownInfo hasToInfo ["has",name,att] for att in atts]
     name is ['Union,:.] => false
@@ -563,8 +563,12 @@ actOnInfo(u,$e) ==
   u is ["ATTRIBUTE",name,att] =>
     [vval,vmode,.]:= GetValue name
     compilerMessage('"augmenting %1: %2p", [name,["ATTRIBUTE",att]])
-    key:= if CONTAINED("$",vmode) then "domain" else name
-    cat:= ["CATEGORY",key,["ATTRIBUTE",att]]
+    key :=
+      -- FIXME: there should be a better to tell whether name
+      --        designates a domain, as opposed to a package
+      CONTAINED("$",vmode) => 'domain
+      'package
+    cat := ["CATEGORY",key,["ATTRIBUTE",att]]
     $e:= put(name,"value",[vval,mkJoin(cat,vmode),nil],$e)
       --there is nowhere %else that this sort of thing exists
   u is ["SIGNATURE",name,operator,modemap,:q] =>
@@ -580,7 +584,11 @@ actOnInfo(u,$e) ==
     [vval,vmode,.]:= GetValue name
     compilerMessage('"augmenting %1: %2p", 
        [name,["SIGNATURE",operator,modemap,:q]])
-    key:= if CONTAINED("$",vmode) then "domain" else name
+    key :=
+      -- FIXME: there should be a better to tell whether name
+      --        designates a domain, as opposed to a package
+      CONTAINED("$",vmode) => 'domain
+      'package
     cat:= ["CATEGORY",key,["SIGNATURE",operator,modemap,:q]]
     $e:= put(name,"value",[vval,mkJoin(cat,vmode),nil],$e)
   u is ["has",name,cat] =>
diff --git a/src/interp/parse.boot b/src/interp/parse.boot
index 607a646a..4cdbeb82 100644
--- a/src/interp/parse.boot
+++ b/src/interp/parse.boot
@@ -87,7 +87,7 @@ parseTypeList l ==
   l = nil => nil
   [parseType first l, :parseTypeList rest l]
 
-parseTranList: %List -> %List
+parseTranList: %List %Form -> %List %Form
 parseTranList l ==
   atom l => parseTran l
   [parseTran first l,:parseTranList rest l]
@@ -358,13 +358,13 @@ makeSimplePredicateOrNil p ==
   wrapSEQExit [["%LET",g:= gensym(),p],g]
  
 
-parseWhere: %List -> %Form
+parseWhere: %List %Form -> %Form
 parseWhere t == 
   t isnt ["where",:l] => systemErrorHere ["parseWhere",t]
   ["where",:parseTranList l]
  
  
-parseSeq: %List -> %Form
+parseSeq: %List %Form -> %Form
 parseSeq t ==
   t isnt ["SEQ",:l] => systemErrorHere ["parseSeq",t]
   l isnt [:.,["exit",:.]] =>
@@ -372,7 +372,7 @@ parseSeq t ==
   transSeq parseTranList l
  
 
-transSeq: %List -> %Form
+transSeq: %List %Form -> %Form
 transSeq l ==
   l = nil => nil
   l is [x] => decExitLevel x
@@ -412,7 +412,7 @@ transCategoryItem x ==
   [x]
  
 
-superSub: (%Symbol, %List) -> %Form
+superSub: (%Symbol, %List %Form ) -> %Form
 superSub(name,x) ==
   for u in x repeat y:= [:y,:u]
   code:=
@@ -420,22 +420,22 @@ superSub(name,x) ==
     strconc('"_(",scriptTranRow first x,scriptTran rest x,'"_)")
   [INTERNL(symbolName name,"$",code),:y]
  
-scriptTran: %List -> %String
+scriptTran: %List %Form -> %String
 scriptTran x ==
   x = nil => '""
   strconc('";",scriptTranRow first x,scriptTran rest x)
  
-scriptTranRow: %List -> %String
+scriptTranRow: %List %Form -> %String
 scriptTranRow x ==
   x = nil => '""
   strconc($quadSymbol,scriptTranRow1 rest x)
 
-scriptTranRow1: %List -> %String 
+scriptTranRow1: %List %Form -> %String 
 scriptTranRow1 x ==
   x = nil => '""
   strconc('",",$quadSymbol,scriptTranRow1 rest x)
  
-parseVCONS: %List -> %Form
+parseVCONS: %List %Form -> %Form
 parseVCONS l == 
   ["VECTOR",:parseTranList rest l]
 
diff --git a/src/interp/posit.boot b/src/interp/posit.boot
index 114916ee..82d1f09d 100644
--- a/src/interp/posit.boot
+++ b/src/interp/posit.boot
@@ -35,10 +35,10 @@ import sys_-macros
 import astr
 namespace BOOT
 module posit where
-  %Position <=> %List
-  tokType: %List -> %Symbol
-  tokPart: %List -> %Thing
-  tokPosn: %List -> %Position
+  %Position <=> %List %Form
+  tokType: %List %Form -> %Symbol
+  tokPart: %List %Form -> %Thing
+  tokPosn: %List %Form -> %Position
 
 $nopos ==
   ['noposition]
diff --git a/src/interp/postpar.boot b/src/interp/postpar.boot
index 602732d9..ba65872b 100644
--- a/src/interp/postpar.boot
+++ b/src/interp/postpar.boot
@@ -39,11 +39,11 @@ module postpar
 
 ++ The type of parse trees.
 %ParseTree <=> 
-  %Number or %Symbol or %String or %Pair
+  %Number or %Symbol or %String or %Pair(%Thing,%Thing)
 
 ++ The result of processing a parse tree.
 %ParseForm <=>
-  %Number or %Symbol or %String or %Pair
+  %Number or %Symbol or %String or %Pair(%Thing,%Thing)
 
 $postStack := []
 
@@ -92,7 +92,7 @@ postTran x ==
   op ~= (y:= postOp op) => [y,:postTranList rest x]
   postForm x
 
-postTranList: %List -> %List
+postTranList: %List %ParseTree -> %List %ParseForm
 postTranList x == 
   [postTran y for y in x]
 
@@ -187,7 +187,7 @@ postBlock t ==
   t isnt ["%Block",:l,x] => systemErrorHere ["postBlock",t]
   ["SEQ",:postBlockItemList l,["exit",postTran x]]
 
-postBlockItemList: %List -> %List
+postBlockItemList: %List %ParseTree -> %List %ParseTree
 postBlockItemList l == 
   [postBlockItem x for x in l]
 
@@ -241,7 +241,7 @@ postDef t ==
   specialCaseForm := [nil for x in form]
   ["DEF",newLhs,typeList,specialCaseForm,postTran rhs]
 
-postDefArgs: %List -> %List
+postDefArgs: %List %ParseTree -> %List %ParseForm
 postDefArgs argl ==
   null argl => argl
   argl is [[":",a],:b] =>
@@ -316,7 +316,7 @@ postQuote [.,a] ==
   ["QUOTE",a]
 
 
-postScriptsForm: (%ParseTree,%List) -> %ParseForm
+postScriptsForm: (%ParseTree,%List %ParseTree) -> %ParseForm
 postScriptsForm(t,argl) ==
   t isnt ["Scripts",op,a] => systemErrorHere ["postScriptsForm",t]
   [getScriptName(op,a,#argl),:postTranScripts a,:argl]
@@ -416,7 +416,7 @@ postTupleCollect t ==
   t isnt [constructOp,:m,x] => systemErrorHere ["postTupleCollect",t]
   postCollect [constructOp,:m,["construct",x]]
 
-postIteratorList: %List -> %List
+postIteratorList: %List %ParseTree -> %List %ParseForm
 postIteratorList x ==
   x is [p,:l] =>
     (p:= postTran p) is ["IN",y,u] =>
diff --git a/src/interp/serror.boot b/src/interp/serror.boot
index 59318cbd..9dcf1c3a 100644
--- a/src/interp/serror.boot
+++ b/src/interp/serror.boot
@@ -37,20 +37,20 @@ namespace BOOT
 --% Functions to handle specific errors (mostly syntax)
  
 
-syGeneralErrorHere: () -> %Thing
+syGeneralErrorHere: () -> %Void
 syGeneralErrorHere() ==
    sySpecificErrorHere('S2CY0002, [])
  
-sySpecificErrorHere: (%Symbol,%List) -> %Thing
+sySpecificErrorHere: (%Symbol,%List %Form) -> %Void
 sySpecificErrorHere(key,args) ==
    sySpecificErrorAtToken($stok, key, args)
  
-sySpecificErrorAtToken: (%Thing,%Symbol,%List) -> %Thing
+sySpecificErrorAtToken: (%Thing,%Symbol,%List %Form) -> %Void
 sySpecificErrorAtToken(tok,key,args) ==
    pos := tokPosn tok
    ncSoftError(pos, key, args)
  
-syIgnoredFromTo: (%List,%List) -> %Thing
+syIgnoredFromTo: (%List %Form,%List %Form) -> %Void
 syIgnoredFromTo(pos1, pos2) ==
   if pfGlobalLinePosn pos1 = pfGlobalLinePosn pos2 then
       ncSoftError(FromTo(pos1,pos2), 'S2CY0005, [])
@@ -58,7 +58,7 @@ syIgnoredFromTo(pos1, pos2) ==
       ncSoftError(From pos1, 'S2CY0003, [])
       ncSoftError(To   pos2, 'S2CY0004, [])
  
-npTrapForm: %Thing -> %Thing
+npTrapForm: %Thing -> %Void
 npTrapForm(x)==
    a:=pfSourceStok x
    a='NoToken =>
diff --git a/src/interp/sys-utility.boot b/src/interp/sys-utility.boot
index 6d9bf52c..349304f8 100644
--- a/src/interp/sys-utility.boot
+++ b/src/interp/sys-utility.boot
@@ -82,15 +82,15 @@ getVMType d ==
     IntegerMod => "%Integer"
     DoubleFloat => "%DoubleFloat"
     String => "%String"
-    List => "%List"
+    List => ["%List",getVMType second d']
     Vector => ["%Vector",getVMType second d']
     PrimitiveArray => ["%SimpleArray", getVMType second d']
-    Pair => "%Pair"
-    Union => "%Pair"
+    Pair => ["%Pair",getVMType second d',getVMType third d']
+    Union => ["%Pair",'%Thing,'%Thing]
     Record =>
       #rest d' > 2 => "%Shell"
-      "%Pair"
-    IndexedList => "%List"
+      ["%Pair",'%Thing,'%Thing]
+    IndexedList => ["%List", getVMType second d']
     Int8 => ["SIGNED-BYTE", 8]
     Int16 => ["SIGNED-BYTE", 16]
     Int32 => ["SIGNED-BYTE", 32]
@@ -117,7 +117,6 @@ functionp f ==
   function? f
 
 ++ remove `item' from `sequence'.
-delete: (%Thing,%Sequence) -> %Sequence
 delete(item,sequence) ==
   symbol? item => 
     REMOVE(item,sequence,KEYWORD::TEST,function sameObject?)
@@ -154,7 +153,7 @@ ASSOCRIGHT x ==
 
 ++ Put the association list pair `(x . y)' into `l', erasing any 
 ++ previous association for `x'.
-ADDASSOC: (%Thing,%Thing,%List) -> %List
+ADDASSOC: (%Thing,%Thing,%Alist(%Thing,%Thing)) -> %Alist(%Thing,%Thing)
 ADDASSOC(x,y,l) ==
   atom l => [[x,:y],:l]
   x = first first l => [[x,:y],:rest l]
@@ -162,7 +161,7 @@ ADDASSOC(x,y,l) ==
 
 
 ++ Remove any assocation pair `(u . x)' from list `v'.
-DELLASOS: (%Thing,%List) -> %List
+DELLASOS: (%Thing,%Alist(%Thing,%Thing)) -> %Alist(%Thing,%Thing)
 DELLASOS(u,v) ==
   atom v => nil
   u = first first v => rest v
@@ -171,14 +170,14 @@ DELLASOS(u,v) ==
 
 ++ Return the datum associated with key `x' in association list `y'.
 -- ??? Should not this be named `alistValue'?
-LASSOC: (%Thing,%List) -> %Thing
+LASSOC: (%Thing,%Alist(%Thing,%Thing)) -> %Thing
 LASSOC(x,y) ==
   atom y => nil
   x = first first y => rest first y
   LASSOC(x,rest y)
 
 ++ Return the key associated with datum `x' in association list `y'.
-rassoc: (%Thing,%List) -> %Thing
+rassoc: (%Thing,%Alist(%Thing,%Thing)) -> %Thing
 rassoc(x,y) ==
   atom y => nil
   x = rest first y => first first y
diff --git a/src/interp/types.boot b/src/interp/types.boot
index 6022a5cb..915279ee 100644
--- a/src/interp/types.boot
+++ b/src/interp/types.boot
@@ -34,117 +34,14 @@
 import boot_-pkg
 namespace BOOT
 
---% Basic types used throughout Boot codes.
-
-++ Type of nothing.  Bottom of the abstract machine type lattice.
-++ Since Lisp functions always returns something, we cannot
-++ use the `nil' type specifier (the ideal answer).  Second
-++ best possibility is to have Void-returning functions
-++ systematically return `nil'.  However, until the Lisp
-++ backend is fixed, we will use the interpretation that a 
-++ Void-returning function may return anything, but nobody cares.
-++ Hence, the choice below which contradicts the very first line
-++ of this description.
-%Void <=> 
-  true
-
-++ Type of truth values.
-%Boolean <=> 
-  BOOLEAN
-
-++ Type of a bit value.
-%Bit <=>
-  BIT
-
-++ Type of 8-bit sized unsigned integer values.
-%Byte <=>
-  UNSIGNED_-BYTE 8
-
-++ Type of characters -- no distinction yet.
-%Char <=>
-  CHARACTER
-
-++ Type of fixnums.
-%Short <=> 
-  FIXNUM
-
-++ Type of unlimited precision integers.
-%Bignum <=> 
-  BIGNUM
-
-%Integer <=>
-  INTEGER
-
-%IntegerSection n <=>
-  INTEGER n
-
-++ Type of single precision floating point numbers.  Most of the
-++ time, this is a 32-bit datatype on IEEE-754 host.
-%SingleFloat <=>
-)if %hasFeature KEYWORD::GCL
-  SHORT_-FLOAT
-)else
-  SINGLE_-FLOAT
-)endif
-
-++ Type of double precision floating point numbers.  Most of the time,
-++ this is a 64-bit sized datatype on IEEE-756 host.
-%DoubleFloat <=>
-  DOUBLE_-FLOAT
-
-++ General type for numbers.
-%Number <=> 
-  NUMBER
-
-++ Type of identifiers.  Ideally, we want actually want to exclude
-++ Lisp oddities such as NIL and T.
-%Symbol <=> 
-  SYMBOL
-
-++ The type of literal strings
-%String <=> 
-  STRING
-
-++ Anything that is not a cons cell.
-%Atom <=> atom
-
-++ nil or a cons cell.  Ideally, this should be parameterized, but
-++ we cannot afford that luxury with Lisp.
-%List <=> 
-  LIST
-
-++ The type of a linear homogeneous non-extensible array.
-%SimpleArray a <=> 
-  SIMPLE_-ARRAY a
-
-%Vector a <=> VECTOR a
-
-%BitVector <=> %Vector %Bit
-
-%Thing <=> true
-
-%Sequence <=> SEQUENCE
-
-%Pair <=> CONS
+--% Data structures for the compiler
 
-%Maybe a <=> null or a
+%Alist(s,t) <=> %List %Pair(s,t)               -- association list
 
---% Data structures for the compiler
 %Constructor <=> %Symbol                       -- constructor
-%Form <=> %Number or %Symbol or %String or %Pair -- input syntax form
 %Instantiation <=> [%Constructor,:%Form]       -- constructor instance
-%Env <=> %List                                 -- compiling env
-%Mode <=> %Symbol or %String or %List          -- type of forms
-%Code <=> %Form or %Char                       -- generated code
-%Triple <=>                                    -- form + type + env
-  [%Code,:[%Mode,:[%Env,:null]]]
-
-%Signature                      -- signature
-  <=> %Symbol or %Pair
 
-%Modemap <=> %List                             -- modemap
+%Modemap <=> %List(%Form)                      -- modemap
 
 %ConstructorKind <=>                           -- kind of ctor instances
   MEMBER(category,domain,package)
-
-%Shell <=> SIMPLE_-VECTOR                      -- constructor instantiation