Extraction fails with 'The informative inductive type sigT has a Prop instance'

[cpitclaudel]

Description of the problem

In the following example, a sigT of two Types fails to extract, printing an error message about props:

Require Import Extraction.

Inductive unit_type : Type := tt_type.
Inductive unit_set : Set := tt_set.

Example set_and_set : { n: unit_set & unit_set } :=
  existT (fun _ : unit_set => unit_set) tt_set tt_set.

Example type_and_set : { n: unit_type & unit_set } :=
  existT (fun _ : unit_type => unit_set) tt_type tt_set.

Example set_and_type : { n: unit_set & unit_type } :=
  existT (fun _ : unit_set => unit_type) tt_set tt_type.

Example type_and_type : { n: unit_type & unit_type } :=
  existT (fun _ : unit_type => unit_type) tt_type tt_type.

Extraction set_and_set.
Extraction type_and_set.
Extraction set_and_type.
Fail Extraction type_and_type.

The error message is this:

The command has indeed failed with message:
The informative inductive type sigT has a Prop instance
in type_and_type (or in its mutual block).
This happens when a sort-polymorphic singleton inductive type
has logical parameters, such as (I,I) : (True * True) : Prop.
The Ocaml extraction cannot handle this situation yet.
Instead, use a sort-monomorphic type such as (True /\ True)
or extract to Haskell.

… but I don't see any props in here. Is this a bug?

Coq Version

Confirmed on 8.4pl6, 8.7.2, 8.9.1, and master.

[cpitclaudel]

Also, changing the extraction language to JSON or Scheme produces the same message ("The Ocaml extraction cannot handle this situation yet.").

[SkySkimmer]

Inductive unit_type : Type := tt_type.
Check unit_type. (* : Prop *)

See #7424

[silene]

The message might a bit confusing, but this is a traditional limitation of extraction. Since { n: unit_type & unit_type } has potentially the Prop type, it means that type_and_type might have no actual value at execution time, yet you can pass it to a function such as projT1. All hell ensues. So, the extraction mechanism prefers to complain rather than to produce an OCaml program that will perform illegal memory accesses.

[cpitclaudel]

All hell ensues. So, the extraction mechanism prefers to complain rather than to produce an OCaml program that will perform illegal memory accesses.

Thanks. Can you clarify why extracting to Haskell works, then?
Also, is there a workaround, short of redefining sigT with let t := Type in t?

See #7424

Thanks; is the issue really just that? In my non-simplified example, I'm running into is with a sigT that contains two instances of eq:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive member {K: Type}: K -> list K -> Type :=
| MemberHd: forall k sig, member k (k :: sig)
| MemberTl: forall k k' sig, member k sig -> member k (k' :: sig).

Definition mdestruct {K sig} {k: K} (m: member k sig)
  : match sig return member k sig -> Type with
    | [] => fun m => False
    | k' :: sig =>
      fun m => ({ m': member k sig & m = MemberTl k k' sig m' } +
             { eqn: k = k'
                    & m = eq_rect _ _ (fun _ => MemberHd k sig)
                                  _ eqn m
                    (* ⇨ & unit ⇦ *) })%type
    end m.
  destruct m; cbn.
  - right; exists eq_refl; eauto using tt.
  - left; eauto.
Defined.

Lemma member_map {A B} (f: A -> B) a:
  forall ls,
    member a ls ->
    member (f a) (List.map f ls).
Proof.
  induction ls; cbn; intros m.
  - destruct (mdestruct m).
  - destruct (mdestruct m) as [(m' & Heq) | [ eqn Heq (* ⇨ _ ⇦ *) ] ];
      [ destruct Heq | destruct eqn, Heq ];
      eauto using MemberHd, MemberTl.
Defined.

Require Import Extraction.
Extraction member_map.

If I change to a sigT2 and add a unit (by uncommenting the parts in (* ⇨ & … ⇦ *)), it works, which I guess is because it forces the type to be in Set? But then why doesn't adding a cast (<: Set) in the right places work?

[cpitclaudel]

Why doesn't adding a cast (<: Set) in the right places work?

Using k = k' <: Type doesn't work, but defining Definition eq_type {A} (a a': A) : Type := eq a a'. and using eq_type k k' does work, so I guess that's one workaround.

[silene]

When extracting to Haskell, Coq (ab)uses the lazyness of the language. In other words, applying projT1 is just as broken as in OCaml, but the term will never be forcefully reduced, so it does not matter.