Add eta-expansion as a coercion.

FStarLang · Jan 13, 2025 · 3617cf6 · 3617cf6
1 parent abd7d4e
commit 3617cf6
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fsti b/src/typechecker/FStarC.TypeChecker.Rel.fsti
@@ -52,6 +52,9 @@ val head_matches_delta (env:env) (logical:bool) (smt_ok:bool) (t1 t2:typ) : (mat
 val may_relate_with_logical_guard (env:env) (is_equality:bool) (head:typ) : bool
 val guard_to_string           : env -> guard_t -> string
 val simplify_guard            : env -> guard_t -> guard_t
+
+val maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term
+
 val solve_deferred_constraints: env -> guard_t -> guard_t
 val solve_non_tactic_deferred_constraints: maybe_defer_flex_flex:bool -> env -> guard_t -> guard_t
 

diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst
@@ -2572,6 +2572,15 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_
               BU.print1 "(%s) No user coercion found\n"
                       (Range.string_of_range e.pos)
       in
+
+      match 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');
+        // FIXME: do we need to type-check this again?
+        e', { lc with res_typ = exp_t }, Env.trivial_guard
+
+      | None ->
 
       (* TODO: hide/reveal also user coercions? it's trickier for sure *)