(.module:
  lux
  (lux (control [monad #+ do])
       (data [error])
       [macro]
       (language (type ["tc" check])))
  [///]
  [// #+ Operation])

(def: #export (with-type expected action)
  (All [a] (-> Type (Operation a) (Operation a)))
  (function (_ compiler)
    (case (action (set@ #.expected (#.Some expected) compiler))
      (#error.Success [compiler' output])
      (let [old-expected (get@ #.expected compiler)]
        (#error.Success [(set@ #.expected old-expected compiler')
                         output]))

      (#error.Error error)
      (#error.Error error))))

(def: #export (with-env action)
  (All [a] (-> (tc.Check a) (Operation a)))
  (function (_ compiler)
    (case (action (get@ #.type-context compiler))
      (#error.Error error)
      ((///.fail error) compiler)

      (#error.Success [context' output])
      (#error.Success [(set@ #.type-context context' compiler)
                       output]))))

(def: #export (with-fresh-env action)
  (All [a] (-> (Operation a) (Operation a)))
  (function (_ compiler)
    (let [old (get@ #.type-context compiler)]
      (case (action (set@ #.type-context tc.fresh-context compiler))
        (#error.Success [compiler' output])
        (#error.Success [(set@ #.type-context old compiler')
                         output])

        output
        output))))

(def: #export (infer actualT)
  (-> Type (Operation Any))
  (do ///.Monad<Operation>
    [expectedT macro.expected-type]
    (with-env
      (tc.check expectedT actualT))))

(def: #export (with-inference action)
  (All [a] (-> (Operation a) (Operation [Type a])))
  (do ///.Monad<Operation>
    [[_ varT] (..with-env
                tc.var)
     output (with-type varT
              action)
     knownT (..with-env
              (tc.clean varT))]
    (wrap [knownT output])))