"Could not compile test program" when dealing with Uint63.

[mikkelmilo]

coqc version: 8.11
quickchick version: 1.3.2

When I run the sample program below I get the error "Could not compile test program"

From Coq Require Import Int63.
From QuickChick Require Import QuickChick. Import QcNotation.
Instance showInt63 : Show Int63.int :=
{|
  show i := show (to_Z i)
|}.
Instance gensizedInt63 : GenSized Int63.int :=
{|
  arbitrarySized n := liftM of_Z (arbitrarySized n)
|}.
Instance shrinkInt63 : Shrink Int63.int :=
{|
  shrink n := cons n nil
|}.

Definition gint : G int := arbitrary.
Sample gint.

the error given by coqtop is:

File "QuickChickbee056.ml", line 276, characters 6-7:
276 |   eqb i (Uint63.of_int (0))
            ^
Warning 20: this argument will not be used by the function.
File "QuickChickbee056.ml", line 276, characters 8-27:
276 |   eqb i (Uint63.of_int (0))
              ^^^^^^^^^^^^^^^^^^^
Warning 20: this argument will not be used by the function.
File "QuickChickbee056.ml", line 276, characters 9-22:
276 |   eqb i (Uint63.of_int (0))
               ^^^^^^^^^^^^^
Error: Unbound module Uint63
Command exited with code 2.

This could also be the reason why Derive GenSized for Int63.int fails.

[Lysxia]

Thanks for reporting this issue. We indeed need some work to support native ints.

1. We must be able to tell QuickChick where to find the Uint63 module (I'm not even sure we're supposed to get it from Coq, it is part of an internal library). In the meantime I believe the only workaround is to extract and compile the OCaml by hand.

2. We must add Gen instances (it's not a type for which this should be derived.)

[mikkelmilo]

It seems that Int63.int is extracted to OCaml's Uint63: https://coq.inria.fr/library/Coq.extraction.ExtrOCamlInt63.html.

But the extraction seems to works fine:

From Coq Require Import Extraction.
Local Open Scope int_scope.
Definition ex : Int63.int := 2 + 3.
Extraction ex.

extracts to:

(** val ex : int **)
let ex =
  add (Uint63.of_int (2)) (Uint63.of_int (3))

Not sure if this helps.