Coq: Extraction with dependent records produces `assert false`

[arthuraa]

Version

8.8.0

Operating system

Ubuntu

Description of the problem

Consider the following snippet:

From Coq Require Import Extraction.

Extraction Language OCaml.

Record rec := Rec {sort :> Type; op : sort -> bool}.

Definition foo (x : unit) := unit.

Record bar x := {
  f1 : foo x;
  f2 : foo x
}.

Definition wrong x (b : bar x) : bool := op (Rec unit (fun _ => true)) (f1 x b).

Extraction "test.ml" wrong.

On my machine, this leads to the following extracted file:

type __ = Obj.t

type unit0 =
| Tt

type bool =
| True
| False

type rec0 = __ -> bool
  (* singleton inductive, whose constructor was Rec *)

type sort = __

(** val op : rec0 -> sort -> bool **)

let op r =
  r

type foo = unit0

type bar = { f1 : foo; f2 : foo }

(** val f1 : unit0 -> bar -> foo **)

let f1 _ x = x.f1

(** val wrong : unit0 -> bar -> bool **)

let wrong _ b =
  op (fun _ -> True) (Obj.magic f1 (assert false (* Proj Args *)) b)

The extractor included an assert false that causes the program to crash when calling wrong. Oddly, the issue disappears if I remove the f2 field from the record bar.

[samuelgruetter]

I think I ran into the same issue today with Coq 8.7.2: The extracted code contains

(Obj.magic loadByte0 (assert false (* Proj Args *)) memIsMem)

where memIsMem is an instance of the following typeclass:

Class Memory(m: Set)(w: nat) := mkMemory {
  loadByte   : m -> (word w) -> word  8;
  storeByte  : m -> (word w) -> word  8 -> m;
  ...
  memSize: m -> nat;

  loadStoreByte_eq: forall m (a1 a2: word w) v,
    valid_addr a1 1 (memSize m) ->
    a2 = a1 ->
    loadByte (storeByte m a1 v) a2 = v;
  ...
}

I could extract a minimal example if developers think they need more than @arthuraa's example above to investigate it.

[anton-trunov]

This bug affects OCaml code extracted from a Coq development based on SSReflect. This happens e.g. if we compare elements of finType for equality.

[anton-trunov]

@Zimmi48 Would it make sense to add ssreflect tag here? (because SSReflect-style libraries have a lot of things like this one)

[dranov]

Here is an example of what @anton-trunov mentioned:

From mathcomp.ssreflect
Require Import ssreflect ssrbool eqtype fintype.

Definition tuple := prod 'I_2 'I_2.

Definition all :=
  enum [finType of tuple].

Recursive Extraction all.

The extraction includes:

  let base2 c =
    { Countable.base = c.base; Countable.mixin =
      (Obj.magic mixin_base (assert false (* Proj Args *)) c.mixin) }

... which is actually executed when all is called.

[Zimmi48]

Sure.

[pi8027]

https://github.com/coq/coq/blob/c70412ec8b0bb34b7a5607c07d34607a147d834c/plugins/extraction/extraction.ml#L751-L762

As one can see in this comment, this kind of assert should not appear in the output. Inlining all the record projections would solve this issue. For the first example:

Extraction Inline f1 f2.

I think that the extraction plugin should inline them by default and the above let mla = ... in is not needed anymore, but we would need to ask Pierre Letouzey for his opinion.