1 files changed, 154 insertions, 0 deletions
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.
+