- let lty = NCicSubstitution.subst_meta lc ty in
- pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
- ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t);
- let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
+ let metasenv, subst, t =
+ match ty with
+ | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
+ | _ ->
+ pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+ let t, ty_t =
+ try t, NCicTypeChecker.typeof ~subst ~metasenv context t
+ with NCicTypeChecker.TypeCheckerFailure _ ->
+ let ft = fix_sorts t in
+ if ft == t then assert false else
+ try
+ pp (lazy ("typeof: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ft));
+ ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
+ with NCicTypeChecker.TypeCheckerFailure msg ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
+ prerr_endline (Lazy.force msg);
+ assert false
+ in
+ let lty = NCicSubstitution.subst_meta lc ty in
+ pp (lazy("On the types: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+ ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
+ let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
+ metasenv, subst, t
+ in