diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 2ec0f58d8..2926e6d0b 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -407,6 +407,18 @@ struct
       (* in *)
       F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange))
 
+  and fun_application ~span f args generic_args =
+    let generic_args =
+      generic_args
+      |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
+      |> List.map ~f:(function
+           | GConst const -> (pexpr const, F.AST.Nothing)
+           | GLifetime _ -> .
+           | GType ty -> (pty span ty, F.AST.Hash))
+    in
+    let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
+    F.mk_app f (generic_args @ args)
+
   and pexpr_unwrapped (e : expr) =
     match e.e with
     | Literal l -> pliteral_as_expr e.span l
@@ -452,16 +464,7 @@ struct
                 chars: '" ^ s ^ "'");
         F.AST.Const (F.Const.Const_int (s, None)) |> F.term
     | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
-        let generic_args =
-          generic_args
-          |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
-          |> List.map ~f:(function
-               | GConst const -> (pexpr const, F.AST.Nothing)
-               | GLifetime _ -> .
-               | GType ty -> (pty e.span ty, F.AST.Hash))
-        in
-        let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
-        F.mk_app (pexpr f) (generic_args @ args)
+        fun_application ~span:e.span (pexpr f) args generic_args
     | If { cond; then_; else_ } ->
         F.term
         @@ F.AST.If
@@ -1156,7 +1159,7 @@ struct
     | Trait { name; generics; items } ->
         let bds =
           List.map
-            ~f:FStarBinder.(of_generic_param ~kind:Explicit e.span >> to_binder)
+            ~f:FStarBinder.(of_generic_param e.span >> to_binder)
             generics.params
         in
         let name_str = U.Concrete_ident_view.to_definition_name name in
@@ -1293,9 +1296,9 @@ struct
           @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics)
         in
         let typ =
-          F.mk_e_app
+          fun_application ~span:e.span
             (F.term @@ F.AST.Name (pglobal_ident e.span trait))
-            (List.map ~f:(pgeneric_value e.span) generic_args)
+            [] generic_args
         in
         let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in
         let fields =
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index eda0b67cf..d49db0fb5 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
   else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
+let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index #(t_Array v_T (sz 10)) #t_SafeIndex =
   {
     f_Output = v_T;
     f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
@@ -79,7 +79,7 @@ open FStar.Mul
 type t_Foo = | Foo : u8 -> t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
+let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
   {
     f_Output = t_Foo;
     f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8));
@@ -88,7 +88,7 @@ let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
   }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
