X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=eb9d376f2aea3841eae4f0a96236bd5b690fceb9;hb=26b754bcd3763fd7624637adab0635edefa1168f;hp=0c0646d05a559dfc745c044d7fa1b2ced6a9e01a;hpb=d356a5023cc06477b6d66a7b22a031ad7dffe947;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 0c0646d05..eb9d376f2 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -75,7 +75,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = 
@@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te =
          Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
-    | C.Meta (_,l) ->
+    | C.Meta (mno,l) ->
        List.fold_right
         (fun x i ->
           match x with
              None -> i
            | Some x -> i && does_not_occur ~subst context n nn x) l true &&
        (try
-         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+         let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in
           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
         with
          CicUtil.Subst_not_found _ -> true)
@@ -273,10 +273,11 @@ and does_not_occur ?(subst=[]) context n nn te =
        does_not_occur ~subst context n nn so &&
         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
          dest
-    | C.LetIn (name,so,dest) ->
+    | C.LetIn (name,so,ty,dest) ->
        does_not_occur ~subst context n nn so &&
-        does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
-         (n + 1) (nn + 1) dest
+        does_not_occur ~subst context n nn ty &&
+         does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
+          (n + 1) (nn + 1) dest
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
     | C.Var (_,exp_named_subst)
@@ -292,8 +293,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
         in
          List.fold_right
           (fun (_,_,ty,bo) i ->
@@ -304,8 +309,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
         in
          List.fold_right
           (fun (_,ty,bo) i ->
@@ -757,9 +766,10 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
-   | C.LetIn (name,so,ta) ->
+   | C.LetIn (name,so,ty,ta) ->
       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
-       check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
+       check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
+        check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
@@ -791,7 +801,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -842,7 +852,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -886,7 +896,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -899,7 +914,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -914,10 +934,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
   function
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
-      (match List.nth context (n-1) with
+      (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
+           guarded_by_destructors ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -935,10 +955,11 @@ and guarded_by_destructors ~subst context n nn kl x safes =
       guarded_by_destructors ~subst context n nn kl x safes so &&
        guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
-   | C.LetIn (name,so,ta) ->
+   | C.LetIn (name,so,ty,ta) ->
       guarded_by_destructors ~subst context n nn kl x safes so &&
-       guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context)
-        (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
+       guarded_by_destructors ~subst context n nn kl x safes ty &&
+        guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
+         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
        if not (List.length tl > k) then false
@@ -985,7 +1006,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                      | (_,_,ty,_)::_ ->
                         fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys@lefts,len,isinductive,paramsno,cl')
+                    (lefts@tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1038,7 +1059,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1091,7 +1112,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -1104,7 +1130,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1257,7 +1288,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
         let n_plus_len = n + len
         and nn_plus_len = nn + len
         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+        and tys,_ =
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+	    ) ([],0) fl
+        in
          List.fold_right
           (fun (_,ty,bo) i ->
             i && does_not_occur ~subst context n nn ty &&
@@ -1298,7 +1335,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
+       in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1309,7 +1352,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+	  ) ([],0) fl
+       in
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1325,11 +1374,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   let arity1 = CicReduction.whd ~subst context arity1 in
   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
    match arity1, CicReduction.whd ~subst context arity2 with
-     (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
+     (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
        if b then
-	 check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+	 check_allowed_sort_elimination ~subst ~metasenv ~logger 
+           ((Some (name,C.Decl so1))::context) uri i
           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
           ugraph1
        else
@@ -1445,11 +1495,9 @@ and check_metasenv_consistency ~logger ~subst metasenv context
          [] -> []
        | (Some (n,C.Decl t))::tl ->
            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
-       | (Some (n,C.Def (t,None)))::tl ->
-           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
-       | (Some (n,C.Def (t,Some ty)))::tl ->
-           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
+       | (Some (n,C.Def (t,ty)))::tl ->
+           (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
     in
      aux 1 canonical_context
    in
@@ -1458,8 +1506,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context
        match (t,ct) with
        | _,None -> ugraph
        | Some t,Some (_,C.Def (ct,_)) ->
+          (*CSC: the following optimization is to avoid a possibly expensive
+                 reduction that can be easily avoided and that is quite
+                 frequent. However, this is better handled using levels to
+                 control reduction *)
+          let optimized_t =
+           match t with
+              Cic.Rel n ->
+               (try
+                 match List.nth context (n - 1) with
+                    Some (_,C.Def (te,_)) -> S.lift n te
+                  | _ -> t
+                with
+                 Failure _ -> t)
+            | _ -> t
+          in
+(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
+else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
 	   let b,ugraph1 = 
-	     R.are_convertible ~subst ~metasenv context t ct ugraph 
+	     R.are_convertible ~subst ~metasenv context optimized_t ct ugraph 
 	   in
 	   if not b then
 	     raise 
@@ -1504,10 +1569,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t,ugraph
-          | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
-          | Some (_,C.Def (bo,None)) ->
-             debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
-              type_of_aux ~logger context (S.lift n bo) ugraph
+          | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
           | None -> raise 
 	      (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
         with
@@ -1543,8 +1605,11 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_gt t' t ugraph in
-         (C.Sort (C.Type t')),ugraph1
+       (try
+         let ugraph1 = CicUniv.add_gt t' t ugraph in
+           (C.Sort (C.Type t')),ugraph1
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
@@ -1579,9 +1644,19 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 
        in
 	 (C.Prod (n,s,type2)),ugraph2
-   | C.LetIn (n,s,t) ->
+   | C.LetIn (n,s,ty,t) ->
       (* only to check if s is well-typed *)
-      let ty,ugraph1 = type_of_aux ~logger context s ugraph in
+      let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+      let b,ugraph1 =
+       R.are_convertible ~subst ~metasenv context ty ty' ugraph1
+      in 
+       if not b then
+        raise 
+         (TypeCheckerFailure 
+           (lazy (sprintf
+             "The type of %s is %s but it is expected to be %s" 
+               (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
+       else
        (* The type of a LetIn is a LetIn. Extremely slow since the computed
           LetIn is later reduced and maybe also re-checked.
        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
@@ -1596,7 +1671,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           Moreover the inferred type is closer to the expected one. *)
        let ty1,ugraph2 = 
 	 type_of_aux ~logger 
-	   ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 
+	   ((Some (n,(C.Def (s,ty))))::context) t ugraph1 
        in
        (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
    | C.Appl (he::tl) when List.length tl > 0 ->
@@ -1605,7 +1680,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 List.fold_right (
 	   fun x (l,ugraph) -> 
 	     let ty,ugraph1 = type_of_aux ~logger context x ugraph in
-	     let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
+	     (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
 	       ((x,ty)::l,ugraph1)) 
 	   tl ([],ugraph1) 
        in
@@ -1765,21 +1840,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       in
 	if not b then
         raise
-          (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed")));
+          (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
         (* let's check if the type of branches are right *)
-      let parsno =
+      let parsno,constructorsno =
         let obj,_ =
           try
             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
           with Not_found -> assert false
         in
         match obj with
-            C.InductiveDefinition (_,_,parsno,_) -> parsno
+            C.InductiveDefinition (il,_,parsno,_) ->
+             let _,_,_,cl =
+              try List.nth il i with Failure _ -> assert false
+             in
+              parsno, List.length cl
           | _ ->
               raise (TypeCheckerFailure
                 (lazy ("Unknown mutual inductive definition:" ^
                   UriManager.string_of_uri uri)))
-	in
+      in
+      if List.length pl <> constructorsno then
+       raise (TypeCheckerFailure
+        (lazy ("Wrong number of cases in case analysis"))) ;
       let (_,branches_ok,ugraph5) =
         List.fold_left
           (fun (j,b,ugraph) p ->
@@ -1831,16 +1913,14 @@ end;
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->
-      let types_times_kl,ugraph1 =
-	(* WAS: list rev list map *)
+      let types,kl,ugraph1,len =
         List.fold_left
-          (fun (l,ugraph) (n,k,ty,_) ->
+          (fun (types,kl,ugraph,len) (n,k,ty,_) ->
             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
-            ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
-	  ) ([],ugraph) fl
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              k::kl,ugraph1,len+1)
+	  ) ([],[],ugraph,0) fl
       in
-      let (types,kl) = List.split types_times_kl in
-      let len = List.length types in
       let ugraph2 = 
 	List.fold_left
           (fun ugraph (name,x,ty,bo) ->
@@ -1874,15 +1954,15 @@ end;
       let (_,_,ty,_) = List.nth fl i in
 	ty,ugraph2
    | C.CoFix (i,fl) ->
-       let types,ugraph1 =
+       let types,ugraph1,len =
 	 List.fold_left
-	   (fun (l,ugraph) (n,ty,_) -> 
+	   (fun (l,ugraph,len) (n,ty,_) -> 
               let _,ugraph1 = 
 		type_of_aux ~logger context ty ugraph in 
-		(Some (C.Name n,(C.Decl ty))::l,ugraph1)
-	   ) ([],ugraph) fl
+		(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+                 ugraph1,len+1)
+	   ) ([],ugraph,0) fl
        in
-       let len = List.length types in
        let ugraph2 = 
 	 List.fold_left
            (fun ugraph (_,ty,bo) ->
@@ -1962,9 +2042,12 @@ end;
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-       let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-       C.Sort (C.Type t'),ugraph2
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.Type t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
@@ -1985,6 +2068,8 @@ end;
 	 (match (CicReduction.whd ~subst context hetype) with 
               Cic.Prod (n,s,t) ->
 		let b,ugraph1 = 
+(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then(
+prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*)
 		  CicReduction.are_convertible 
 		    ~subst ~metasenv context hety s ugraph 
 		in	
@@ -2118,6 +2203,9 @@ let typecheck_obj0 ~logger uri ugraph =
       let _,ugraph = type_of ~logger ty ugraph in
        ugraph
    | C.CurrentProof (_,conjs,te,ty,_,_) ->
+      (* this block is broken since the metasenv should 
+       * be topologically sorted before typing metas *)
+      ignore(assert false);
       let _,ugraph =
        List.fold_left
         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -2219,3 +2307,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
   ~logger:(new CicLogger.logger) [] uri i true
   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
   CicUniv.empty_ugraph)
+;;
+
+Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;