Anomaly as a result of extraction in CertiCoq (assertion fails in ml code)

[mkarup]

I apologize if this is not the right place to report this, I admit I haven't investigated it thoroughly. Using the CertiCoq project to try to extract the parsing of the binary representation of a WebAssembly module (using WasmCert-Coq), I encountered an "anomaly", and at a quick glance, it looked like it originated in one of the phases that MetaCoq is responsible for. Again, I haven't investigated exactly what part of WasmCert that triggers this, so for now I leave this "minimal" example, and I will report back if I pinpoint it more accurately.

From Coq Require Import List.
From Coq.Strings Require Import Byte.
From CertiCoq.Plugin Require Import CertiCoq.
From Wasm Require Import binary_format_parser datatypes instantiation_func.

Definition test_bytes : list Byte.byte := x00 :: x61 :: x73 :: x6d :: x01 :: x00 :: x00 :: x00 :: nil.

Definition test_module : option module := run_parse_module test_bytes.

CertiCoq Compile test_module.

Error message:

Error:
Anomaly
"File "extraction/pCUICSafeRetyping.ml", line 48, characters 25-31: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Don't know if it even makes sense to include this, but the assertion failing code snippet in question is this:

(** val infer_as_sort :
    checker_flags -> abstract_env_impl -> __ -> PCUICEnvironment.context ->
    term -> principal_type -> principal_sort **)

let infer_as_sort cf x_type x _UU0393_ t0 tx =
  let filtered_var =
    reduce_to_sort cf x_type x _UU0393_
      (principal_type_type cf x_type x _UU0393_ t0 tx)
  in
  (match filtered_var with
   | Checked_comp a -> let Coq_existT (u, _) = a in Coq_existT (u, __)
   | TypeError_comp _ -> assert false (* absurd case *))

[mkarup]

I have to go back on my statement: I currently don't have the time to investigate this, so take the above code as the full bug report.

[mattam82]

That's an interesting report, will look into it!