Import to github.

12 files changed, 1517 insertions, 0 deletions

diff --git a/type/README b/type/README
new file mode 100644
index 0000000..dc40c55
--- /dev/null
+++ b/type/README
@@ -0,0 +1 @@
+This directory contains the type inference phase.
diff --git a/type/default.scm b/type/default.scm
new file mode 100644
index 0000000..529f4f8
--- /dev/null
+++ b/type/default.scm
@@ -0,0 +1,47 @@
+;;; This handles the default rule.
+
+(define (maybe-default-ambiguous-tyvar type def module)
+  (let ((classes (ntyvar-context type)))
+   (and (not (null? classes)) ; this happens only during cleanup after an error
+    (let ((non-standard? '#f)
+	  (numeric? '#f))
+      (dolist (class classes)
+	(cond ((eq? (class-kind class) 'numeric)
+	       (setf numeric? '#t))
+	      ((not (eq? (class-kind class) 'standard))
+	       (setf non-standard? '#t))))
+      (cond ((or non-standard? (not numeric?))
+	     (remember-context def
+ 	       (phase-error 'Non-defaultable-ambiguous-context
+"An ambiguous context, ~A, cannot be defaulted.~%Ambiguity in call to ~A~%"
+                  classes def))
+	     '#f)
+	    (else
+	     (find-default-type type classes classes
+			(tuple-2-2 (assq module *default-decls*)))))))))
+
+(define (find-default-type tyvar classes all-classes defaults)
+  (cond ((null? defaults)
+	 (phase-error 'no-default-applies
+	    "Ambiguous context: ~A~%No default applies.~%"
+	    all-classes)
+	 '#f)
+	((null? classes)
+	 (instantiate-tyvar tyvar (car defaults))
+	 '#t)
+	((type-in-class? (car defaults) (car classes))
+	 (find-default-type tyvar (cdr classes) all-classes defaults))
+	(else
+	 (find-default-type tyvar all-classes all-classes (cdr defaults)))))
+	 
+(define (type-in-class? ntype class)
+  (let* ((ntype (expand-ntype-synonym ntype))
+	 (alg (ntycon-tycon ntype))
+	 (inst (lookup-instance alg class)))
+    (if (eq? inst '#f)
+	'#f
+	(let ((res '#t))
+	  (do-contexts (c (instance-context inst)) (ty (ntycon-args ntype))
+	    (when (not (type-in-class? ty c))
+	      (setf res '#f)))
+	  res))))
diff --git a/type/dictionary.scm b/type/dictionary.scm
new file mode 100644
index 0000000..0a0260e
--- /dev/null
+++ b/type/dictionary.scm
@@ -0,0 +1,229 @@
+
+;;; type/dictionary.scm
+
+;;; This function supports dictionary conversion.  It creates lambda
+;;; variables to bind to the dictionary args needed by the context.
+;;; The actual conversion to lambda is done in the cfn.  Each tyvar in
+;;; the context has an associated mapping from class to dictionary
+;;; variable.  This mapping depends on the decl containing the placeholder
+;;; since different recursive decls share common tyvars.  The mapping is
+;;; two levels: decl -> class -> var.
+
+;;; Due to language restrictions this valdef must be a simple variable
+;;; definition.
+
+(define (dictionary-conversion/definition valdef tyvars)
+  (let* ((var (decl-var valdef))
+	 (type (var-type var))
+	 (context (gtype-context type))
+	 (dict-param-vars '()))
+    (dolist (c context)
+      (let ((tyvar (car tyvars))
+	    (dparams '()))
+       (when (not (null? c))
+	(dolist (class c)
+          (let ((var (create-temp-var
+		      (string-append "d_"
+				     (symbol->string (def-name class))))))
+	    (setf (var-force-strict? var) '#t)
+	    (push (tuple class var) dparams)
+	    (push var dict-param-vars)))
+	(push (tuple valdef dparams) (ntyvar-dict-params tyvar)))
+       (setf tyvars (cdr tyvars))))
+    (setf (valdef-dictionary-args valdef) (nreverse dict-param-vars))))
+
+;;; These routines deal with dict-var processing.
+
+;;; This discharges the tyvars associated with dictionaries.  The dict-vars
+;;; to be processed at the next level are returned.
+
+(define (process-placeholders placeholders deferred decls)
+  (if (null? placeholders)
+      deferred
+      (let ((d1 (process-placeholder (car placeholders) deferred decls)))
+	(process-placeholders (cdr placeholders) d1 decls))))
+
+;;; This processes a placeholder.  The following cases arise:
+;;;  a) the variable has already been processed (no placeholders remain) -
+;;;     ignore it.  placeholders may contain duplicates so this is likely.
+;;;  b) the type variable is from an outer type environment (in ng-list)
+;;;     and should just be passed up to the next level (added to old-placeholders)
+;;;  c) the type variable is associated with a dictionary parameter
+;;;  d) the type variable is instantiated to a type constructor
+;;;  e) the type variable is ambiguous (none of the above)
+
+(define (process-placeholder p deferred decls)
+  (let* ((tyvar (placeholder-tyvar p))
+	 (type (prune tyvar)))
+    (cond ((ntycon? type)
+	   (process-instantiated-tyvar
+	    (expand-ntype-synonym type) p deferred decls))
+	  ((non-generic? type)
+	   (cons p deferred))
+	  ((not (null? (ntyvar-dict-params type)))
+	   (if (dict-placeholder? p)
+	       (placeholder->dict-param p (ntyvar-dict-params type) decls)
+	       (placeholder->method p (ntyvar-dict-params type) decls))
+	   deferred)
+	  (else
+	   ;; Since default types are monotypes, no new vars will
+	   ;; be added to old-placeholders
+	   (when (maybe-default-ambiguous-tyvar
+		  type (placeholder-overloaded-var p)
+		  (valdef-module (car (placeholder-enclosing-decls p))))
+	      (process-placeholder p deferred decls))
+	   deferred))))
+	       
+;;; The type variable is associated with a dictionary parameter.  The only
+;;; complication here is that the class needed may not be directly available -
+;;; it may need to be obtained from the super classes of the parameter
+;;; dictionaries.
+
+(define (placeholder->dict-param p param-vars decls)
+  (let ((class (dict-placeholder-class p))
+	(edecls (dict-placeholder-enclosing-decls p)))
+    (setf (placeholder-exp p)
+	  (dict-reference-code class (locate-params param-vars edecls decls)))))
+
+(define (dict-reference-code class param-vars)
+  (let ((var (assq class param-vars)))
+    (if (not (eq? var '#f))
+	(**var/def (tuple-2-2 var))
+	(search-superclasses class param-vars))))
+
+(define (locate-params param-vars enclosing-decls decls)
+  (if (null? (cdr param-vars))
+      (tuple-2-2 (car param-vars))
+      (let ((decl (search-enclosing-decls enclosing-decls decls)))
+	(tuple-2-2 (assq decl param-vars)))))
+
+;;; This finds the first dictionary containing the needed class in its
+;;; super classes and generates a selector to get the needed dictionary.
+
+(define (search-superclasses class param-vars)
+  (let ((pclass (tuple-2-1 (car param-vars))))
+    (if (memq class (class-super* pclass))
+	(**dsel/dict pclass class (**var/def (tuple-2-2 (car param-vars))))
+	(search-superclasses class (cdr param-vars)))))
+
+(define (placeholder->method p param-vars decls)
+  (let* ((method (method-placeholder-method p))
+	 (class (method-var-class method))
+	 (edecls (placeholder-enclosing-decls p))
+	 (params (locate-params param-vars edecls decls)))
+    (setf (placeholder-exp p)
+	  (method-reference-code method class params))))
+
+(define (method-reference-code m c param-vars)
+ (let ((pclass (tuple-2-1 (car param-vars))))
+  (if (or (eq? c pclass)
+	  (memq c (class-super* pclass)))
+      (let* ((msel (assq m (class-selectors pclass)))
+	     (mvar (tuple-2-2 msel)))
+	(**app (**var/def mvar) (**var/def (tuple-2-2 (car param-vars)))))
+      (method-reference-code m c (cdr param-vars)))))
+
+;;; This is for tyvars instantiated to a tycon.  A reference to the
+;;; appropriate dictionary is generated.  This reference must be recursively
+;;; dictionary converted since dictionaries may need subdictionaries
+;;; when referenced.
+
+(define (process-instantiated-tyvar tycon p deferred decls)
+  (let* ((alg (ntycon-tycon tycon))
+	 (edecls (placeholder-enclosing-decls p))
+	 (var (placeholder-overloaded-var p))
+	 (class (if (dict-placeholder? p)
+		    (dict-placeholder-class p)
+		    (method-var-class (method-placeholder-method p))))
+	 (instance (lookup-instance alg class)))
+    (if (dict-placeholder? p)
+	(mlet (((code def1)
+		(generate-dict-ref instance tycon deferred decls edecls var)))
+	   (setf (placeholder-exp p) code)
+	   (setf deferred def1))
+	(let ((method (method-placeholder-method p)))
+	  (if (every (function null?) (instance-gcontext instance))
+	      (let ((mvar (tuple-2-2
+			   (assq method (instance-methods instance)))))
+		(setf (placeholder-exp p) (**var/def mvar)))
+	      (mlet (((code def1)
+		      (generate-dict-ref
+		         instance tycon deferred decls edecls var))
+		     (sel (tuple-2-2 (assq method (class-selectors class)))))
+		(setf (method-placeholder-exp p) (**app (**var/def sel) code))
+		(setf deferred def1)))))
+    deferred))
+
+;;; This generates a reference to a specific dictionary and binds
+;;; needed subdictionaries.  Since subdictionaries may be part of the outer
+;;; type environment new placeholders may be generated for later resolution.
+
+(define (generate-dict-ref instance type deferred decls edecls var)
+  (let* ((ctxt (instance-gcontext instance))
+	 (dict (dict-ref-code instance)))
+    (do-contexts (class ctxt) (ty (ntycon-args type))
+      (let ((ntype (prune ty)))
+	(cond
+	 ((ntycon? ntype)
+	  (mlet ((ntype (expand-ntype-synonym ntype))
+		 (alg (ntycon-tycon ntype))
+		 (instance (lookup-instance alg class))
+		 ((code dv1)
+		  (generate-dict-ref
+		    instance ntype deferred decls edecls var)))
+	      (setf dict (**app dict code))
+	      (setf deferred dv1)))
+	 ((non-generic? ntype)
+	  (let ((p (**dict-placeholder
+		    class ntype edecls var)))
+	    (setf dict (**app dict p))
+	    (push p deferred)))
+	 ((null? (ntyvar-dict-params ntype))
+	  (let ((ref-code (**dict-placeholder
+			   class ntype edecls var)))
+	     (when (maybe-default-ambiguous-tyvar
+		    ntype var (valdef-module (car edecls)))
+		(process-placeholder ref-code '() decls))
+	     (setf dict (**app dict ref-code))))
+	 (else
+	  (let ((p (locate-params (ntyvar-dict-params ntype) edecls decls)))
+	    (setf dict (**app dict (dict-reference-code class p))))))))
+    (values dict deferred)))
+
+;;; The following routines deal with recursive placeholders.  The basic
+;;; strategy is to pass the entire context as a parameter with each
+;;; recursive call (this could be optimized later to make use of an
+;;; internal entry point).  The basic complication is that the context
+;;; of each function in a letrec may be arranged differently.
+
+;;; This generates a call inside decl 'from' to the var 'to'.  Vmap is an
+;;; alist from vars to a list of vars corresponding to the gtyvars of
+;;; the decl signature.
+
+(define (recursive-call-code from to vmap)
+  (let ((exp (**var/def to))
+	(tyvars (tuple-2-2 (assq to vmap)))
+	(contexts (gtype-context (var-type to))))
+    (do-contexts (class contexts) (tyvar tyvars)
+       (setf exp (**app exp (locate-param-var tyvar class from))))
+    exp))
+
+(define (locate-param-var tyvar class decl)
+  (let ((vmap (tuple-2-2 (assq decl (ntyvar-dict-params tyvar)))))
+    (**var/def (tuple-2-2 (assq class vmap)))))
+
+;;; This is used to get the code for a specific dictionary reference.
+
+(define (dict-ref-code instance)
+  (**var/def (instance-dictionary instance)))
+
+;;; This is used to locate the correct enclosing decl.
+
+(define (search-enclosing-decls decl-list decls)
+  (cond ((null? decl-list)
+	 (error "Lost decl in search-enclosing-decls!"))
+	((memq (car decl-list) decls)
+	 (car decl-list))
+	(else
+	 (search-enclosing-decls (cdr decl-list) decls))))
+
diff --git a/type/expression-typechecking.scm b/type/expression-typechecking.scm
new file mode 100644
index 0000000..f4606d1
--- /dev/null
+++ b/type/expression-typechecking.scm
@@ -0,0 +1,364 @@
+;;; This file contains typecheckers for all expressions except vars and
+;;; declarations.
+
+;;; From valdef-structs:
+;;;   valdef, single-fun-def are in type-decls
+
+(define-type-checker guarded-rhs
+  (type-check guarded-rhs rhs rhs-type
+    (type-check guarded-rhs guard guard-type
+      (type-unify guard-type *bool-type*
+          (type-mismatch/fixed (guarded-rhs-guard object)
+	   "Guards must be of type Bool" guard-type))
+      (return-type object rhs-type))))
+
+;;; These type checkers deal with patterns.
+
+(define-type-checker as-pat
+  (type-check as-pat pattern as-type
+    (setf (var-type (var-ref-var (as-pat-var object))) as-type)
+    (return-type object as-type)))
+
+(define-type-checker irr-pat
+  (type-check irr-pat pattern pattern-type
+    (return-type object pattern-type)))
+
+(define-type-checker var-pat
+  (fresh-type var-type
+    (setf (var-type (var-ref-var (var-pat-var object))) var-type)
+    (return-type object var-type)))
+
+(define-type-checker wildcard-pat
+ (fresh-type pat-type
+    (return-type object pat-type)))
+
+;;; Constant patterns create a piece of code to actually to the
+;;; match: ((==) k), where k is the constant.  This code is placed in the
+;;; match-fn slot of the const-pat and is used by the cfn.
+
+(define-type-checker const-pat
+ (let* ((val (const-pat-value object))
+	(match-fn (**app (**var/def (core-symbol "==")) val)))
+   (setf (const-pat-match-fn object) match-fn)
+   (type-check const-pat match-fn match-type
+     (fresh-type res-type
+       (type-unify match-type (**arrow res-type *bool-type*) #f)
+       (return-type object res-type)))))
+
+(define-type-checker plus-pat
+  (let* ((kp (**int (plus-pat-k object)))
+	 (km (**int (- (plus-pat-k object))))
+	 (match-fn (**app (**var/def (core-symbol "<=")) kp))
+	 (bind-fn (**app (**var/def (core-symbol "+")) km)))
+    (setf (plus-pat-match-fn object) match-fn)
+    (setf (plus-pat-bind-fn object) bind-fn)
+    (fresh-type res-type
+      (setf (ntyvar-context res-type) (list (core-symbol "Integral")))
+      (type-check plus-pat match-fn match-type
+        (type-check plus-pat bind-fn bind-type
+          (type-check plus-pat pattern pat-type
+	    (type-unify match-type (**arrow pat-type *bool-type*) #f)
+	    (type-unify bind-type (**arrow pat-type pat-type) #f)
+	    (type-unify res-type pat-type #f)
+	    (return-type object res-type)))))))
+
+(define-type-checker pcon
+ (type-check/list pcon pats arg-types
+   (fresh-type res-type
+     (let ((con-type (instantiate-gtype (con-signature (pcon-con object)))))
+       (type-unify con-type (**arrow/l-2 arg-types res-type) #f)
+       (return-type object res-type)))))
+
+(define-type-checker list-pat
+  (if (null? (list-pat-pats object))
+      (return-type object (instantiate-gtype
+			     (algdata-signature (core-symbol "List"))))
+      (type-check/unify-list list-pat pats element-type
+	   (type-mismatch/list object
+	     "List elements have different types")
+	(return-type object (**list-of element-type)))))
+
+;;; These are in the order defined in exp-structs.scm
+
+(define-type-checker lambda
+ (with-new-tyvars
+  (fresh-monomorphic-types (length (lambda-pats object)) arg-vars
+    (type-check/list lambda pats arg-types
+     (unify-list arg-types arg-vars)
+     (type-check lambda body body-type
+      (return-type object (**arrow/l-2 arg-vars body-type)))))))
+
+(define-type-checker let
+  (type-check/decls let decls
+    (type-check let body let-type
+      (return-type object let-type))))
+
+(define-type-checker if
+  (type-check if test-exp test-type
+    (type-unify test-type *bool-type*
+        (type-mismatch/fixed object
+	 "The test in an if statement must be of type Bool"
+	 test-type))
+    (type-check if then-exp then-type
+      (type-check if else-exp else-type
+        (type-unify then-type else-type
+              (type-mismatch object
+		   "then and else clauses have different types"
+		   then-type else-type))
+	(return-type object then-type)))))
+
+(define-type-checker case
+ (with-new-tyvars
+  (let ((case-exp object))  ; needed since object is rebound later
+   (fresh-monomorphic-type arg-type
+    (type-check case exp exp-type
+      (type-unify arg-type exp-type #f) ; just to make it monomorphic
+      (fresh-type res-type
+	(dolist (object (case-alts object))
+	  (recover-type-error ;;; %%% Needs work
+	   (type-check alt pat pat-type
+	     (type-unify pat-type arg-type
+                 (type-mismatch case-exp
+		  "Case patterns type conflict."
+		  pat-type arg-type))
+	     (type-check/decls alt where-decls
+	       (type-check/unify-list alt rhs-list rhs-type
+                 (type-mismatch/list case-exp
+		     "Guarded expressions must have the same type")
+		 (type-unify rhs-type res-type
+			      (type-mismatch case-exp
+		   "Case expression alternatives must have the same type"
+		                 rhs-type res-type)))))))
+	(return-type case-exp res-type)))))))
+
+;;; Expressions with signatures are transformed into let expressions
+;;; with signatures.  
+
+;;;    exp :: type   is rewritten as
+;;;    let temp = exp
+;;;        temp :: type
+;;;     in temp
+
+(define-type-checker exp-sign
+ (type-rewrite
+  (let* ((temp-var (create-temp-var "TC"))
+	 (decl (**valdef (**var-pat/def temp-var) '() (exp-sign-exp object)))
+	 (let-exp (**let (list decl) (**var/def temp-var)))
+	 (signature (exp-sign-signature object)))
+      (setf (var-signature temp-var)
+	    (ast->gtype (signature-context signature)
+			(signature-type signature)))
+      let-exp)))
+
+;;; Rather than complicate the ast structure with a new node for dictSel
+;;; we recognize the dictSel primitive as an application and treat it
+;;; specially.
+
+(define-type-checker app
+ (if (and (var-ref? (app-fn object))
+	  (eq? (var-ref-var (app-fn object)) (core-symbol "dictSel")))
+  (type-check-dict-sel (app-arg object))
+  (type-check app fn fn-type
+    (type-check app arg arg-type
+      (fresh-type res-type
+        (fresh-type arg-type-1
+          (type-unify fn-type (**arrow arg-type-1 res-type)
+              (type-mismatch/fixed object
+		       "Attempt to call a non-function"
+		       fn-type))
+	  (type-unify arg-type-1 arg-type
+              (type-mismatch object
+		 "Argument type mismatch" arg-type-1 arg-type))
+	  (return-type object res-type)))))))
+
+;;; This is a special hack for typing dictionary selection as used in
+;;; generic tuple functions.  This extracts a dictionary from a TupleDict
+;;; object and uses is to resolve the overloading of a designated
+;;; expression.  The expresion must generate exactly one new context.
+
+(define (type-check-dict-sel arg)
+  (when (or (not (app? arg))
+	    (not (app? (app-fn arg))))
+     (dict-sel-error))
+  (let* ((exp (app-fn (app-fn arg)))
+	 (dict-var (app-arg (app-fn arg)))
+	 (i (app-arg arg))
+	 (p (dynamic *placeholders*)))
+    (mlet (((object exp-type) (dispatch-type-check exp)))
+	  ; check for exactly one new context
+      (when (or (eq? (dynamic *placeholders*) p)
+		(not (eq? (cdr (dynamic *placeholders*)) p)))
+	 (dict-sel-error))
+	(mlet ((placeholder (car (dynamic *placeholders*)))
+	       (tyvar (placeholder-tyvar placeholder))
+	       ((dict-var-ast dict-var-type) (dispatch-type-check dict-var))
+	       ((index-ast index-type) (dispatch-type-check i)))
+	   (setf (ntyvar-context tyvar) '())  ; prevent context from leaking out
+	   (setf (dynamic *placeholders*) p)
+           (type-unify dict-var-type
+			  (**ntycon (core-symbol "TupleDicts") '()) #f)
+	   (type-unify index-type *int-type* #f)
+	   (cond ((method-placeholder? placeholder)
+		  (dict-sel-error))  ; I am lazy.  This means that
+		 ; dictSel must not be passed a method
+		 (else
+		  (setf (placeholder-exp placeholder)
+			(**app (**var/def (core-symbol "dictSel"))
+			       dict-var-ast index-ast))))
+	   (return-type object exp-type)))))
+
+(define (dict-sel-error)
+  (fatal-error 'dict-sel-error "Bad dictSel usage."))
+
+(define-type-checker con-ref
+  (return-type object (instantiate-gtype (con-signature (con-ref-con object)))))
+
+(define-type-checker integer-const
+  (cond ((const-overloaded? object)
+	 (setf (const-overloaded? object) '#f)
+	 (type-rewrite (**fromInteger object)))
+	(else
+	 (return-type object *Integer-type*))))
+
+(define-type-checker float-const
+  (cond ((const-overloaded? object)
+	 (setf (const-overloaded? object) '#f)
+	 (type-rewrite (**fromRational object)))
+	(else
+	 (return-type object *Rational-type*))))
+
+(define-type-checker char-const
+  (return-type object *char-type*))
+
+(define-type-checker string-const
+  (return-type object *string-type*))
+
+(define-type-checker list-exp
+  (if (null? (list-exp-exps object))
+      (return-type object (instantiate-gtype
+			     (algdata-signature (core-symbol "List"))))
+      (type-check/unify-list list-exp exps element-type
+	      (type-mismatch/list object
+		 "List elements do not share a common type")
+	(return-type object (**list-of element-type)))))
+
+(define-type-checker sequence
+  (type-rewrite (**enumFrom (sequence-from object))))
+
+(define-type-checker sequence-to
+  (type-rewrite (**enumFromTo (sequence-to-from object)
+			      (sequence-to-to object))))
+
+(define-type-checker sequence-then
+  (type-rewrite (**enumFromThen (sequence-then-from object)
+				(sequence-then-then object))))
+
+(define-type-checker sequence-then-to
+  (type-rewrite (**enumFromThenTo (sequence-then-to-from object)
+				  (sequence-then-to-then object)
+				  (sequence-then-to-to object))))
+
+(define-type-checker list-comp
+ (with-new-tyvars
+  (dolist (object (list-comp-quals object))
+    (if (is-type? 'qual-generator object)
+	(fresh-type pat-type
+	 (push pat-type (dynamic *non-generic-tyvars*))
+	 (type-check qual-generator pat pat-type-1
+	   (type-unify pat-type pat-type-1 #f)
+	   (type-check qual-generator exp qual-exp-type
+	     (type-unify (**list-of pat-type) qual-exp-type
+                            (type-mismatch/fixed object
+		 "Generator expression is not a list" qual-exp-type)))))
+	 (type-check qual-filter exp filter-type
+	   (type-unify filter-type *bool-type*
+              (type-mismatch/fixed object
+		"Filter must have type Bool" filter-type)))))
+  (type-check list-comp exp exp-type
+     (return-type object (**list-of exp-type)))))
+
+(define-type-checker section-l
+  (type-check section-l op op-type
+    (type-check section-l exp exp-type
+      (fresh-type a-type
+        (fresh-type b-type
+          (fresh-type c-type
+            (type-unify op-type (**arrow a-type b-type c-type)
+                (type-mismatch/fixed object
+		     "Binary function required in section" op-type))
+	    (type-unify b-type exp-type
+                  (type-mismatch object
+		      "Argument type mismatch" b-type exp-type))
+	    (return-type object (**arrow a-type c-type))))))))
+
+(define-type-checker section-r
+  (type-check section-r op op-type
+    (type-check section-r exp exp-type
+      (fresh-type a-type
+        (fresh-type b-type
+          (fresh-type c-type
+            (type-unify op-type (**arrow a-type b-type c-type)
+                  (type-mismatch/fixed object
+			 "Binary function required" op-type))
+	    (type-unify exp-type a-type
+                    (type-mismatch object
+			 "Argument type mismatch" a-type exp-type))
+	    (return-type object (**arrow b-type c-type))))))))
+
+(define-type-checker omitted-guard
+  (return-type object *bool-type*))
+
+(define-type-checker con-number
+  (let ((arg-type (instantiate-gtype
+		   (algdata-signature (con-number-type object)))))
+    (type-check con-number value arg-type1
+      (type-unify arg-type arg-type1 #f)
+      (return-type object *int-type*))))
+
+(define-type-checker sel
+  (let ((con-type (instantiate-gtype
+		   (con-signature (sel-constructor object)))))
+    (mlet (((res-type exp-type1) (get-ith-type con-type (sel-slot object))))
+      (type-check sel value exp-type
+        (type-unify exp-type exp-type1 #f)
+	(return-type object res-type)))))
+
+(define (get-ith-type type i)
+ (let ((args (ntycon-args type)))  ; must be an arrow
+  (if (eq? i 0)
+      (values (car args) (get-ith-type/last (cadr args)))
+      (get-ith-type (cadr args) (1- i)))))
+
+(define (get-ith-type/last type)
+  (if (eq? (ntycon-tycon type) (core-symbol "Arrow"))
+      (get-ith-type/last (cadr (ntycon-args type)))
+      type))
+
+(define-type-checker is-constructor
+  (let ((alg-type (instantiate-gtype
+		   (algdata-signature
+		    (con-alg (is-constructor-constructor object))))))
+    (type-check is-constructor value arg-type
+      (type-unify arg-type alg-type #f)
+      (return-type object *bool-type*))))
+
+(define-type-checker cast
+  (type-check cast exp _
+    (fresh-type res
+      (return-type object res))))
+
+;;; This is used for overloaded methods.  The theory is to avoid supplying
+;;; the context at the class level.  This type checks the variable as if it had
+;;; the supplied signature.
+
+(define-type-checker overloaded-var-ref
+  (let* ((var (overloaded-var-ref-var object))
+	 (gtype (overloaded-var-ref-sig object))
+	 (ovar-type (var-type var)))
+    (when (recursive-type? ovar-type)
+	 (error
+	  "Implementation error: overloaded method found a recursive type"))
+    (mlet (((ntype new-vars) (instantiate-gtype/newvars gtype))
+	   (object1 (insert-dict-placeholders
+		     (**var/def var) new-vars object)))
+	  (return-type object1 ntype))))
diff --git a/type/pattern-binding.scm b/type/pattern-binding.scm
new file mode 100644
index 0000000..769e155
--- /dev/null
+++ b/type/pattern-binding.scm
@@ -0,0 +1,38 @@
+;;; This implements the pattern binding rule.
+
+(define (apply-pattern-binding-rule? decls)
+ (not
+  (every (lambda (decl)
+	   (or (function-binding? decl)
+	       (simple-pattern-binding-with-signature? decl)))
+	 decls)))
+
+(define (function-binding? decl)
+  (let ((defs (valdef-definitions decl)))
+    (not (null? (single-fun-def-args (car defs))))))
+
+(define (simple-pattern-binding-with-signature? decl)
+  (let ((lhs (valdef-lhs decl))
+	(defs (valdef-definitions decl)))
+    (and (is-type? 'var-pat lhs)
+	 (null? (single-fun-def-args (car defs)))
+	 (not (eq? (var-signature (var-ref-var (var-pat-var lhs))) '#f)))))
+
+(define (do-pattern-binding-rule decls necessary-tyvars ng-list)
+  (setf ng-list (append necessary-tyvars ng-list))
+  (find-exported-pattern-bindings decls)
+  ng-list)
+
+(define (find-exported-pattern-bindings decls)
+  (dolist (decl decls)
+    (dolist (var-ref (collect-pattern-vars (valdef-lhs decl)))
+     (let ((var (var-ref-var var-ref)))
+      (when (def-exported? var)
+	(recoverable-error 'exported-pattern-binding
+           "Can't export pattern binding of ~A~%" var-ref))
+      (when (not (eq? (var-signature var) '#f))
+         (recoverable-error 'entire-group-needs-signature
+           "Variable ~A signature declaration ignored~%" var-ref))))))
+
+
+
diff --git a/type/type-decl.scm b/type/type-decl.scm
new file mode 100644
index 0000000..790c0ca
--- /dev/null
+++ b/type/type-decl.scm
@@ -0,0 +1,337 @@
+;;; This deals with declarations (let & letrec).  The input is a list of
+;;; declarations (valdefs) which may contain recursive-decl-groups, as
+;;; introduced in dependency analysis.  This function alters the list
+;;; of non-generic type variables.  Expressions containing declarations
+;;; need to rebind the non-generic list around the decls and all expressions
+;;; within their scope.
+
+;;; This returns an updated decl list with recursive decl groups removed.
+
+(define (type-decls decls)
+  (cond ((null? decls)
+	 '())
+	((is-type? 'recursive-decl-group (car decls))
+	 (let ((d (recursive-decl-group-decls (car decls))))
+ 	   (type-recursive d)
+	   (append d (type-decls (cdr decls)))))
+	(else
+	 (type-non-recursive (car decls))
+	 (cons (car decls)
+	       (type-decls (cdr decls))))))
+
+;;; This typechecks a mutually recursive group of declarations (valdefs).
+;;; Generate a monomorphic variable for each declaration and unify it with
+;;; the lhs of the decl.  The variable all-vars collects all variables defined
+;;; by the declaration group.  Save the values of placeholders and ng-list
+;;; before recursing.
+
+;;; The type of each variable is marked as recursive.
+
+(define (type-recursive decls)
+  (let ((old-ng (dynamic *non-generic-tyvars*))
+	(old-placeholders (dynamic *placeholders*))
+	(all-vars '())
+	(new-tyvars '())
+	(decls+tyvars '()))
+    ;; on a type error set all types to `a' and give up.
+    (setf (dynamic *placeholders*) '())
+    (recover-type-error 
+       (lambda (r)
+	 (make-dummy-sigs decls)
+	 (setf (dynamic *dict-placeholders*) old-placeholders)
+	 (funcall r))
+       ;; Type the lhs of each decl and then mark each variable bound
+       ;; in the decl as recursive.
+       (dolist (d decls)
+        (fresh-type lhs-type
+	  (push lhs-type (dynamic *non-generic-tyvars*))
+	  (push lhs-type new-tyvars)
+	  (type-decl-lhs d lhs-type)
+	  (push (tuple d lhs-type) decls+tyvars))
+	(dolist (var-ref (collect-pattern-vars (valdef-lhs d)))
+	  (let ((var (var-ref-var var-ref)))
+	    (push var all-vars)
+	    (setf (var-type var)
+		  (make recursive-type (type (var-type var))
+			(placeholders '()))))))
+
+;;; This types the decl right hand sides.  Each rhs type is unified with the
+;;; tyvar corresponding to the lhs.  Before checking the signatures, the
+;;; ng-list is restored.  
+
+       (dolist (d decls+tyvars)
+	 (let ((rhs-type (type-decl-rhs (tuple-2-1 d)))
+	       (lhs-type (tuple-2-2 d)))
+	   (type-unify lhs-type rhs-type
+		 (type-mismatch (tuple-2-1 d)
+			  "Decl type mismatch" lhs-type rhs-type))))
+       (setf (dynamic *non-generic-tyvars*) old-ng)
+       (let ((sig-contexts (check-user-signatures all-vars)))
+
+;;; This generalizes the signatures of recursive decls.  First, the
+;;; context of the declaration group is computed.  Any tyvar in the
+;;; bodies with a non-empty context must appear in all signatures that
+;;; are non-ambiguous.
+	  
+	 (let* ((all-tyvars (collect-tyvars/l new-tyvars))
+		(overloaded-tyvars '()))
+	   (dolist (tyvar all-tyvars)
+	      (when (and (ntyvar-context tyvar) (not (non-generic? tyvar)))
+		 (push tyvar overloaded-tyvars)))
+	   (reconcile-sig-contexts overloaded-tyvars sig-contexts)
+	 ;; We should probably also emit a warning about inherently
+	 ;; ambiguous decls.
+	   (when (and overloaded-tyvars
+		      (apply-pattern-binding-rule? decls))
+		 (setf (dynamic *non-generic-tyvars*)
+		       (do-pattern-binding-rule
+			decls overloaded-tyvars old-ng))
+		 (setf overloaded-tyvars '()))
+	 ;; The next step is to compute the signatures of the defined
+	 ;; variables and to define all recursive placeholders.  When
+	 ;; there is no context the placeholders become simple var refs.
+	 ;; and the types are simply converted.
+	   (cond ((null? overloaded-tyvars)
+		  (dolist (var all-vars)
+		    (let ((r (var-type var)))
+		      (setf (var-type var) (recursive-type-type (var-type var)))
+		      (dolist (p (recursive-type-placeholders r))
+		        (setf (recursive-placeholder-exp p)
+			      (**var/def var)))
+		      (generalize-type var))))
+	 ;; When the declaration has a context things get very hairy.
+	 ;; First, grap the recursive placeholders before generalizing the
+	 ;; types.
+		 (else
+		  ;; Mark the overloaded tyvars as read-only.  This prevents
+		  ;; signature unification from changing the set of tyvars
+		  ;; defined in the mapping.
+		  (dolist (tyvar overloaded-tyvars)
+		     (setf (ntyvar-read-only? tyvar) '#t))
+		  (let ((r-placeholders '()))
+		    (dolist (var all-vars)
+		     (let ((rt (var-type var)))
+		      (dolist (p (recursive-type-placeholders rt))
+			(push p r-placeholders))
+		      (setf (var-type var) (recursive-type-type rt))))
+	 ;; Now compute a signature for each definition and do dictionary
+	 ;; conversion.  The var-map defines the actual parameter associated
+	 ;; with each of the overloaded tyvars.
+		    (let ((var-map (map (lambda (decl)
+					 (tuple (decl-var decl)
+					  (generalize-overloaded-type
+					   decl overloaded-tyvars)))
+					decls)))
+	 ;; Finally discharge each recursive placeholder.
+		      (dolist (p r-placeholders)
+			(let ((ref-to (recursive-placeholder-var p))
+			      (decl-from
+			       (search-enclosing-decls
+				 (recursive-placeholder-enclosing-decls p)
+				 decls)))
+			  (setf (recursive-placeholder-exp p)
+				(recursive-call-code decl-from ref-to var-map)))
+			)))))
+	   (setf (dynamic *placeholders*)
+		 (process-placeholders
+		  (dynamic *placeholders*) old-placeholders decls)))))))
+
+;;; Non-recursive decls are easier.  Save the placeholders, use a fresh type
+;;; for the left hand side, check signatures, and generalize.
+
+(define (type-non-recursive decl)
+ (remember-context decl
+  (fresh-type lhs-type
+    (let ((old-placeholders (dynamic *placeholders*))
+	  (all-vars (map (lambda (x) (var-ref-var x))
+			    (collect-pattern-vars (valdef-lhs decl)))))
+     (setf (dynamic *placeholders*) '())
+     (recover-type-error
+      (lambda (r)
+        (make-dummy-sigs (list decl))
+	(setf (dynamic *placeholders*) old-placeholders)
+        (funcall r))
+      (type-decl-lhs decl lhs-type)
+      (let ((rhs-type (type-decl-rhs decl)))
+	(type-unify lhs-type rhs-type
+           (type-mismatch decl
+	       "Decl type mismatch" lhs-type rhs-type)))
+      (check-user-signatures all-vars)
+      (let ((all-tyvars (collect-tyvars lhs-type))
+	    (overloaded-tyvars '()))
+	(dolist (tyvar all-tyvars)
+	  (when (ntyvar-context tyvar)
+	     (push tyvar overloaded-tyvars)))
+	(when (and overloaded-tyvars
+		   (apply-pattern-binding-rule? (list decl)))
+	 (setf (dynamic *non-generic-tyvars*)
+	   (do-pattern-binding-rule
+	    (list decl) overloaded-tyvars (dynamic *non-generic-tyvars*)))
+	 (setf overloaded-tyvars '()))
+	(if (null? overloaded-tyvars)
+	    (dolist (var all-vars)
+	      (generalize-type var))
+	    (generalize-overloaded-type decl '()))
+	(setf (dynamic *placeholders*)
+	      (process-placeholders
+	       (dynamic *placeholders*) old-placeholders (list decl)))))))))
+
+;;; These functions type check definition components.
+
+;;; This unifies the type of the lhs pattern with a type variable.
+
+(define (type-decl-lhs object type)
+ (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*))))
+  (remember-context object
+   (type-check valdef lhs pat-type
+    (type-unify type pat-type #f)))))
+
+
+;;; This types the right hand side.  The *enclosing-decls* variable is
+;;; used to keep track of which decl the type checker is inside.  This
+;;; is needed for both defaulting (to find which module defaults apply)
+;;; and recursive types to keep track of the dictionary parameter variables
+;;; for recursive references.
+
+(define (type-decl-rhs object)
+ (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*))))
+  (remember-context object
+   (type-check/unify-list valdef definitions res-type
+       (type-mismatch/list object
+	   "Right hand sides have different types")
+       res-type))))
+
+
+;;; This is similar to typing lambda.
+
+(define-type-checker single-fun-def
+  (fresh-monomorphic-types (length (single-fun-def-args object)) tyvars
+    (type-check/list single-fun-def args arg-types
+      (unify-list tyvars arg-types)
+      (type-check/decls single-fun-def where-decls
+        (type-check/unify-list single-fun-def rhs-list rhs-type
+           (type-mismatch/list object
+			"Bodies have incompatible types")
+	  (return-type object (**arrow/l-2 arg-types rhs-type)))))))
+
+
+;;; These functions are part of the generalization process.
+
+;;; This function processes user signature declarations for the set of
+;;; variables defined in a declaration.  Since unification of one signature
+;;; may change the type associated with a previously verified signature,
+;;; signature unification is done twice unless only one variable is
+;;; involved.  The context of the signatures is returned to compare
+;;; with the overall context of the declaration group.
+
+(define (check-user-signatures vars)
+  (cond ((null? (cdr vars))
+	 (let* ((var (car vars))
+		(sig (var-signature var)))
+	   (if (eq? sig '#f)
+	       '()
+	       (list (tuple var (check-var-signature var sig))))))
+	(else
+	 (let ((sigs '()))
+	   (dolist (var vars)
+	     (let ((sig (var-signature var)))
+	       (unless (eq? sig '#f)
+		 (check-var-signature var sig))))
+	   (dolist (var vars)
+	     (let ((sig (var-signature var)))
+	       (unless (eq? sig '#f)
+		 (push (tuple var (check-var-signature var sig)) sigs))))
+	   sigs))))
+
+
+(define (check-var-signature var sig)
+  (mlet (((sig-type sig-vars) (instantiate-gtype/newvars sig)))
+    (dolist (tyvar sig-vars)
+      (setf (ntyvar-read-only? tyvar) '#t))
+    (type-unify (remove-recursive-type (var-type var)) sig-type
+	     (signature-mismatch var))
+    (dolist (tyvar sig-vars)
+      (setf (ntyvar-read-only? tyvar) '#f))
+    sig-vars))
+  
+;;; Once the declaration context is computed, it must be compared to the
+;;; contexts given by the user.  All we need to check is that all tyvars
+;;; constrained in the user signatures are also in the decl-context.
+;;; All user supplied contexts are correct at this point - we just need
+;;; to see if some ambiguous portion of the context exists.
+
+;;; This error message needs work.  We need to present the contexts.
+
+(define (reconcile-sig-contexts overloaded-tyvars sig-contexts)
+  (dolist (sig sig-contexts)
+    (let ((sig-vars (tuple-2-2 sig)))
+      (dolist (d overloaded-tyvars)
+	(when (not (memq d sig-vars))
+	  (type-error
+"Declaration signature has insufficiant context in declaration~%~A~%"
+            (tuple-2-1 sig)))))))
+
+;;; This is used for noisy type inference
+
+(define (report-typing var)
+ (when (memq 'type (dynamic *printers*))
+  (let* ((name (symbol->string (def-name var))))
+    (when (not (or (string-starts? "sel-" name)
+		   (string-starts? "i-" name)
+		   (string-starts? "default-" name)
+		   (string-starts? "dict-" name)))
+      (format '#t "~A :: ~A~%" var (var-type var))))))
+
+;;; This is used during error recovery.  When a type error occurs, all
+;;; variables defined in the enclosing declaration are set to type `a'
+;;; and typing is resumed.
+
+(define (make-dummy-sigs decls)
+  (let ((dummy-type (make gtype (context '(()))
+			        (type (**gtyvar 0)))))
+    (dolist (d decls)
+      (dolist (var-ref (collect-pattern-vars (valdef-lhs d)))
+        (let ((var (var-ref-var var-ref)))
+	  (setf (var-type var) dummy-type))))))
+
+
+;;; This is used to generalize the variable signatures.  If there is
+;;; an attached signature, the signature is used.  Otherwise the ntype
+;;; is converted to a gtype.
+
+(define (generalize-type var)
+  (if (eq? (var-signature var) '#f)
+      (setf (var-type var) (ntype->gtype (var-type var)))
+      (setf (var-type var) (var-signature var)))
+  (report-typing var))
+      
+;;; For overloaded types, it is necessary to map the declaration context
+;;; onto the generalized type.  User signatures may provide different but
+;;; equivilant contexts for different declarations in a decl goup.
+
+;;; The overloaded-vars argument allows ambiguous contexts.  This is not
+;;; needed for non-recursive vars since the context cannot be ambiguous.
+
+(define (generalize-overloaded-type decl overloaded-vars)
+  (let* ((var (decl-var decl))
+	 (sig (var-signature var))
+	 (new-tyvars '()))
+    (cond ((eq? sig '#f)
+	   (mlet (((gtype tyvars)
+		   (ntype->gtype/env (var-type var) overloaded-vars)))
+	      (setf (var-type var) gtype)
+	      (setf new-tyvars tyvars)))
+	  (else
+	   (mlet (((ntype tyvars) (instantiate-gtype/newvars sig)))
+	     (unify ntype (var-type var))
+	     (setf (var-type var) sig)
+	     (setf new-tyvars (prune/l tyvars)))))
+    (report-typing var)
+    (dictionary-conversion/definition decl new-tyvars)
+    new-tyvars))
+
+(define (remove-recursive-type ty)
+  (if (recursive-type? ty)
+      (recursive-type-type ty)
+      ty))
+
diff --git a/type/type-error-handlers.scm b/type/type-error-handlers.scm
new file mode 100644
index 0000000..ac7af9c
--- /dev/null
+++ b/type/type-error-handlers.scm
@@ -0,0 +1,40 @@
+;;; This file contains error handlers for the type checker.
+
+(define (type-error msg . args)
+  (apply (function phase-error) `(type-error ,msg ,@args))
+  (report-non-local-type-error)
+  (continue-from-type-error))
+
+(define (report-non-local-type-error)
+  (when (pair? (dynamic *type-error-handlers*))
+     (funcall (car (dynamic *type-error-handlers*)))))
+
+(define (continue-from-type-error)
+  (funcall (car (dynamic *type-error-recovery*))))
+
+(define (type-mismatch/fixed object msg type)
+  (format '#t "While typing ~A:~%~A~%Type: ~A~%" object msg type))
+
+(define (type-mismatch object msg type1 type2)
+  (format '#t "While type checking~%~A~%~A~%Types: ~A~%       ~A~%"
+	  object msg type1 type2))
+
+(define (type-mismatch/list types object msg)
+  (format '#t "While typing ~A:~%~A~%Types: ~%" object msg)
+  (dolist (type types)
+     (format '#t "~A~%" type)))
+
+;;; Error handlers
+
+(define (signature-mismatch var)
+  (format '#t
+      "Signature mismatch for ~A~%Inferred type: ~A~%Declared type: ~A~%"
+      var
+      (remove-type-wrapper (ntype->gtype (var-type var)))
+      (var-signature var)))
+
+(define (remove-type-wrapper ty)
+  (if (recursive-type? ty) (recursive-type-type ty) ty))
+
+
+	
\ No newline at end of file
diff --git a/type/type-macros.scm b/type/type-macros.scm
new file mode 100644
index 0000000..c6dc168
--- /dev/null
+++ b/type/type-macros.scm
@@ -0,0 +1,159 @@
+
+;;; This file also contains some random globals for the type checker:
+
+(define-walker type ast-td-type-walker)
+
+;;; Some pre-defined types
+(define *bool-type* '())
+(define *char-type* '())
+(define *string-type* '())
+(define *int-type* '())
+(define *integer-type* '())
+(define *rational-type* '())
+
+;;; These two globals are used throughout the typechecker to avoid
+;;; passing lots of stuff in each function call.
+
+(define *placeholders* '())
+(define *non-generic-tyvars* '())
+(define *enclosing-decls* '())
+
+;;; Used by the defaulting mechanism
+
+(define *default-decls* '())
+
+;;; Used in error handling & recovery
+
+(define *type-error-handlers* '())
+(define *type-error-recovery* '())
+
+
+;;; This associates a type checker function with an ast type.  The variable
+;;; `object' is bound to the value being types.
+
+(define-syntax (define-type-checker ast-type . cont)
+  `(define-walker-method type ,ast-type (object)
+     ,@cont))
+
+;;; This recursively type checks a structure slot in the current object.
+;;; This updates the ast in the slot (since type checking rewrites the ast)
+;;; and binds the computed type to a variable.  The slot must contain an
+;;; expression.
+
+(define-syntax (type-check struct slot var . cont)
+  `(mlet ((($$$ast$$$ ,var)
+	   (dispatch-type-check (struct-slot ',struct ',slot object))))
+	 (setf (struct-slot ',struct ',slot object) $$$ast$$$)
+	 ,@cont))
+
+;;; This is used to scope decls.
+
+(define-syntax (with-new-tyvars . cont)
+  `(dynamic-let ((*non-generic-tyvars* (dynamic *non-generic-tyvars*)))
+     ,@cont))
+
+
+;;; Similar to type-check, the slot must contain a list of decls.
+;;; This must be done before any reference to a variable defined in the
+;;; decls is typechecked.
+		
+(define-syntax (type-check/decls struct slot . cont)
+  `(with-new-tyvars
+    (let (($$$decls$$$
+	  (type-decls (struct-slot ',struct ',slot object))))
+     (setf (struct-slot ',struct ',slot object) $$$decls$$$)
+     ,@cont)))
+
+;;; The type checker returns an expression / type pair.  This
+;;; abstracts the returned value.
+
+(define-syntax (return-type object type)
+  `(values ,object ,type))
+
+;;; When an ast slot contains a list of expressions, there are two
+;;; possibilities: the expressions all share the same type or each has
+;;; an independant type.  In the first case, a single type (computed
+;;; by unifying all types in the list) is bound to a variable.
+
+(define-syntax (type-check/unify-list struct slot var error-handler . cont)
+  `(mlet ((($$$ast$$$ $$$types$$$)
+	   (do-type-check/list (struct-slot ',struct ',slot object))))
+    (setf (struct-slot ',struct ',slot object) $$$ast$$$)
+    (with-type-error-handler ,error-handler ($$$types$$$)
+       (unify-list/single-type $$$types$$$)
+       (let ((,var (car $$$types$$$)))
+	 ,@cont))))
+
+;;; When a list of expressions does not share a common type, the result is
+;;; a list of types.
+
+(define-syntax (type-check/list struct slot var . cont)
+  `(mlet ((($$$ast$$$ ,var)
+	   (do-type-check/list (struct-slot ',struct ',slot object))))
+    (setf (struct-slot ',struct ',slot object) $$$ast$$$)
+    ,@cont))
+
+;;; This creates a fresh tyvar and binds it to a variable.
+
+(define-syntax (fresh-type var . cont)
+  `(let ((,var (**ntyvar)))
+     ,@cont))
+
+;;; This drives the unification routine.  Two types are unified and the
+;;; context is updated.  Currently no error handling is implemented to
+;;; deal with unification errors.
+
+(define-syntax (type-unify type1 type2 error-handler)
+  `(with-type-error-handler ,error-handler ()
+     (unify ,type1 ,type2)))
+
+;;; This generates a fresh set of monomorphic type variables.
+
+(define-syntax (fresh-monomorphic-types n vars . cont)
+  `(with-new-tyvars
+     (let ((,vars '()))
+       (dotimes (i ,n)
+	   (let ((tv (**ntyvar)))
+	     (push tv ,vars)
+	     (push tv (dynamic *non-generic-tyvars*))))
+       ,@cont)))
+
+;;; This creates a single monomorphic type variable.
+
+(define-syntax (fresh-monomorphic-type var . cont)
+  `(let* ((,var (**ntyvar)))
+     (with-new-tyvars
+       (push ,var (dynamic *non-generic-tyvars*))
+       ,@cont)))
+
+;;; This is used to rewrite the current ast as a new ast and then
+;;; recursively type check the new ast.  The original ast is saved for
+;;; error message printouts.
+
+(define-syntax (type-rewrite ast)
+  `(mlet (((res-ast type) (dispatch-type-check ,ast))
+	  (res (**save-old-exp object res-ast)))
+      (return-type res type)))
+
+;;; These are the type error handlers
+
+(define-syntax (recover-type-error error-handler . body)
+ (let ((temp (gensym))
+       (err-fn (gensym)))
+  `(let/cc ,temp
+    (let ((,err-fn ,error-handler))
+     (dynamic-let ((*type-error-recovery*
+		    (cons (lambda ()
+			    (funcall ,err-fn ,temp))
+			  (dynamic *type-error-recovery*))))
+        ,@body)))))
+
+(define-syntax (with-type-error-handler handler extra-args . body)
+  (if (eq? handler '#f)
+      `(begin ,@body)
+      `(dynamic-let ((*type-error-handlers*
+		      (cons (lambda ()
+			     (,(car handler) ,@extra-args ,@(cdr handler)))
+			    (dynamic *type-error-handlers*))))
+	    ,@body)))
+
diff --git a/type/type-main.scm b/type/type-main.scm
new file mode 100644
index 0000000..c5ffe14
--- /dev/null
+++ b/type/type-main.scm
@@ -0,0 +1,56 @@
+
+;;; This is the main entry point to the type checker.
+
+
+(define (do-haskell-type-check object modules)
+  (type-init modules)
+  (when (is-type? 'let object) ; may be void
+    (dynamic-let ((*non-generic-tyvars* '())
+		  (*placeholders* '())
+		  (*enclosing-decls* '()))
+      (type-check/decls let decls
+	 (setf (dynamic *non-generic-tyvars*) '())
+         (process-placeholders (dynamic *placeholders*) '() '()))))
+  'done)
+
+;;; This is the main recursive entry to the type checker.
+
+(define (dispatch-type-check exp)
+ (remember-context exp
+  (call-walker type exp)))
+
+(define (do-type-check/list exps)
+  (if (null? exps)
+      (values '() '())
+      (mlet (((obj1 type1) (dispatch-type-check (car exps)))
+	     ((objs types) (do-type-check/list (cdr exps))))
+	(values (cons obj1 objs) (cons type1 types)))))
+
+(define (type-init modules)
+  ;; Built in types
+  (setf *char-type* (**ntycon (core-symbol "Char") '()))
+  (setf *string-type* (**ntycon (core-symbol "List")
+				(list *char-type*)))
+  (setf *bool-type* (**ntycon (core-symbol "Bool") '()))
+  (setf *int-type* (**ntycon (core-symbol "Int") '()))
+  (setf *integer-type* (**ntycon (core-symbol "Integer") '()))
+  (setf *rational-type* (**ntycon (core-symbol "Ratio")
+				  (list *integer-type*)))
+  (setf *default-decls* '())
+  (dolist (m modules)
+    (let ((default-types '()))
+      (dolist (d (default-decl-types (module-default m)))
+        (let* ((ty (ast->gtype '() d))
+	       (ntype (gtype-type ty)))
+	  (cond ((not (null? (gtype-context ty)))
+		 (recoverable-error 'not-monotype
+		   "~A is not a monotype in default decl" ty))
+		((not (type-in-class? ntype (core-symbol "Num")))
+		 (recoverable-error 'not-Num-class
+		   "~A is not in class Num" ty))
+		(else
+		 (push ntype default-types)))))
+      (push (tuple (module-name m) (reverse default-types)) *default-decls*))))
+
+(define (remember-placeholder placeholder)
+  (push placeholder (dynamic *placeholders*)))
diff --git a/type/type-vars.scm b/type/type-vars.scm
new file mode 100644
index 0000000..4091ce4
--- /dev/null
+++ b/type/type-vars.scm
@@ -0,0 +1,60 @@
+;;; This type checks a variable.  Possible cases:
+;;;  a) recursive variables
+;;;  b) method variables
+;;;  c) generalized variables 
+;;;  d) other variables
+
+(define-type-checker var-ref
+ (let* ((var (var-ref-var object))
+	(type (var-type var)))
+   (cond ((method-var? var)
+;;; The context of a method variable always has the carrier class
+;;; first.
+	  (mlet (((ntype new-tyvars) (instantiate-gtype/newvars type))
+		 (carrier-tyvar (car new-tyvars))
+		 (extra-context (cdr new-tyvars))
+		 (p (**method-placeholder
+		     var carrier-tyvar (dynamic *enclosing-decls*) object))
+		 (new-object (insert-dict-placeholders p extra-context object)))
+	    (remember-placeholder p)
+	    (return-type (**save-old-exp object new-object) ntype)))
+	 ((recursive-type? type)
+	  (let ((placeholder (**recursive-placeholder
+			      var (dynamic *enclosing-decls*))))
+	    (push placeholder (recursive-type-placeholders type))
+	    (return-type placeholder (recursive-type-type type))))
+	 ((gtype? type)
+	  (mlet (((ntype new-vars) (instantiate-gtype/newvars type))
+		 (object1 (insert-dict-placeholders object new-vars object)))
+            (return-type (if (eq? object1 object)
+			     object
+			     (**save-old-exp object object1))
+			 ntype)))
+	 (else
+	  (return-type object type)))))
+
+;;; This takes an expression and a context and returns an updated
+;;; expression containing placeholders for the context information
+;;; implied by the context.  Tyvars in the context are added to dict-vars.
+
+(define (insert-dict-placeholders object tyvars var)
+  (cond ((null? tyvars)
+	 object)
+	((null? (ntyvar-context (car tyvars)))
+	 (insert-dict-placeholders object (cdr tyvars) var))
+	(else
+	 (let ((tyvar (car tyvars)))
+	   (insert-dict-placeholders
+	    (insert-dict-placeholders/tyvar
+	     tyvar (ntyvar-context tyvar) object var)
+	    (cdr tyvars)
+	    var)))))
+
+(define (insert-dict-placeholders/tyvar tyvar classes object var)
+  (if (null? classes)
+      object
+      (let ((p (**dict-placeholder
+		 (car classes) tyvar (dynamic *enclosing-decls*) var)))
+	(remember-placeholder p)
+	(insert-dict-placeholders/tyvar tyvar (cdr classes) 
+					(**app object p) var))))
diff --git a/type/type.scm b/type/type.scm
new file mode 100644
index 0000000..8a3a82f
--- /dev/null
+++ b/type/type.scm
@@ -0,0 +1,32 @@
+(define-compilation-unit type
+  (source-filename "$Y2/type/")
+  (require ast haskell-utils)
+  (unit type-macros
+        (source-filename "type-macros.scm"))
+  (unit unify
+	(require type-macros)
+	(source-filename "unify.scm"))
+  (unit type-main
+	(require type-macros)
+	(source-filename "type-main.scm"))
+  (unit type-decl
+	(require type-macros)
+	(source-filename "type-decl.scm"))
+  (unit dictionary
+	(require type-macros)
+	(source-filename "dictionary.scm"))
+  (unit default
+	(require type-macros)
+	(source-filename "default.scm"))
+  (unit pattern-binding
+	(require type-macros)
+	(source-filename "pattern-binding.scm"))
+  (unit type-vars
+	(require type-macros)
+	(source-filename "type-vars.scm"))
+  (unit expression-typechecking
+	(require type-macros)
+	(source-filename "expression-typechecking.scm"))
+  (unit type-error-handlers
+	(require type-macros)
+	(source-filename "type-error-handlers.scm")))
diff --git a/type/unify.scm b/type/unify.scm
new file mode 100644
index 0000000..59248c9
--- /dev/null
+++ b/type/unify.scm
@@ -0,0 +1,154 @@
+
+;;; File: type/unify.scm   Author: John
+
+;;; This is the basic unification algorithm used in type checking.
+
+;;; Unification failure invokes the current type error handler
+
+;;; Start by removing instantiated type variables from the type.
+
+(define (unify type1 type2)
+  (unify-1 (prune type1) (prune type2)))
+
+;;; The only real tweak here is the read-only bit on type variables.
+;;; The rule is that a RO tyvar can be unified only with a generic
+;;; non-RO tyvar which has the same or more general context.
+
+;;; Aside from this, this is standard unification except that context
+;;; propagation is needed when a tyvar with a non-empty context is
+;;; instantiated.
+
+;;; If type2 is a tyvar and type1 is not they are switched.
+
+(define (unify-1 type1 type2)
+    (cond ((eq? type1 type2)  ;; this catches variable to variable unify
+	   'OK)
+	  ((ntyvar? type1)
+	   (cond ((occurs-in-type type1 type2)
+		  (type-error "Circular type: cannot unify ~A with ~A"
+			      type1 type2))
+		 ((ntyvar-read-only? type1)
+		  (cond ((or (not (ntyvar? type2)) (ntyvar-read-only? type2))
+			 (type-error
+			  "Signature too general: cannot unify ~A with ~A"
+			  type1 type2))
+			(else
+			 (unify-1 type2 type1))))
+		 ((and (ntyvar? type2)
+		       (ntyvar-read-only? type2)
+		       (non-generic? type1))
+		  (type-error
+ "Type signature cannot be used: monomorphic type variables present."))
+		 (else
+		  (instantiate-tyvar type1 type2)
+		  (let ((classes (ntyvar-context type1)))
+		    (if (null? classes)
+			'OK
+			(propagate-contexts/ntype type1 type2 classes))))))
+	  ((ntyvar? type2)
+	   (unify-1 type2 type1))
+	  ((eq? (ntycon-tycon type1) (ntycon-tycon type2))
+	   (unify-list (ntycon-args type1) (ntycon-args type2)))
+	  (else
+	   (let ((etype1 (expand-ntype-synonym type1))
+		 (etype2 (expand-ntype-synonym type2)))
+	    (if (same-tycon? (ntycon-tycon etype1) (ntycon-tycon etype2))
+		(unify-list (ntycon-args etype1) (ntycon-args etype2))
+		;; This error message should probably show both the original
+		;; and the expanded types for clarity.
+		(type-error
+		      "Type conflict: type ~A does not match ~A"
+			    etype1 etype2))))))
+
+
+(define-integrable (instantiate-tyvar tyvar val)
+  (setf (ntyvar-value tyvar) val))
+
+;;; This is needed since interface files may leave multiple def's
+;;; for the same tycon sitting around.
+
+(define (same-tycon? ty1 ty2)
+  (or (eq? ty1 ty2)
+      (and (eq? (def-name ty1) (def-name ty2))
+	   (eq? (def-module ty1) (def-module ty2)))))
+
+
+;;; unifies two lists of types pairwise.  Used for tycon args.
+
+(define (unify-list args1 args2)
+  (if (null? args1)
+      'OK
+      (begin (unify-list (cdr args1) (cdr args2))
+	     (unify (car args1) (car args2)))))
+
+;;; combines a list of types into a single type.  Used in constructs
+;;; such as [x,y,z] and case expressions.
+
+(define (unify-list/single-type types)
+  (when (not (null? types))
+    (let ((type (car types)))
+      (dolist (type2 (cdr types))
+        (unify type type2)))))
+
+;;; This propagates the context from a just instantiated tyvar to the
+;;; instantiated value.  If the value is a tycon, instances must be
+;;; looked up.  If the value is a tyvar, the context is added to that of
+;;; other tyvar.
+
+;;; This is used to back out of the unification on errors.  This is a
+;;; poor mans trail stack!  Without this, error messages get very
+;;; obscure.
+
+(define *instantiated-tyvar* '())
+
+(define (propagate-contexts/ntype tyvar type classes)
+ (dynamic-let ((*instantiated-tyvar* tyvar))
+    (propagate-contexts/inner type classes)))
+
+(define (propagate-contexts/inner type classes)
+ (let ((type (prune type)))
+  (if (ntyvar? type)
+      (if (ntyvar-read-only? type)
+	  (if (context-implies? (ntyvar-context type) classes)
+	      'OK ; no need for context propagation here
+	      (begin 
+		(setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f)
+		(type-error "Signature context is too general")))
+	  (if (null? (ntyvar-context type))
+	      (setf (ntyvar-context type) classes)
+	      (setf (ntyvar-context type)
+		    (merge-contexts classes (ntyvar-context type)))))
+      (propagate-contexts-1 (expand-ntype-synonym type) classes))))
+
+;;; The type has now been expanded.  This propagates each class constraint
+;;; in turn.
+
+(define (propagate-contexts-1 type classes)
+  (dolist (class classes)
+     (propagate-single-class type class)))
+
+;;; Now we have a single class & data type.  Either an instance decl can
+;;; be found or a type error should be signalled.  Once the instance
+;;; decl is found, contexts are propagated to the component types.
+
+(define (propagate-single-class type class)
+  (let ((instance (lookup-instance (ntycon-tycon type) class)))
+    (cond ((eq? instance '#f)
+	   ;; This remove the instantiation which caused the type
+	   ;; error - perhaps stop error propagation & make
+	   ;; error message better.
+	   (setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f)
+	   (type-error "Type ~A is not in class ~A" type class))
+	  (else
+	   ;; The instance contains a list of class constraints for
+	   ;; each argument.  This loop pairs the argument to the
+	   ;; type constructor with the context required by the instance
+	   ;; decl.
+	   (dolist2 (classes (instance-gcontext instance))
+		    (arg (ntycon-args type))
+	     (propagate-contexts/inner arg classes)))))
+  'OK)
+
+;;; The routines which handle contexts (merge-contexts and context-implies?)
+;;; are in type-utils.  The occurs check is also there.
+