;;; 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.