`Set Crane Loopify` generates `return std::monostate{}` inside `void` lambda for sequenced `unit` branches

[joom]

With Set Crane Loopify., Crane can generate C++ lambdas declared -> void whose branches return std::monostate{}. The generated C++ then fails to compile with:

error: void block should not return a value
  return std::monostate{};

Minimal Repro

From Stdlib Require Import Lists.List.
From Crane Require Import Mapping.Std Mapping.NatIntStd Monads.ITree.
From Crane Require Extraction.
Import ListNotations.

Set Crane Loopify.
Local Open Scope itree_scope.

Module LoopifyUnitVoidRepro.

Axiom c_int : Type.
Axiom c_zero : c_int.

Axiom reproE : Type -> Type.
Crane Extract Skip reproE.

Definition cell_size : nat := 42.

Axiom draw_hidden_tile : nat -> nat -> itree reproE unit.
Axiom draw_revealed_tile : nat -> nat -> itree reproE unit.

Fixpoint loop (x y : nat) (cells : list bool) : itree reproE unit :=
  match cells with
  | [] => Ret tt
  | revealed :: rest =>
      (if revealed
        then draw_revealed_tile x y
        else draw_hidden_tile x y) ;;
      loop (x + cell_size) y rest
  end.

Definition main : itree reproE c_int :=
  loop 0 0 [true; false] ;;
  Ret c_zero.

End LoopifyUnitVoidRepro.

Crane Extract Inlined Constant LoopifyUnitVoidRepro.c_int => "int".
Crane Extract Inlined Constant LoopifyUnitVoidRepro.c_zero => "0".
Crane Extract Inlined Constant LoopifyUnitVoidRepro.draw_hidden_tile =>
  "((void)%a0, (void)%a1)".
Crane Extract Inlined Constant LoopifyUnitVoidRepro.draw_revealed_tile =>
  "((void)%a0, (void)%a1)".

Crane Extraction "loopify_unit_void_repro" LoopifyUnitVoidRepro LoopifyUnitVoidRepro.main.

Generated C++ Shape

The generated C++ includes a lambda declared as returning void, but the branches return std::monostate{}:

[&]() -> void {
  if (d_a0) {
    ((void)_loop_x, (void)y);
    return std::monostate{};
  } else {
    ((void)_loop_x, (void)y);
    return std::monostate{};
  }
}();

Compile Error

Compiling the generated C++ fails:

error: void block should not return a value
  return std::monostate{};

Expected Behavior

The generated C++ should not return a value from a lambda declared -> void.

[joom]

This may be a simpler file (without loopification) that recreates it:

From Stdlib Require Import Lists.List.
From Crane Require Import Mapping.NatIntStd Monads.ITree.
From Crane Require Extraction.
Import ListNotations.

Local Open Scope itree_scope.

Module NoMappingEventProbe.

Inductive reproE : Type -> Type :=
| Hidden : nat -> nat -> reproE unit
| Revealed : nat -> nat -> reproE unit.

Definition cell_size : nat := 42.

Definition draw_hidden_tile (x y : nat) : itree reproE unit :=
  embed (Hidden x y).

Definition draw_revealed_tile (x y : nat) : itree reproE unit :=
  embed (Revealed x y).

Fixpoint loop (x y : nat) (cells : list bool) : itree reproE unit :=
  match cells with
  | [] => Ret tt
  | revealed :: rest =>
      (if revealed
       then draw_revealed_tile x y
       else draw_hidden_tile x y) ;;
      loop (x + cell_size) y rest
  end.

End NoMappingEventProbe.

Crane Extraction "no_mapping_event_probe" NoMappingEventProbe.