some docs

FStarLang · May 13, 2021 · 2686888 · 2686888
1 parent 34830b7
commit 2686888
Show file tree

Hide file tree

Showing 3 changed files with 94 additions and 126 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -24,6 +24,20 @@ Guidelines for the changelog:
   * Friend modules (https://github.com/FStarLang/FStar/wiki/Friend-modules)
 
 ## Core typechecker
+
+  * F* no longer supports eta equivalence. Dominique Unruh observed
+    that the primitive `pointwise` tactic (which treats provable
+    equality as a congruence) allows proving functional
+    extensionality, which is unsound in conjunction with subtyping in
+    F*. It turns out that a crucial step in that unsoundness proof is
+    the use of eta equivalence (See Bug1966a.fst for a proof of that,
+    with thanks due there also to Catalin Hritcu). As a fix, we
+    removed eta equivalence. As a result, functional extensionality is
+    now a theorem in F\*, no longer an axiom, which is an
+    improvement. The removal of eta equivalence introduced regressions
+    in some proofs that were implicitly relying on it. See, for
+    example, https://github.com/project-everest/hacl-star/pull/442
+
   * PR https://github.com/FStarLang/FStar/pull/2256 adds support for Coq-style
     dependent pattern matching. F* now supports `match e returns C with |...`
     syntax for typechecking the branches with `C` appropriately substituted.

diff --git a/src/ocaml-output/FStar_TypeChecker_Rel.ml b/src/ocaml-output/FStar_TypeChecker_Rel.ml
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fs b/src/typechecker/FStar.TypeChecker.Rel.fs
@@ -2253,18 +2253,24 @@ and solve_t_flex_rigid_eq env (orig:prob) wl
                           Syntax.order_bv
     in
 
+    (*
+       mk_solution takes care to not introduce needless eta expansions
+
+       lhs is of the form `?u bs`
+       Abstractly, the goal is to set `?u := fun bs -> rhs`
+
+       But, this is optimized so that in case `rhs` is say `e bs`,
+       where `bs` does not appear free in `e`,
+       then we set `?u := e`.
+
+       This is important since eta equivalence is not validated by F*.
+
+       So, introduce needless eta expansions here would lead to unification
+       failures elsewhere
+    *)
     let mk_solution env (lhs:flex_t) (bs:binders) (rhs:term) =
-        let debug f =
-          if Env.debug env <| Options.Other "ETA"
-          then f()
-        in
         let bs_orig = bs in
         let rhs_orig = rhs in
-        debug (fun () ->
-                 BU.print3 "mk_solution::\n\tlhs=%s\n\trhs=%s\n\tbinders=%s\n"
-                       (flex_t_to_string lhs)
-                       (Print.term_to_string rhs)
-                       (Print.binders_to_string ", " bs));
         let (Flex (_, ctx_u, args)) = lhs in
         let bs, rhs =
           let bv_not_free_in_arg x arg =
@@ -2289,10 +2295,6 @@ and solve_t_flex_rigid_eq env (orig:prob) wl
                 lhs_binders, rhs_args
           in
           let rhs_hd, rhs_args = U.head_and_args rhs in
-          debug (fun () ->
-                   BU.print2 "remove_matching_prefix::\n\tlhs=%s\n\trhs=%s\n"
-                              (Print.args_to_string  (List.rev args))
-                              (Print.args_to_string  (List.rev rhs_args)));
           let bs, rhs_args =
             remove_matching_prefix
               (List.rev bs_orig)
@@ -2308,12 +2310,6 @@ and solve_t_flex_rigid_eq env (orig:prob) wl
           | _ ->
             u_abs ctx_u.ctx_uvar_typ (sn_binders env bs) rhs
         in
-        debug (fun () ->
-                 BU.print2 "mk_solution:: Optimized solution\n\tfrom %s\n\tto %s\n"
-                                  (let default_sol = u_abs ctx_u.ctx_uvar_typ (sn_binders env bs_orig) rhs_orig in
-                                   Print.term_to_string default_sol)
-                                  (Print.term_to_string sol));
-
         [TERM(ctx_u, sol)]
     in