- let metasenv, subst, he, ty_he =
- typeof_aux metasenv subst context None he in
- let metasenv, subst, t, ty =
- eat_prods rdb ~localise force_ty metasenv subst context expty t
- orig_he he ty_he args in
- let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
- metasenv, subst, t, ty
+ let hbr t =
+ if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t
+ in
+ let refine_appl () =
+ let metasenv, subst, he, ty_he =
+ typeof_aux metasenv subst context None he in
+ let metasenv, subst, t, ty =
+ eat_prods rdb ~localise force_ty metasenv subst context expty t
+ orig_he he ty_he args in
+ metasenv, subst, hbr t, ty
+ in
+ if args = [C.Implicit `Vector] && expty <> None then
+ (* we try here to expand the vector a 0 implicits, but we use
+ * the expected type *)
+ try
+ let metasenv, subst, he, ty_he =
+ typeof_aux metasenv subst context expty he in
+ metasenv, subst, hbr he, ty_he
+ with Uncertain _ | RefineFailure _ -> refine_appl ()
+ else refine_appl ()