Fixes #12418: an assert false in inference of return clause

[herbelin]

This is a quick fix to avoid the anomaly, with a fallback on before b1b8243.

Kind: bug fix

Fixes / closes #12418

• Added / updated test-suite (example is too large)
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

[JasonGross]

(example is too large)

Should I run the test-case through my bug minimizer?

[herbelin]

If does not take you time, why not.

[JasonGross]

I've set up my bug-minimizer-runner repo at https://github.com/JasonGross/run-coq-bug-minimizer/blob/master/run.sh to run the minimizer for this on GitHub actions. If I got it right, the minimized and standalone test-case should be available in https://github.com/JasonGross/run-coq-bug-minimizer/actions/runs/118319573 shortly

[herbelin]

It seems that the minimizer failed on a missing dependency in ExtLib.

[JasonGross]

Now updated to have it install coq-ext-lib, running at https://github.com/JasonGross/run-coq-bug-minimizer/runs/718296942?check_suite_focus=true

[JasonGross]

Updated, standalone version:
bug.v.zip

bug.v

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "Cava" "Cava" "-top" "Netlist" "-R" "." "Top" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/runner/.opam/4.08.1/lib/coq/user-contrib/Ltac2" "Ltac2") -*- *)
(* File reduced by coq-bug-finder from original input, then from 382 lines to 167 lines, then from 421 lines to 276 lines, then from 554 lines to 314 lines, then from 540 lines to 355 lines, then from 404 lines to 361 lines, then from 375 lines to 362 lines, then from 393 lines to 362 lines, then from 520 lines to 383 lines, then from 433 lines to 383 lines, then from 497 lines to 409 lines, then from 422 lines to 408 lines *)
(* coqc version 8.11.1 (May 2020) compiled on May 28 2020 23:11:31 with OCaml 4.08.1
   coqtop version 8.11.1 (May 2020) *)
Require Coq.Strings.String.
Require Coq.ZArith.ZArith.

Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.

Section monadic.

  Definition mcompose@{c d}
             {m:Type@{d}->Type@{c}}
             {M: Monad m}
             {T U V:Type@{d}}
             (f: T -> m U) (g: U -> m V): (T -> m V) :=
    fun x => bind (f x) g.

