 ;;    E |- lambda x:A . t  ::>  prod x:A . B
 ;;}
 
-(defn type-of-abs [env x A t]
+(defn type-of-abs [def-env env x A t]
   (let [env' (env-put env x A)
-        [status B :as res] (type-of env' t)]
+        [status B] (type-of def-env env' t)]
     (if (= status :ko)
-      res
+      [:ko {:msg "Cannot calculate codomain type of abstraction."
+            :term (list 'lambda [x A] t) :from B}]
       (let [tprod (list 'prod [x A] B)
-            [status sort :as res] (type-of env tprod)]
+            [status sort] (type-of def-env env tprod)]
         (if (= status :ko)
-          res
-          (if (not (s/valid? ::sx/sort (b/normalize sort)))
-            [:ko {:msg "Not a valid type" :term tprod :env env}]
+          [:ko {:msg "Not a valid codomain type in abstraction (cannot calculate super-type)."
+                :term (list 'lambda [x A] t)
+                :codomain B :from sort}]
+          (if (not (stx/sort? (norm/normalize def-env sort)))
+            [:ko {:msg "Not a valid codomain type in abstraction (super-type not a sort)."
+                  :term (list 'lambda [x A] t)
+                  :codomain B
+                  :type sort}]
             [:ok tprod]))))))
 
 (example
- (type-of '[[bool :type] [t bool] [y bool]]
+ (type-of {} '[[bool :type] [t bool] [y bool]]
           '(lambda [x bool] x))
  => '[:ok (prod [x bool] bool)])
 
 (example
- (type-of [] '(lambda [x :type] x)) => '[:ok (prod [x :type] :type)])
-
-(example
- (type-of '[[y bool]] '(lambda [x bool] x))
- => '[:ko {:msg "No such variable", :term bool, :env [[y bool] [x bool]]}])
-
- (example
-  (type-of '[[y :type] [z y]] '(lambda [x z] x))
-  => '[:ko {:msg "Not a correct type", :term z, :env [[y :type] [z y] [x z]]}])
-
-(example
- (type-of '[[y bool]] '(lambda [x :type] y))
- => '[:ko {:msg "No such variable", :term bool, :env [[y bool] [x :type]]}])
-
-(example
- (type-of '[[y bool]] '(lambda [x :type] :kind))
- => [:ko {:msg "Kind has not type"}])
-
-(example
- (type-of '[[y bool]] '(lambda [x :type] :type))
- => [:ko {:msg "Kind has not type"}])
-
- (example
-  (type-of '[[w :type] [y w] [z y]] '(lambda [x :type] z))
-  => '[:ko {:msg "Not a correct type",
-            :term y,
-            :env [[w :type] [y w] [z y] [x :type]]}])
+ (type-of {} [] '(lambda [x :type] x)) => '[:ok (prod [x :type] :type)])
+
+(example
+ (type-of {} '[[y bool]] '(lambda [x bool] x))
+ => '[:ko {:msg "Cannot calculate codomain type of abstraction.", :term (lambda [x bool] x),
+           :from {:msg "Cannot calculate type of variable.", :term x,
+                  :from {:msg "No such variable in type environment", :term bool}}}])
+
+(example
+ (type-of {} '[[y :type] [z y]] '(lambda [x z] x))
+ => '[:ko {:msg "Cannot calculate codomain type of abstraction.", :term (lambda [x z] x),
+           :from {:msg "Not a correct type (super-type is not a sort)", :term x, :type z, :sort y}}])
+
+(example
+ (type-of {} '[[y bool]] '(lambda [x :type] y))
+ => '[:ko {:msg "Cannot calculate codomain type of abstraction.", :term (lambda [x :type] y),
+           :from {:msg "Cannot calculate type of variable.", :term y,
+                  :from {:msg "No such variable in type environment", :term bool}}}])
+
+(example
+ (type-of {} '[[y bool]] '(lambda [x :type] :kind))
+ => '[:ko {:msg "Cannot calculate codomain type of abstraction.", :term (lambda [x :type] :kind),
+           :from {:msg "Kind has not type" :term :kind}}])
+
+(example
+ (type-of {} '[[y bool]] '(lambda [x :type] :type))
+ => '[:ko {:msg "Not a valid codomain type in abstraction (cannot calculate super-type).",
+           :term (lambda [x :type] :type), :codomain :kind,
+           :from {:msg "Cannot calculate codomain type of product.", :term :kind,
+                  :from {:msg "Kind has not type", :term :kind}}}])
+(example
+ (type-of {} '[[w :type] [y w] [z y]] '(lambda [x :type] z))
+ => '[:ko {:msg "Cannot calculate codomain type of abstraction.", :term (lambda [x :type] z),
+           :from {:msg "Not a correct type (super-type is not a sort)", :term z, :type y, :sort w}}])
 
 ;;{
 ;;       E |- rator ::> prod x:A . B    E|- rand :: A

         type-of-var
         type-of-prod
         type-of-abs
         type-of-app)

(defn type-of [env term]
  (let [[tag _] (sx/validate ::sx/term term)]
    (case tag
      :kind [:ko {:msg "Kind has not type"}]
      :type (type-of-type)
      :var (type-of-var env term)
      :bind (let [[binder [x ty] body] term]
              (case binder
                lambda (type-of-abs env x ty body)
                prod (type-of-prod env x ty body)
                (throw (ex-info "No such binder (please report)" {:binder binder}))))
      :app (type-of-app env (first term) (second term))
      (throw (ex-info "Invalid term (please report)" {:term term})))))

(example
 (type-of [] :kind) => [:ko {:msg "Kind has not type"}])

(defn type-check? [env term type]
  (let [[status type'] (type-of env term)]
    (if (= status :ok)
      (b/beta-eq? type type')
      (throw (ex-info "Cannot check type of term" {:term term :env env})))))


;;{
;;

(defn env-put [env x t]
  (conj env [x t]))

(defn mk-env [& args]
  args)


;;{
;; ## Synthesis rules
;;}
