(module tc-let-unit (lib "a-unit.ss")
  (require "signatures.ss"
           (lib "match.ss")
           "types.ss"
           "types-aux.ss"
           "effects.ss"
           "tc-utils.ss"
           "subtype.ss"
           "subst.ss"
           "infer2.ss"
           "type-annotation.ss"
           "type-env.ss"
           "type-environments.ss"
           "lexical-env.ss"
           (lib "kerncase.ss" "syntax"))
  
  (require-for-template (lib "match.ss") "internal-forms.ss" mzscheme)
  (require-for-syntax (lib "match.ss") "internal-forms.ss")
  
  
  (import typechecker^)
  (export tc-let^)
  
  (define (do-check expr->type namess types form exprs body)
    ;; just for error reporting
    (define clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)]))
    ;; extend the lexical environment for checking the body
    (with-lexical-env/extend 
     ;; the list of lists of name
     namess
     ;; the types
     types
     (for-each (lambda (stx e t) (check-type stx (expr->type e) t))
               clauses
               exprs 
               (map list->values-ty types))
     (tc-exprs (syntax->list body))))
  
  #|
;; this is more abstract, but sucks
  (define ((mk f) namess exprs body form)
    (let* ([names (map syntax->list (syntax->list namess))]
           [exprs (syntax->list exprs)])
      (f (lambda (e->t namess types exprs) (do-check e->t namess types form exprs body)) names exprs)))
  
  (define tc/letrec-values 
    (mk (lambda (do names exprs)
          (let ([types (map (lambda (l) (map get-type l)) names)])
            (do tc-expr/t names types exprs)))))
  
  (define tc/let-values
    (mk (lambda (do names exprs)
          (let* (;; the types of the exprs
                 [inferred-types (map tc-expr/t exprs)]
                 ;; the annotated types of the name (possibly using the inferred types)
                 [types (map get-type/infer names inferred-types)])
            (do (lambda (x) x) names types inferred-types)))))
  |#
  
  (define (tc/letrec-values namess exprs body form)
    (let* ([names (map syntax->list (syntax->list namess))]
           [exprs (syntax->list exprs)]
           [types (map (lambda (l) (map get-type l)) names)])             
      (do-check tc-expr/t names types form exprs body)))
  
  (define (tc/let-values namess exprs body form)
    (let* (;; a list of each name clause
           [names (map syntax->list (syntax->list namess))]
           ;; all the trailing expressions - the ones actually bound to the names
           [exprs (syntax->list exprs)]
           ;; the types of the exprs
           [inferred-types (map tc-expr/t exprs)]
           ;; the annotated types of the name (possibly using the inferred types)
           [types (map get-type/infer names inferred-types)])
      (do-check (lambda (x) x) names types form inferred-types body)))

  
  )