Circuit combinators requiring casts

[samuelgruetter]

While trying to write some circuit combinator over abstract input/output/state types, I noted that we sometimes need to insert casts. For instance:

Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.

Require Import Cava.Types.
Require Import Cava.Expr.
Require Import Cava.Primitives.
Require Import Cava.Semantics.

Section WithVar.
  Context {var: tvar}.

  (* TODO don't match on e but on boolean equality between s1 and s2, to make sure it also
     computes when e has been Qed'd instead of Defined *)
  Definition cast_circuit_state{s1 s2 x y: type}(e: s1 = s2): Circuit s1 x y -> Circuit s2 x y :=
    match e with
    | eq_refl => id
    end.

  Lemma absorb_Unit_r{x}: x ++ [] = x.
  Proof. destruct x; reflexivity. Defined.

  (* Note: this is not a correct implementation of `Delay`, because LetDelay has
     Mealy semantics, but we'd need Moore semantics to implement `Delay` like this *)
  Definition Delay'{x : type}(init: denote_type x): Circuit x [x] x :=
    cast_circuit_state absorb_Unit_r
      (Abs (fun inp => LetDelay init (fun _ => Var inp) (fun state => Var state))).
End WithVar.

If I omit the line cast_circuit_state absorb_Unit_r, I get a typechecking error saying that the term has type Circuit (x ++ [] ++ []) [x] x while it is expected to have type Circuit x [x] x (cannot unify x ++ [] ++ [] and x).

Is there a better way to deal with such errors?

[blaxill]

I've been leaving the states unreduced e.g.

Definition Delay'{x : type}(init: denote_type x): Circuit _ [x] x :=

I don't see this as an issue, but perhaps you have something in mind?

A heavy handed alternative could be to have a syntax Expr without the state typing, and then a realise_state: UExpr i o -> Expr state i o function to generate it.

[blaxill]

Another alternative could be to bifurcate the state and variable types, so that state-unit absorbs and the variable-unit doesn't. Since the state of an expression is created from these known state-units, and a variable-unit wouldnt reduce (like the other non-unit types), the state type wouldn't need rewriting to reduce in the case of unknown variable types.

[jadephilipoom]

I attempted to resolve this in some experiments here in case it's helpful; I used typeclasses to automatically find state-type-conversion functions (as opposed to proofs, to avoid issues with opaque terms in computation).