- let tyt = type_of_aux' metasenv' subst' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ (try
+ let tyt =
+ type_of_aux' metasenv' subst'' context t
+ in
+ fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
+ with AssertFailure _ ->
+ (* TODO huge hack!!!!
+ * we keep on unifying/refining in the hope that the problem will be
+ * eventually solved. In the meantime we're breaking a big invariant:
+ * the terms that we are unifying are no longer well typed in the
+ * current context (in the worst case we could even diverge)
+ *)
+(*
+prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
+prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
+*)
+ (subst'', metasenv'))