Cannot do per-target type definitions

[emersion]

I ran into this issue while working on rems-project/linksem#9

This PR required to have a Byte_sequence type which maps to the OCaml Byte_sequence_wrapper.byte_sequence for the OCaml target, and to list byte on all other targets. This doesn't seem too hard at first, let's try:

type byte_sequence = list byte
declare ocaml target_rep type byte_sequence = `Byte_sequence_wrapper.byte_sequence`

(* Let's try to add a function *)
val length : byte_sequence -> natural
let length bs = List.length bs
declare ocaml target_rep function length = `Byte_sequence_wrapper.big_num_length`
(* Works! *)

(* Let's try to add another function, which works on all backends, and uses this length function we just defined *)
val do_stuff : byte_sequence -> natural
let do_stuff bs = 1 + (length bs)
(* Lem is happy, but ugh, OCaml isn't
   In fact the generated OCaml function takes a list of bytes as first argument, not our OCaml type *)

Let's try with another strategy:

type byte_sequence
declare coq target_rep type byte_sequence = list byte
(* Same for all other backends except… *)
declare ocaml target_rep type byte_sequence = `Byte_sequence_wrapper.byte_sequence`

val length : byte_sequence -> natural
declare coq target_rep function length = List.length
declare ocaml target_rep function length = `Byte_sequence_wrapper.big_num_length`
(* Err, the Coq line fails with:
    Type error: type mismatch: top-level expression
      Byte_sequence.byte_sequence
    and
      list _
*)

It seems using the native list length function with backticks instead of Lem's List.length would work. But that would require copy-pasting a lot of list.lem from the stdlib and more importantly re-coding a lot of functions in each backend's language (basically creating one Byte_sequence_wrapper per backend). I don't want to write a whole file of Coq, so I decided to reject that solution.

I've tried other strategies, like defining separate types and then trying to merge them in the byte_sequence type, but this doesn't work either.