+let impl_1: Core.Ops.Arith.t_Mul #t_Foo #t_Foo =
   {
     f_Output = t_Foo;
     f_mul_pre
@@ -131,7 +131,7 @@ let mutation_example
   (t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Index.t_Index t_MyArray usize =
+let impl: Core.Ops.Index.t_Index #t_MyArray #usize =
   {
     f_Output = u8;
     f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX);
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index db8f3cd46..33d524da6 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -48,7 +48,7 @@ open FStar.Mul
 let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
   ()
 
-class t_Foo (v_Self: Type0) = {
+class t_Foo (#v_Self: Type0) = {
   f_const_add_pre:v_N: usize -> v_Self -> bool;
   f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
   f_const_add:v_N: usize -> x0: v_Self
@@ -56,7 +56,7 @@ class t_Foo (v_Self: Type0) = {
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_usize: t_Foo usize =
+let impl_Foo_for_usize: t_Foo #usize =
   {
     f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
     f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index a4ce27894..39e2269d3 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -32,7 +32,7 @@ module Include_flag
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 /// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
@@ -76,7 +76,7 @@ let main_c (_: Prims.unit) : Prims.unit =
 type t_Foo = | Foo : t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
+let impl_Trait_for_Foo: t_Trait #t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index b3a95740d..e4173e16e 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -54,7 +54,7 @@ type t_Bar = | Bar : t_Bar
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Convert.t_From t_Bar Prims.unit =
+let impl: Core.Convert.t_From #t_Bar #Prims.unit =
   {
     f_from_pre = (fun ((): Prims.unit) -> true);
     f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true);
@@ -65,7 +65,7 @@ val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
 /// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Convert.t_From t_Bar u8 =
+let impl_1: Core.Convert.t_From #t_Bar #u8 =
   {
     f_from_pre = (fun (x: u8) -> true);
     f_from_post = (fun (x: u8) (out: t_Bar) -> true);
diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
index 76f5002cd..d01460536 100644
--- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap	
@@ -32,7 +32,7 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-class t_FooTrait (v_Self: Type0) = {
+class t_FooTrait (#v_Self: Type0) = {
   f_z_pre:v_Self -> bool;
   f_z_post:v_Self -> v_Self -> bool;
   f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
@@ -173,7 +173,7 @@ type t_Bar = {
 type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
+let impl_FooTrait_for_Foo: t_FooTrait #t_Foo =
   {
     f_z_pre = (fun (self: t_Foo) -> true);
     f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index 68c009f19..9162f2abc 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -108,22 +108,22 @@ type t_Foo2 =
   | Foo2_A : t_Foo2
   | Foo2_B { f_x:usize }: t_Foo2
 
-class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+class t_FooTrait (#v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
-class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
+class t_T1 (#v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
+let impl_T1_for_Foo: t_T1 #t_Foo = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
+let impl_T1_for_tuple_Foo_u8: t_T1 #(t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
+class t_T2_for_a (#v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
 
-class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
+class t_T3_e_for_a (#v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
+let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a #t_Foo = { __marker_trait = () }
 
 let v_INHERENT_CONSTANT: usize = sz 3
 
@@ -146,7 +146,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
+let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a #(t_Arity1 (t_Foo & u8)) =
   { __marker_trait = () }
 
 type t_B = | B : t_B
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 8047ce566..36079953d 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -32,13 +32,13 @@ module Traits.For_clauses.Issue_495_.Minimized_3_
 open Core
 open FStar.Mul
 
-class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl
       (#v_P: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8)
-    : t_Trait v_P = { __marker_trait = () }
+    : t_Trait #v_P = { __marker_trait = () }
 '''
 "Traits.For_clauses.Issue_495_.fst" = '''
 module Traits.For_clauses.Issue_495_
@@ -105,7 +105,7 @@ module Traits.For_clauses
 open Core
 open FStar.Mul
 
-class t_Foo (v_Self: Type0) (v_T: Type0) = {
+class t_Foo (#v_Self: Type0) (#v_T: Type0) = {
   f_to_t_pre:v_Self -> bool;
   f_to_t_post:v_Self -> v_T -> bool;
   f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
@@ -132,7 +132,7 @@ open FStar.Mul
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: Traits.Implicit_dependencies_issue_667_.Trait_definition.t_MyTrait
-Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType =
+#Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType =
   {
     f_my_method_pre
     =
@@ -150,7 +150,7 @@ module Traits.Implicit_dependencies_issue_667_.Trait_definition
 open Core
 open FStar.Mul
 
-class t_MyTrait (v_Self: Type0) = {
+class t_MyTrait (#v_Self: Type0) = {
   f_my_method_pre:v_Self -> bool;
   f_my_method_post:v_Self -> Prims.unit -> bool;
   f_my_method:x0: v_Self
@@ -173,13 +173,80 @@ let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyTy
   Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType
     x
 '''
+"Traits.Interlaced_consts_types.fst" = '''
+module Traits.Interlaced_consts_types
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Foo (#v_Self: Type0) (v_FooConst: usize) (#v_FooType: Type0) = {
+  f_fun_pre:
+      v_FunConst: usize ->
+      #v_FunType: Type0 ->
+      t_Array v_FooType v_FooConst ->
+      t_Array v_FunType v_FunConst
+    -> bool;
+  f_fun_post:
+      v_FunConst: usize ->
+      #v_FunType: Type0 ->
+      t_Array v_FooType v_FooConst ->
+      t_Array v_FunType v_FunConst ->
+      Prims.unit
+    -> bool;
+  f_fun:
+      v_FunConst: usize ->
+      #v_FunType: Type0 ->
+      x0: t_Array v_FooType v_FooConst ->
+      x1: t_Array v_FunType v_FunConst
+    -> Prims.Pure Prims.unit
+        (f_fun_pre v_FunConst v_FunType x0 x1)
+        (fun result -> f_fun_post v_FunConst v_FunType x0 x1 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0)
+    : t_Foo #v_SelfType v_FooConst #v_FooType =
+  {
+    f_fun_pre
+    =
+    (fun
+        (v_FunConst: usize)
+        (#v_FunType: Type0)
+        (x: t_Array v_FooType v_FooConst)
+        (y: t_Array v_FunType v_FunConst)
+        ->
+        true);
+    f_fun_post
+    =
+    (fun
+        (v_FunConst: usize)
+        (#v_FunType: Type0)
+        (x: t_Array v_FooType v_FooConst)
+        (y: t_Array v_FunType v_FunConst)
+        (out: Prims.unit)
+        ->
+        true);
+    f_fun
+    =
+    fun
+      (v_FunConst: usize)
+      (#v_FunType: Type0)
+      (x: t_Array v_FooType v_FooConst)
+      (y: t_Array v_FunType v_FunConst)
+      ->
+      ()
+  }
+
+type t_Bar (v_FooConst: usize) (v_FooType: Type0) =
+  | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType
+'''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''
 module Traits.Unconstrainted_types_issue_677_
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
 open Core
 open FStar.Mul
 
-class t_PolyOp (v_Self: Type0) = {
+class t_PolyOp (#v_Self: Type0) = {
   f_op_pre:u32 -> u32 -> bool;
   f_op_post:u32 -> u32 -> u32 -> bool;
   f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result)
@@ -191,7 +258,7 @@ let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp
 type t_Plus = | Plus : t_Plus
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: t_PolyOp t_Plus =
+let impl: t_PolyOp #t_Plus =
   {
     f_op_pre = (fun (x: u32) (y: u32) -> true);
     f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true);
@@ -201,7 +268,7 @@ let impl: t_PolyOp t_Plus =
 type t_Times = | Times : t_Times
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: t_PolyOp t_Times =
+let impl_1: t_PolyOp #t_Times =
   {
     f_op_pre = (fun (x: u32) (y: u32) -> true);
     f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true);
@@ -216,7 +283,7 @@ module Traits
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type0) = {
+class t_Bar (#v_Self: Type0) = {
   f_bar_pre:v_Self -> bool;
   f_bar_post:v_Self -> Prims.unit -> bool;
   f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result)
@@ -234,7 +301,7 @@ let impl__Error__for_application_callback (_: Prims.unit) :  Prims.unit -> t_Err
 
 let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail  -> isz 0
 
-class t_Lang (v_Self: Type0) = {
+class t_Lang (#v_Self: Type0) = {
   f_Var:Type0;
   f_s_pre:v_Self -> i32 -> bool;
   f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> bool;
@@ -242,7 +309,7 @@ class t_Lang (v_Self: Type0) = {
     -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result)
 }
 
-class t_SuperTrait (v_Self: Type0) = {
+class t_SuperTrait (#v_Self: Type0) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> bool;
   f_function_of_super_trait_post:v_Self -> u32 -> bool;
@@ -253,7 +320,7 @@ class t_SuperTrait (v_Self: Type0) = {
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_SuperTrait_for_i32: t_SuperTrait i32 =
+let impl_SuperTrait_for_i32: t_SuperTrait #i32 =
   {
     _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve;
     f_function_of_super_trait_pre = (fun (self: i32) -> true);
@@ -261,7 +328,7 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
   }
 
-class t_Foo (v_Self: Type0) = {
+class t_Foo (#v_Self: Type0) = {
   f_AssocType:Type0;
   f_AssocType_17663802186765685673:t_SuperTrait f_AssocType;
   f_AssocType_10139459042277121690:Core.Clone.t_Clone f_AssocType;
@@ -312,7 +379,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
     : u32 = f_function_of_super_trait #i1.f_AssocType x
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_tuple_: t_Foo Prims.unit =
+let impl_Foo_for_tuple_: t_Foo #Prims.unit =
   {
     f_AssocType = i32;
     f_AssocType_17663802186765685673 = FStar.Tactics.Typeclasses.solve;
diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
index 9821c42d0..1d01124ef 100644
--- a/tests/traits/src/lib.rs
+++ b/tests/traits/src/lib.rs
@@ -163,3 +163,16 @@ mod implicit_dependencies_issue_667 {
         }
     }
 }
+
+// Related to issue 719
+mod interlaced_consts_types {
+    struct Bar<const FooConst: usize, FooType>([FooType; FooConst]);
+
+    trait Foo<const FooConst: usize, FooType> {
+        fn fun<const FunConst: usize, FunType>(x: [FooType; FooConst], y: [FunType; FunConst]);
+    }
+
+    impl<const FooConst: usize, FooType, SelfType> Foo<FooConst, FooType> for SelfType {
+        fn fun<const FunConst: usize, FunType>(x: [FooType; FooConst], y: [FunType; FunConst]) {}
+    }
+}