diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 5897caa03..ba830aace 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -578,10 +578,8 @@ struct
       let ident = plocal_ident p.ident in
       match p.kind with
       | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
-      | GPType { default = None } ->
+      | GPType { default = _ } ->
           { kind; typ = F.term @@ F.AST.Name (F.lid [ "Type" ]); ident }
-      | GPType _ ->
-          Error.unimplemented span ~details:"pgeneric_param:Type with default"
       | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
 
     let of_generic_constraint span (nth : int) (c : generic_constraint) =
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 8c20cdfe9..8555fa751 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1003,9 +1003,8 @@ end) : EXPR = struct
       | Type { default; _ } ->
           let default = Option.map ~f:(c_ty param.span) default in
           GPType { default }
-      | Const { default = Some _; _ } ->
-          unimplemented [ param.span ] "c_generic_param:Const with a default"
-      | Const { default = None; ty } -> GPConst { typ = c_ty param.span ty }
+      (* 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
     let span = Span.of_thir param.span in
     let attrs = c_attrs param.attributes in
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index 64e3362fe..eee521479 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -29,6 +29,16 @@ Compiling generics v0.1.0 (WORKSPACE_ROOT/generics)
 diagnostics = []
 
 [stdout.files]
+"Generics.Defaults_generics.fst" = '''
+module Generics.Defaults_generics
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Defaults (v_T: Type) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_Defaults v_T v_N
+
+let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = ()
+'''
 "Generics.fst" = '''
 module Generics
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index e1fad0d42..610369e3c 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -214,12 +214,6 @@ dependencies = [
  "cfg-if",
 ]
 
-[[package]]
-name = "dyn-clone"
-version = "1.0.14"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "23d2f3407d9a573d666de4b5bdf10569d73ca9478087346697dcbae6244bfbcd"
-
 [[package]]
 name = "either"
 version = "1.9.0"
@@ -300,6 +294,9 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
+dependencies = [
+ "hax-lib-macros",
+]
 
 [[package]]
 name = "hax-lib-macros"
@@ -318,7 +315,6 @@ version = "0.1.0-pre.1"
 dependencies = [
  "proc-macro2",
  "quote",
- "schemars",
  "serde",
  "serde_json",
  "uuid",
@@ -813,30 +809,6 @@ dependencies = [
  "winapi-util",
 ]
 
-[[package]]
-name = "schemars"
-version = "0.8.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1f7b0ce13155372a76ee2e1c5ffba1fe61ede73fbea5630d61eee6fac4929c0c"
-dependencies = [
- "dyn-clone",
- "schemars_derive",
- "serde",
- "serde_json",
-]
-
-[[package]]
-name = "schemars_derive"
-version = "0.8.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e85e2a16b12bdb763244c69ab79363d71db2b4b918a2def53f80b02e0574b13c"
-dependencies = [
- "proc-macro2",
- "quote",
- "serde_derive_internals",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "secret_integers"
 version = "0.1.7"
@@ -862,17 +834,6 @@ dependencies = [
  "syn 1.0.109",
 ]
 
-[[package]]
-name = "serde_derive_internals"
-version = "0.26.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "85bf8229e7920a9f636479437026331ce11aa132b4dde37d121944a44d6e5f3c"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "serde_json"
 version = "1.0.99"
diff --git a/tests/generics/src/lib.rs b/tests/generics/src/lib.rs
index 1f201bbcf..cb14662fd 100644
--- a/tests/generics/src/lib.rs
+++ b/tests/generics/src/lib.rs
@@ -45,3 +45,9 @@ struct Bar;
 impl Bar {
     fn inherent_impl_generics<T, const N: usize>(x: [T; N]) {}
 }
+
+/// Test defaults types and constants
+mod defaults_generics {
+    struct Defaults<T = (), const N: usize = 2>([T; N]);
+    fn f(_: Defaults) {}
+}