feat: turn type aliases extraction off by default

Fixes #708

cli/options/src/lib.rs

@@ -313,6 +313,16 @@ pub struct BackendOptions {
     #[arg(short, long = "debug-engine")]
     pub debug_engine: Option<DebugEngineMode>,
 
+    /// Extract type aliases. This is disabled by default, since
+    /// extracted terms depends on expanded types rather than on type
+    /// aliases. Turning this option on is discouraged: Rust type
+    /// synonyms can ommit generic bounds, which are ususally
+    /// necessary in the hax backends, leading to typechecking
+    /// errors. For more details see
+    /// https://github.com/hacspec/hax/issues/708.
+    #[arg(long)]
+    pub extract_type_aliases: bool,
+
     #[command(flatten)]
     pub translation_options: TranslationOptions,
 }

engine/bin/lib.ml

@@ -94,6 +94,13 @@ let run (options : Types.engine_options) : Types.output =
       options.backend.translation_options.include_namespaces
     in
     let items = import_thir_items include_clauses options.input in
+    let items =
+      if options.backend.extract_type_aliases then items
+      else
+        List.filter
+          ~f:(function { v = TyAlias _; _ } -> false | _ -> true)
+          items
+    in
     Logs.info (fun m ->
         m "Applying phase for backend %s"
           ([%show: Diagnostics.Backend.t] M.backend));

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -181,12 +181,6 @@ open FStar.Mul
 
 type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} =
   | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T
-
-unfold
-let t_SynonymA (#v_T: Type0) = t_StructWithGenericBounds v_T
-
-unfold
-let t_SynonymB (#v_T: Type0) = t_StructWithGenericBounds (v_T & v_T)
 '''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''
 module Traits.Unconstrainted_types_issue_677_