End monadic.

  Delimit Scope monad_scope with monad.
  Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope.

  Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2))
    (at level 61, c1 at next level, right associativity) : monad_scope.

  Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
    (at level 61, right associativity) : monad_scope.

  Notation "' pat <- c1 ;; c2" :=
    (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))
    (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.

Module Export StateMonad.

Set Implicit Arguments.

Section StateType.
  Variable S : Type.

  Record state (t : Type) : Type := mkState
  { runState : S -> t * S }.

  Global Instance Monad_state : Monad state :=
  { ret  := fun _ v => mkState (fun s => (v, s))
  ; bind := fun _ _ c1 c2 =>
    mkState (fun s =>
      let (v,s) := runState c1 s in
      runState (c2 v) s)
  }.

End StateType.

End StateMonad.

Import Coq.Strings.String.
Import Coq.ZArith.ZArith.

Inductive Signal : Type :=
  | Gnd: Signal
  | Vcc: Signal
  | Wire: N -> Signal
  | NamedWire: string -> Signal.

Import Coq.Lists.List.

Import ListNotations.
Open Scope monad_scope.

Inductive shape {A: Type} : Type :=
  | Empty : shape
  | One : A -> shape
  | Tuple2 : shape -> shape -> shape.

Inductive Kind : Type :=
  | Bit : Kind
  | BitVec : list nat -> Kind .

Notation bundle := (@shape Kind).

Fixpoint denoteBitVecWith {A : Type} (T : Type) (n : list A) : Type :=
  match n with
  | [] => T
  | [x] => list T
  | x::xs => list (denoteBitVecWith T xs)
  end.

Definition denoteKindWith (k : Kind) (T : Type) : Type :=
  match k with
  | Bit => T
  | BitVec v => denoteBitVecWith T v
  end.

Fixpoint mapBitVec {A B} (f: A -> B) (i : list nat) (l : list nat) : @denoteBitVecWith nat A l -> @denoteBitVecWith nat B l :=
  match l, i  return @denoteBitVecWith nat A l -> @denoteBitVecWith nat B l with
  | [], _         => f
  | [x], [_]      => map f
  | x::xs, p::ps  => map (mapBitVec f ps xs)
  | _, _          => fun _ => []
  end.

Fixpoint signalTy (T : Type) (s : shape) : Type :=
  match s with
  | Empty  => unit
  | One t => denoteKindWith t T
  | Tuple2 s1 s2  => prod (signalTy T s1) (signalTy T s2)
  end.

Inductive ConstExpr : Type :=
| HexLiteral: nat -> N -> ConstExpr
| StringLiteral: string -> ConstExpr.

Inductive Instance : Type :=

  | WireInputBit:     string -> Signal -> Instance
  | WireInputBitVec:  forall sizes, string ->
                      @denoteBitVecWith nat Signal sizes -> Instance
  | WireOutputBit:    string -> Signal -> Instance
  | WireOutputBitVec: forall sizes, string ->
                      @denoteBitVecWith nat Signal sizes -> Instance

  | Not:       Signal -> Signal -> Instance
  | And:       Signal -> Signal -> Signal -> Instance
  | Nand:      Signal -> Signal -> Signal -> Instance
  | Or:        Signal -> Signal -> Signal -> Instance
  | Nor:       Signal -> Signal -> Signal -> Instance
  | Xor:       Signal -> Signal -> Signal -> Instance
  | Xnor:      Signal -> Signal -> Signal -> Instance
  | Buf:       Signal -> Signal -> Instance

  | DelayBit:  Signal -> Signal -> Instance

  | AssignBit: Signal -> Signal -> Instance

  | UnsignedAdd : list Signal -> list Signal -> list Signal -> Instance

  | IndexBitArray: list Signal -> list Signal -> Signal -> Instance
  | IndexArray: list (list Signal) -> list Signal -> list Signal -> Instance
  | Component: string -> list (string * ConstExpr) -> list (string * Signal) ->
               Instance.

Notation Netlist := (list Instance).

Import Coq.Classes.Morphisms.

Reserved Infix "~>" (at level 90, no associativity).
Reserved Infix ">>>" (at level 53, right associativity).
Reserved Infix "=M=" (at level 54, no associativity).

Reserved Infix "**" (at level 30, right associativity).

Class Category := {
  object : Type;

  morphism : object -> object -> Type
    where "a ~> b" := (morphism a b);

  id {x} : x ~> x;

  compose {x y z} (f: y ~> z) (g : x ~> y) : x ~> z
    where "g >>> f" := (compose f g);

  morphism_equivalence: forall x y (f g: x ~> y), Prop
    where "f =M= g" := (morphism_equivalence _ _ f g);
  morphism_setoid_equivalence : forall x y , Equivalence (morphism_equivalence x y);
  compose_respects_equivalence : forall x y z , Proper (morphism_equivalence y z ==> morphism_equivalence x y ==> morphism_equivalence x z) compose;

  id_left {x y} (f: x ~> y) : (id >>> f) =M= f;
  id_right {x y} (f: x ~> y) : (f >>> id) =M= f;

  associativity {x y z w} {f: x~>y} {g: y~>z} {h: z~>w} : (f >>> g) >>> h =M= f >>> (g >>> h);
}.

Notation "x ~> y" := (morphism x y) : category_scope.
Notation "g >>> f" := (compose f g) : category_scope.
Notation "f =M= g" := (morphism_equivalence _ _ f g) : category_scope.

Open Scope category_scope.

Class Arrow := {
  cat :> Category;
  unit : object;
  product : object -> object -> object
    where "x ** y" := (product x y);

  copy {x} : x ~> x**x;
  drop {x} : x ~> unit;
  swap {x y} : x**y ~> y**x;

  first  {x y z} (f : x ~> y) : x ** z ~> y ** z;
  second {x y z} (f : x ~> y) : z ** x ~> z ** y;

  exl  {x y} : x ** y ~> x;
  exr  {x y} : x ** y ~> y;

  uncancell {x} : x ~> unit**x;
  uncancelr {x} : x ~> x**unit;
  assoc   {x y z} : ((x**y)**z) ~> (x**(y**z));
  unassoc {x y z} : (x**(y**z)) ~> ((x**y)**z);

  exl_unit_uncancelr x: @exl x unit >>> uncancelr =M= id;
  exr_unit_uncancell x: @exr unit x >>> uncancell =M= id;
  uncancelr_exl x:      uncancelr >>> @exl x unit =M= id;
  uncancell_exr x:      uncancell >>> @exr unit x =M= id;

  drop_annhilates {x y} (f: x~>y): f >>> drop =M= drop;

  exl_unit_is_drop {x}: @exl unit x =M= drop;
  exr_unit_is_drop {x}: @exr x unit =M= drop;

  first_first   {x y z w} (f: x~>y) (g:y~>z): @first x y w f >>> first g  =M= first (f >>> g);
  second_second {x y z w} (f: x~>y) (g:y~>z): @second x y w f >>> second g  =M= second (f >>> g);

  swap_swap {x y}: @swap x y >>> swap =M= id;

  first_id  {x w}: @first x x w id  =M= id;
  second_id {x w}: @second x x w id  =M= id;

  first_f  {x y w} (f: x~>y) (g:x~>y): f =M= g -> @first x y w f =M= first g;
  second_f {x y w} (f: x~>y) (g:x~>y): f =M= g -> @second x y w f =M= second g;

  assoc_unassoc {x y z}: @assoc x y z >>> unassoc =M= id;
  unassoc_assoc {x y z}: @unassoc x y z >>> assoc =M= id;

  first_exl  {x y w} f: @first x y w f >>> exl =M= exl >>> f;
  second_exr {x y w} f: @second x y w f >>> exr =M= exr >>> f;
}.

Notation "x ** y" := (product x y)
  (at level 30, right associativity) : arrow_scope.

Open Scope arrow_scope.

Class Cava  := {
  cava_arrow :> Arrow;

  bit : object;
  bitvec : list nat -> object;

  constant : bool -> (unit ~> bit);
  constant_vec (dimensions: list nat) : denoteBitVecWith bool dimensions -> (unit ~> bitvec dimensions);

  not_gate:  bit        ** unit ~> bit;
  and_gate:  bit ** bit ** unit ~> bit;
  nand_gate: bit ** bit ** unit ~> bit;
  or_gate:   bit ** bit ** unit ~> bit;
  nor_gate:  bit ** bit ** unit ~> bit;
  xor_gate:  bit ** bit ** unit ~> bit;
  xnor_gate: bit ** bit ** unit ~> bit;
  buf_gate:  bit        ** unit ~> bit;

  xorcy:     bit ** bit ** unit ~> bit;
  muxcy:     bit ** bit ** bit ** unit ~> bit;

  unsigned_add a b s: bitvec [a] ** bitvec [b] ** unit ~> bitvec [s];
}.

  #[refine] Instance NetlistCat : Category := {
    object := bundle;
    morphism X Y := signalTy Signal X -> state (Netlist * N) (signalTy Signal Y);
    id X x := ret x;
    compose X Y Z f g := g >=> f;

    morphism_equivalence x y f g := True;
  }.
  Proof.
    intros.
    apply Build_Equivalence.
    unfold Reflexive.
