Merge pull request #947 from hacspec/no-default-params-traits

fix(exporter+engine): drop default parameters on traits
hacspec · Oct 2, 2024 · f8124b7 · f8124b7
2 parents 39a2f0a + 3c3bddd
commit f8124b7
Show file tree

Hide file tree

Showing 12 changed files with 43 additions and 26 deletions.
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -362,10 +362,8 @@ struct
 
   let pgeneric_param_as_argument span : generic_param -> C.AST.argument =
     function
-    | { ident; kind = GPType { default }; _ } ->
-        C.AST.Explicit
-          ( C.AST.Ident ident.name,
-            match default with Some t -> pty span t | None -> C.AST.WildTy )
+    | { ident; kind = GPType; _ } ->
+        C.AST.Explicit (C.AST.Ident ident.name, C.AST.WildTy)
     | _ -> Error.unimplemented ~details:"Coq: TODO: generic_params" span
 
   let rec pitem (e : item) : C.AST.decl list =

diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -1322,11 +1322,10 @@ struct
         SSP.AST.Implicit
           ( SSP.AST.Ident (plocal_ident ident),
             match kind with
-            | GPType { default = Some t } -> pty span t
             | GPConst { typ = t } ->
                 SSPExtraDefinitions.wrap_type_in_both "(fset [])" "(fset [])"
                   (pty span t)
-            | GPType { default = None } -> SSP.AST.WildTy
+            | GPType -> SSP.AST.WildTy
             | _ -> . )
 
   let pgeneric_constraints_as_argument span :

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -675,7 +675,7 @@ struct
       let ident = plocal_ident p.ident in
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
-      | GPType { default = _ } -> { kind = Implicit; typ = F.type0_term; ident }
+      | GPType -> { kind = Implicit; typ = F.type0_term; ident }
       | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =

diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -365,7 +365,7 @@ functor
 
     and generic_param_kind =
       | GPLifetime of { witness : F.lifetime }
-      | GPType of { default : ty option }
+      | GPType
       | GPConst of { typ : ty }
 
     and generic_constraint =

diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
@@ -415,10 +415,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
             let suffix =
               match kind with
               | GPLifetime _ -> space ^^ colon ^^ space ^^ string "'unk"
-              | GPType { default = None } -> empty
-              | GPType { default = Some default } ->
-                  space ^^ equals ^^ space
-                  ^^ print#ty_at GenericParam_GPType default
+              | GPType -> empty
               | GPConst { typ } ->
                   space ^^ colon ^^ space
                   ^^ print#ty_at GenericParam_GPConst typ

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1182,9 +1182,7 @@ end) : EXPR = struct
     let kind =
       match (param.kind : Thir.generic_param_kind) with
       | Lifetime _ -> GPLifetime { witness = W.lifetime }
-      | Type { default; _ } ->
-          let default = Option.map ~f:(c_ty param.span) default in
-          GPType { default }
+      | Type _ -> GPType
       (* Rustc always fills in const generics on use. Thus we can drop this information. *)
       | Const { default = _; ty } -> GPConst { typ = c_ty param.span ty }
     in
@@ -1334,7 +1332,7 @@ let generic_param_to_value ({ ident; kind; span; _ } : generic_param) :
   match kind with
   | GPLifetime { witness } ->
       GLifetime { lt = [%show: local_ident] ident; witness }
-  | GPType _ -> GType (TParam ident)
+  | GPType -> GType (TParam ident)
   | GPConst { typ } -> GConst { e = LocalVar ident; typ; span }
 
 type discriminant_expr =
@@ -1591,8 +1589,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
         let self =
           let id = Local_ident.mk_id Typ 0 (* todo *) in
           let ident = Local_ident.{ name = "Self"; id } in
-          let kind = GPType { default = None } in
-          { ident; span; attrs = []; kind }
+          { ident; span; attrs = []; kind = GPType }
         in
         let params = self :: params in
         let generics = { params; constraints } in

diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml
@@ -138,8 +138,7 @@ struct
       let* kind =
         match kind with
         | GPLifetime _ -> None
-        | GPType { default } ->
-            Some (B.GPType { default = Option.map ~f:(dty span) default })
+        | GPType -> Some B.GPType
         | GPConst { typ } -> Some (B.GPConst { typ = dty span typ })
       in
       Some B.{ ident; kind; attrs; span }

diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml
@@ -391,8 +391,7 @@ module Raw = struct
     let ( ! ) = pure span in
     match pk with
     | GPLifetime _ -> (empty, !": 'unk")
-    | GPType { default = Some default } -> (empty, !" = " & pty span default)
-    | GPType { default = None } -> (empty, empty)
+    | GPType -> (empty, empty)
     | GPConst { typ } -> (!"const ", !":" & pty span typ)
 
   let pgeneric_param (p : generic_param) =

diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
@@ -381,8 +381,7 @@ struct
         match kind with
         | GPLifetime { witness } ->
             B.GPLifetime { witness = S.lifetime span witness }
-        | GPType { default } ->
-            GPType { default = Option.map ~f:(dty span) default }
+        | GPType -> GPType
         | GPConst { typ } -> GPConst { typ = dty span typ }
       in
       { ident; span; kind; attrs }

diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
@@ -2983,8 +2983,16 @@ pub enum GenericParamKind<Body: IsBody> {
         kind: LifetimeParamKind,
     },
     Type {
-        #[map(x.map(|ty| ty.sinto(tcx)))]
-        default: Option<Ty>,
+        /// On use site, Rust always give us all the generic
+        /// parameters, no matter the defaultness. This information is
+        /// thus not so useful. At the same time, as discussed in
+        /// https://github.com/hacspec/hax/issues/310, extracting this
+        /// default type causes failures when querying Rust for trait
+        /// resolution. We thus decided to disable this feature. If
+        /// this default type information is useful to you, please
+        /// open an issue on https://github.com/hacspec/hax.
+        #[map(x.map(|_ty| ()))]
+        default: Option<()>,
         synthetic: bool,
     },
     Const {

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -46,6 +46,19 @@ class t_BlockBackend (v_Self: Type0) = {
     -> Prims.Pure Prims.unit (f_proc_block_pre x0) (fun result -> f_proc_block_post x0 result)
 }
 '''
+"Traits.Default_traits_parameters.fst" = '''
+module Traits.Default_traits_parameters
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
+
+class t_Foo (v_Self: Type0) = {
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_12056653545434731362:t_Bar v_Self f_U;
+  f_U:Type0
+}
+'''
 "Traits.For_clauses.Issue_495_.Minimized_3_.fst" = '''
 module Traits.For_clauses.Issue_495_.Minimized_3_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -281,3 +281,11 @@ mod recursive_trait_with_assoc_type {
         type U;
     }
 }
+
+// issue 310
+mod default_traits_parameters {
+    trait Foo: Bar {
+        type U;
+    }
+    trait Bar<T = <Self as Foo>::U> {}
+}