Dependent type issue with rewrite in CapAsm backend

[argsv]

When trying to prove the goal

Goal (* (forall y, exists off, find_symbol_offset y = Some off) -> *)
     (forall (T : Type) (zs : list T), list_length_z zs = 1) ->
     (Archi.ptr64 = true) ->
     exists x, OK x = transf_program test_program_1.
Proof.

after unfolding and simplifying several function definitions, at some point the context looks like this

H: forall (T : Type) (zs : list T), list_length_z zs = 1
G: Archi.ptr64 = true
--------------------------------------------------------------------
1/1
exists x : program,
  OK x =
  match
    match
      (do f' <-
       (do tf <-
        (do c <-
         (do c2 <-
          OK
            (indexed_memory_access_stack_ofs
               (if Archi.ptr64
                then
                 fun (i r : ireg) (o : offset) => PCUld X1 i r o false false
                else
                 fun (i r : ireg) (o : offset) => PCUlw X1 i r o false false)
               Ptrofs.zero ++
             indexed_memory_access_stack_ofs
               (if Archi.ptr64
                then
                 fun (i r : ireg) (o : offset) => PCUld X3 i r o false false
                else
                 fun (i r : ireg) (o : offset) => PCUlw X3 i r o false false)
               Ptrofs.zero ++
             make_return
               {|
                 ac_nextlabel := 1;
                 ac_code := nil;
                 ac_call_site_count := Ptrofs.zero
               |});

<many many more lines omitted>

Then, when I try rewrite G (or destruct Archi.ptr64), I get the error

Error: abstracting over the term `Archi.ptr64` leads to a term
<many lines omitted>
which is ill typed.
Reason is: illegal application:
The term "agr_comps_transf_partial" of type
 "forall (A B V W : Type) (CA : has_comp A) (CB : has_comp B)
    (transf_fun : ident -> A -> res B),
  (forall id : ident, has_comp_transl_partial (transf_fun id)) ->
  forall (transf_var : ident -> V -> res W) (pol : Policy.t)
    (defs : list (ident * globdef A V)),
  agr_comps pol defs ->
  forall defs' : list (ident * globdef B W),
  transf_globdefs transf_fun transf_var defs = OK defs' ->
  agr_comps pol defs'"
cannot be applied to the terms
<many lines omitted>
which should be coercible to
<many lines omitted>

Note that I shortened the error message to the "essential" parts, since it is almost 3000 lines long. You can reproduce the issue on this commit 2c3bd7c by interactively running CapAsmgen.v up to line 2318 and then adding rewrite G.

Unfortunately, I neither understand the error/problem nor have any idea how to fix it.