- let lty = NCicSubstitution.subst_meta lc ty in
- let ty_t =
- try NCicTypeChecker.typeof ~subst ~metasenv context t
- with NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
- prerr_endline (Lazy.force msg);
- assert false
+ 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