WHY WHY WHY do Pulse functions with functional types no longer typecheck?

This commit gives one example of cumbersome workaround, which I have by far
not replicated yet.

Author: tahina-pro

src/lowparse/pulse/LowParse.Pulse.Combinators.fst

@@ -1939,8 +1939,9 @@ let leaf_compute_remaining_size_dtuple2
       (leaf_compute_remaining_size_dtuple2_body w2)
     )
 
+// FIXME: WHY WHY WHY do my Pulse functions with functional types no longer typecheck? WHY WHY WHY do I need to expand the definition of the functional type in Pulse as below? In most cases this will be awfully painful!
 inline_for_extraction
-fn zero_copy_parse_dtuple2
+fn zero_copy_parse_dtuple2'
   (#tl1 #tl2 #th1: Type)
   (#th2: th1 -> Type)
   (#vmatch1: tl1 -> th1 -> slprop)
@@ -1955,10 +1956,17 @@ fn zero_copy_parse_dtuple2
   (#p2: (x: th1) -> parser k2 (th2 x))
   (#s2: (x: th1) -> serializer (p2 x))
   (w2: (xh: Ghost.erased th1) -> zero_copy_parse (vmatch2 xh) (s2 xh))
-: zero_copy_parse #(tl1 `cpair` tl2) #(dtuple2 th1 th2) (vmatch_dep_prod vmatch1 vmatch2) #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
-= (input: _)
-  (#pm: _)
-  (#v: _)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (dtuple2 th1 th2))
+requires
+  pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v
+returns res: (tl1 `cpair` tl2)
+ensures
+  vmatch_dep_prod vmatch1 vmatch2 res v **
+  Trade.trade
+    (vmatch_dep_prod vmatch1 vmatch2 res v)
+    (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
 {
   let (input1, input2) = split_dtuple2 s1 j1 s2 input;
   unfold (split_dtuple2_post s1 s2 input pm v (input1, input2));
@@ -1976,6 +1984,25 @@ fn zero_copy_parse_dtuple2
   res
 }
 
+inline_for_extraction
+let zero_copy_parse_dtuple2
+  (#tl1 #tl2 #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch1: tl1 -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (j1: jumper p1)
+  (w1: zero_copy_parse vmatch1 s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#vmatch2: (x: th1) -> tl2 -> th2 x -> slprop)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh: Ghost.erased th1) -> zero_copy_parse (vmatch2 xh) (s2 xh))
+: zero_copy_parse #(tl1 `cpair` tl2) #(dtuple2 th1 th2) (vmatch_dep_prod vmatch1 vmatch2) #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= zero_copy_parse_dtuple2' j1 w1 sq w2
+
 inline_for_extraction
 fn read_and_zero_copy_parse_dtuple2
   (#tl #th1: Type)