auto.
    unfold Symmetric.
auto.
    unfold Transitive.
auto.
    intros.
    unfold Proper.
    refine (fun f => _).
intros.
    refine (fun g => _).
intros.
    auto.

    auto.
auto.
auto.
  Defined.

  #[refine] Instance NetlistArr : Arrow := {
    cat := NetlistCat;
    unit := Empty;
    product := Tuple2;

    first X Y Z f '(z,y) :=
      x <- f z ;;
      ret (x,y);

    second X Y Z f '(y,z) :=
      x <- f z ;;
      ret (y,x);

    exl X Y '(x,y) := ret x;
    exr X Y '(x,y) := ret y;

    drop _ _ := ret Datatypes.tt;
    copy _ x := ret (x,x);
    swap _ _ '(x,y) := ret (y,x);

    uncancell _ x := ret (tt, x);
    uncancelr _ x := ret (x, tt);

    assoc _ _ _ '((x,y),z) := ret (x,(y,z));
    unassoc _ _ _ '(x,(y,z)) := ret ((x,y),z);
  }.
  Proof.
    intros.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
    simpl; auto.
  Defined.

  Instance NetlistCava : Cava := {
    cava_arrow := NetlistArr;

    bit := One Bit;
    bitvec n := One (BitVec n);

    constant b _ := match b with
      | true => ret 1%N
      | false => ret 0%N
      end;

    constant_vec n v _ := ret (mapBitVec (fun b => match b with
      | true => 1%N
      | false => 0%N
    end) n n v);

    not_gate '(x,tt) :=
      '(nl, i) <- get ;;
      put (cons (Not x i) nl, Wire ((i+1)%N)) ;;
      ret i;

    and_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (And x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    nand_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (Nand x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    or_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (Or x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    nor_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (Nor x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    xor_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (Xor x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    xnor_gate '(x,(y,tt)) :=
      '(nl, i) <- get ;;
      put (cons (Xnor x y i) nl, Wire ((i+1)%N)) ;;
      ret i;

    buf_gate '(x,tt) :=
      '(nl, i) <- get ;;
      put (cons (Buf x i) nl, Wire ((i+1)%N)) ;;
      ret i;

    xorcy '(x, (y, tt)) :=
      '(nl, i) <- get ;;
      put (cons (Component "XORCY" [] [("O", i); ("CI", x); ("LI", y)]) nl, Wire ((i+1)%N)) ;;
      ret i;

    muxcy '(s,(ci,(di, tt))) :=
      '(nl, i) <- get ;;
      put (cons (Component "MUXCY" [] [("O", i); ("S", s); ("CI", ci); ("DI", di)]) nl, Wire ((i+1)%N)) ;;
      ret i;

    unsigned_add m n s '(x,(y, tt)) :=
      '(nl, i) <- get ;;
      let o := map (compose Wire N.of_nat) (seq (N.to_nat i) s) in
      put (cons (UnsignedAdd x y o) nl, (i + N.of_nat s)%N) ;;
      ret o;
  }.

[ppedrot]

Here is an even smaller test:

Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
  { ret : forall {t : Type@{d}}, t -> m t }.

Record state {S : Type} (t : Type) : Type := mkState { runState : t }.

Global Declare Instance Monad_state : forall S, Monad (@state S).

Class Cava  := {
  constant : bool -> unit;
  constant_vec : unit;
}.

Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit.

Instance T : Cava := {

  constant b := match b with
    | true => ret tt
    | false => ret tt
    end;

  constant_vec := @F _ (fun b => match b with
    | true => tt
    | false => tt
  end);

}.

[ejgallego]

Thanks @ppedrot ; @herbelin , can you add the test-case and a changelog? We will merge afterwards.

[herbelin]

Thanks everyone, is this the last word, or can do we even smaller? In particular, @ppedrot, could you understand whether type classes are necessary for the anomaly to be triggered?

@ejgallego: change log added

[ppedrot]

I think we need typeclasses to postpone the evar resolution, I don't know how to do that otherwise.

[ejgallego]

@herbelin test is failing.

[ppedrot]

Sorry, I forgot to mention that you need to wrap the last command inside a Fail if you want to turn this into a test-suite-worthy test.

[ejgallego]

Failure is spurious; will merge later today.