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