Celestin Apprentice 2/Apprentice-Release2.iso/Tools/Languages/MacHaskell 2.2/type/unify.scm

Text File | 1994-09-27 | 5.4 KB | 155 lines | [TEXT/CCL2]

;;; 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? (forward-def (ntycon-tycon type1))
        (forward-def (ntycon-tycon type2)))
       (unify-list (ntycon-args type1) (ntycon-args type2)))
      (else
       (let ((etype1 (expand-ntype-synonym type1))
         (etype2 (expand-ntype-synonym type2)))
         ;; same-tycon? is part of util/interface-check
        (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))

;;; 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) (remove-dynamic 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)
 (if (eq? class (core-symbol "DynamicType"))
  (propagate-dynamic-class type)
  (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)

(define (propagate-dynamic-class type)
  (dolist (arg (ntycon-args type))
     (propagate-contexts/inner arg (list (core-symbol "DynamicType")))))

;;; The routines which handle contexts (merge-contexts and context-implies?)
;;; are in type-utils.  The occurs check is also there.