Disable eta-expansion in MLish

FStarLang · Jan 10, 2025 · 5f77e2b · 5f77e2b
1 parent 61f8b5e
commit 5f77e2b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst
@@ -2997,6 +2997,8 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term)
           S.mk_Tm_app rhs_hd rhs_args rhs.pos
         in
         let rhs =
+          // eta-expand functions for effect promotion, unless we're in --MLish
+          if Options.ml_ish () then rhs else
           let env = { env with admit=true; expected_typ=None } in
           let t_u, _ =
             let Flex (lhs, _, _) = lhs in

diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst
@@ -2573,7 +2573,8 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_
                       (Range.string_of_range e.pos)
       in
 
-      match maybe_eta_expand_fun env e lc.res_typ exp_t with
+      // eta-expand functions for effect promotion, unless we're in --MLish
+      match if Options.ml_ish () then None else maybe_eta_expand_fun env e lc.res_typ exp_t with
       | Some e' ->
         if !dbg_Coercions then
           BU.print3 "(%s) Eta-expansion coercion from %s to %s" (Range.string_of_range e.pos) (show e) (show e');