fixing a regression revealed in MonotoneMap

src/ocaml-output/FStar_TypeChecker_TcTerm.ml

@@ -4708,36 +4708,39 @@ in (match (uu____9176) with
 | (t, args) -> begin
 (
 
-let uu____9204 = (FStar_Syntax_Util.arrow_formals_comp t)
-in (match (uu____9204) with
+let t = (FStar_TypeChecker_Normalize.normalize ((FStar_TypeChecker_Normalize.UnfoldUntil (FStar_Syntax_Syntax.Delta_constant))::[]) env t)
+in (
+
+let uu____9205 = (FStar_Syntax_Util.arrow_formals_comp t)
+in (match (uu____9205) with
 | (bs, res) -> begin
 (
 
-let res = (FStar_TypeChecker_Normalize.normalize ((FStar_TypeChecker_Normalize.UnfoldUntil (FStar_Syntax_Syntax.Delta_constant))::[]) env (FStar_Syntax_Util.comp_result res))
+let res = (FStar_Syntax_Util.comp_result res)
 in (match (((FStar_List.length bs) = (FStar_List.length args))) with
 | true -> begin
 (
 
 let subst = (FStar_Syntax_Util.subst_of_list bs args)
 in (FStar_Syntax_Subst.subst subst res))
 end
-| uu____9234 -> begin
+| uu____9237 -> begin
 (let _0_604 = (FStar_Syntax_Print.term_to_string res)
 in (level_of_type_fail env e _0_604))
 end))
-end))
+end)))
 end)))
 end
-| FStar_Syntax_Syntax.Tm_match (uu____9237, (hd)::uu____9239) -> begin
+| FStar_Syntax_Syntax.Tm_match (uu____9240, (hd)::uu____9242) -> begin
 (
 
-let uu____9286 = (FStar_Syntax_Subst.open_branch hd)
-in (match (uu____9286) with
-| (uu____9289, uu____9290, hd) -> begin
+let uu____9289 = (FStar_Syntax_Subst.open_branch hd)
+in (match (uu____9289) with
+| (uu____9292, uu____9293, hd) -> begin
 (universe_of_aux env hd)
 end))
 end
-| FStar_Syntax_Syntax.Tm_match (uu____9306, []) -> begin
+| FStar_Syntax_Syntax.Tm_match (uu____9309, []) -> begin
 (level_of_type_fail env e "empty match cases")
 end)))
 

src/typechecker/FStar.TypeChecker.TcTerm.fs

@@ -1940,8 +1940,9 @@ let rec universe_of_aux env e =
           t, args
      in
      let t, args = type_of_head true hd args in
+     let t = N.normalize [N.UnfoldUntil Delta_constant] env t in
      let bs, res = U.arrow_formals_comp t in
-     let res = N.normalize [N.UnfoldUntil Delta_constant] env (U.comp_result res) in
+     let res = U.comp_result res in
      if List.length bs = List.length args
      then let subst = U.subst_of_list bs args in
           SS.subst subst res