(module tc-lambda-unit (lib "a-unit.ss")
  
  (require "planet-requires.ss"
           "signatures.ss"
           "types.ss" ;; doesn't need tests
           "types-aux.ss" ;; maybe needs tests
           "type-environments.ss" ;; doesn't need tests
           "lexical-env.ss" ;; maybe needs tests
           "type-annotation.ss" ;; has tests
           "effects.ss"
           "utils.ss"
           "tc-utils.ss"
           (lib "match.ss"))
  (require-for-template (lib "match.ss") "internal-forms.ss")
  
  (require-libs)
  
  (require (planet "environment.ss" ("cobbe" "environment.plt" 3 0)))  
    
  (require-for-template mzscheme)
  
  (import typechecker^)
  (export tc-lambda^)
  
  (define (remove-var id thns elss)
    (let/ec exit
      (define (fail) (exit #f))
      (define (rv e)
        (match e
          [($ var-true-effect v) (if (module-identifier=? v id) (make-latent-var-true-effect) (fail))]
          [($ var-false-effect v) (if (module-identifier=? v id) (make-latent-var-false-effect) (fail))]
          [(or ($ true-effect) ($ false-effect)) e]
          [($ restrict-effect t v) (if (module-identifier=? v id) (make-latent-restrict-effect t) (fail))]
          [($ remove-effect t v) (if (module-identifier=? v id) (make-latent-remove-effect t) (fail))]))
      (cons (map rv thns) (map rv elss))))
    
  
  ;; typecheck a single lambda, with argument list and body
  ;; fixme: abstract the two cases!
  ;; syntax-list expr-list -> type
  (define (tc/lambda-clause args body)
    (syntax-case args ()
      [(args ...)
       (let* ([arg-list (syntax->list #'(args ...))]
              [arg-types (map get-type arg-list)])
         (with-lexical-env/extend 
          arg-list arg-types
          (match (tc-exprs (syntax->list body))   
            [($ tc-result t thn els)
             (cond
               ;; this is T-AbsPred               
               ;; if this function takes only one argument, and all the effects are about that one argument
               [(and (= 1 (length arg-list)) (remove-var (car arg-list) thn els))
                => (lambda (thn/els) (make-arr arg-types t #f (car thn/els) (cdr thn/els)))]
               ;; otherwise, the simple case
               [else (make-arr arg-types t)])]
            [_ (int-err "bad match")])))]
      [(args ... . rest)
       (let* ([arg-list (syntax->list #'(args ...))]
              [arg-types (map get-type arg-list)]
              [rest-type (get-type #'rest)])
         (with-lexical-env/extend 
          (cons #'rest arg-list) 
          (cons (make-Listof rest-type) arg-types)
          (match-let ([($ tc-result t thn els) (tc-exprs (syntax->list body))])
            (make-arr arg-types t rest-type))))]))

  ;(trace tc-args)
  
  ;; tc/mono-lambda : syntax-list syntax-list -> Funty
  ;; typecheck a sequence of case-lambda clauses
  (define (tc/mono-lambda formals bodies)
    (make-funty (map tc/lambda-clause (syntax->list formals) (syntax->list bodies))))
  ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
  ;; tc/lambda syntax syntax-list syntax-list -> Type
  (define (tc/lambda form formals bodies)
    (if (syntax-property form 'typechecker:plambda)
        (tc/plambda form formals bodies)
        (ret (tc/mono-lambda formals bodies))))
  ;; tc/plambda syntax syntax-list syntax-list -> Poly
  ;; formals and bodies must by syntax-lists
  (define (tc/plambda form formals bodies)
    (with-syntax ([tvars (syntax-property form 'typechecker:plambda)])
      (let* ([literal-tvars (map syntax-e (syntax->list #'tvars))]
             [new-tvars (map make-tvar literal-tvars)]
             [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
                   (tc/mono-lambda formals bodies))])
        (ret (make-poly literal-tvars ty)))))

  
  )