coq: Remove two coercions (USugar and type_sz) to avoid subtle issues

Reported-by: @stellamplau
Co-authored-by: @BTHOM

coq/Circuits.v

@@ -367,10 +367,10 @@ Section CircuitCompilation.
   Defined.
 
   Section Action.
-    Definition compile_unop (fn: fn1) (a: circuit (PrimSignatures.Sigma1 fn).(arg1Type)):
-      circuit (PrimSignatures.Sigma1 fn).(retType) :=
-      let cArg1 fn := circuit (arg1Type (PrimSignatures.Sigma1 fn)) in
-      let cRet fn := circuit (retType (PrimSignatures.Sigma1 fn)) in
+    Definition compile_unop (fn: fn1) (a: circuit (type_sz (PrimSignatures.Sigma1 fn).(arg1Type))):
+      circuit (type_sz (PrimSignatures.Sigma1 fn).(retType)) :=
+      let cArg1 fn := circuit (type_sz (PrimSignatures.Sigma1 fn).(arg1Type)) in
+      let cRet fn := circuit (type_sz (PrimSignatures.Sigma1 fn).(retType)) in
       match fn return cArg1 fn -> cRet fn with
       | Display fn => fun _ => CConst Ob
       | Conv tau fn => fun a =>
@@ -398,12 +398,12 @@ Section CircuitCompilation.
       end a.
 
     Definition compile_binop (fn: fn2)
-               (a1: circuit (PrimSignatures.Sigma2 fn).(arg1Type))
-               (a2: circuit (PrimSignatures.Sigma2 fn).(arg2Type)):
-      circuit (PrimSignatures.Sigma2 fn).(retType) :=
-      let cArg1 fn := circuit (arg1Type (PrimSignatures.Sigma2 fn)) in
-      let cArg2 fn := circuit (arg2Type (PrimSignatures.Sigma2 fn)) in
-      let cRet fn := circuit (retType (PrimSignatures.Sigma2 fn)) in
+               (a1: circuit (type_sz (PrimSignatures.Sigma2 fn).(arg1Type)))
+               (a2: circuit (type_sz (PrimSignatures.Sigma2 fn).(arg2Type))):
+      circuit (type_sz (PrimSignatures.Sigma2 fn).(retType)) :=
+      let cArg1 fn := circuit (type_sz (PrimSignatures.Sigma2 fn).(arg1Type)) in
+      let cArg2 fn := circuit (type_sz (PrimSignatures.Sigma2 fn).(arg2Type)) in
+      let cRet fn := circuit (type_sz (PrimSignatures.Sigma2 fn).(retType)) in
       match fn return cArg1 fn -> cArg2 fn -> cRet fn with
       | Eq tau => fun a1 a2 => CBinop (EqBits (type_sz tau)) a1 a2
       | Bits2 fn => fun a1 a2 => CBinop fn a1 a2
@@ -420,8 +420,8 @@ Section CircuitCompilation.
              (Gamma: ccontext sig)
              (a: action pos_t var_t R Sigma sig tau)
              (clog: rwcircuit):
-      @action_circuit tau * (ccontext sig) :=
-      match a in action _ _ _ _ ts tau return ccontext ts -> @action_circuit tau * ccontext ts with
+      @action_circuit (type_sz tau) * (ccontext sig) :=
+      match a in action _ _ _ _ ts tau return ccontext ts -> @action_circuit (type_sz tau) * ccontext ts with
       | Fail tau => fun Gamma =>
         ({| retVal := $`"fail"`Bits.zero (type_sz tau); (* LATER: Question mark here *)
             erwc := {| canFire := $`"fail_cF"` Ob~0;

coq/Demo.v

@@ -35,8 +35,8 @@ Module Ex1.
     | r1 =>
       {{ let x := read0(R0) in
          if (`UExternalCall Even (UVar "x")`)
-         then write0(R1,`UConstBits Ob~1`)
-         else write0(R1,`UConstBits Ob~1`)
+         then write0(R1,`USugar (UConstBits Ob~1)`)
+         else write0(R1,`USugar (UConstBits Ob~1)`)
                        }}
     end.
 
@@ -345,7 +345,7 @@ Module ManualUnpacker <: Unpacker.
         `SCall2 (USubstField "immediate")
          (SCall2 (USubstField "dst")
                  (SCall2 (USubstField "src")
-                         (UUnop (UConv (UUnpack (struct_t decoded_sig))) (UConstBits (Bits.zero 32)))
+                         (UUnop (UConv (UUnpack (struct_t decoded_sig))) (USugar (UConstBits (Bits.zero 32))))
                          {{ src }})
                  {{ dst }})
          {{ imm }}`
@@ -386,8 +386,9 @@ Module ManualFetcher <: Fetcher.
     end.
 
   Definition fetch_instr reg_t pc : uaction reg_t :=
-    Eval compute in (USwitch (UVar pc) (UConstBits (Bits.zero 32))
-                             (all_branches 3 N.zero instructions)).
+    Eval compute in
+      (USugar (USwitch (UVar pc) (USugar (UConstBits (Bits.zero 32)))
+                       (all_branches 3 N.zero instructions))).
 End ManualFetcher.
 
 Module PrimitiveFetcher <: Fetcher.
@@ -508,7 +509,7 @@ Module Pipeline.
       write0(invalid, Ob~1);
       if `G[[UVar "data"]]` == `G[[F[[UVar "v"]]]]`
       then
-        `UConstBits Ob`
+        `USugar (UConstBits Ob)`
       else
         write0(correct, Ob~0)
     else
@@ -628,7 +629,7 @@ Module RegisterFile_Ordered.
   Definition _ReadReg : uaction _ empty_ext_fn_t :=
     {{
     let v := read0(rIndex) in
-    write0(rIndex,v + `UConstBits (Bits.of_nat (log2 nregs) 1)`);
+    write0(rIndex,v + `USugar (UConstBits (Bits.of_nat (log2 nregs) 1))`);
     write0(rOutput,`UCompleteSwitch (log2 nregs) (pred nregs) "v"
                     (vect_map (fun idx => {{ read0(rData idx) }}) (all_indices nregs))`)
     }}.
@@ -707,7 +708,7 @@ Module Enums.
        let bits_a := `UUnop (UConv UPack) {{read0(rA)}}` in
        let bits_b := `UUnop (UConv UPack) {{read0(rB)}}` in
        let neg_a := !bits_a in
-       let succ_b := bits_b + `UConstBits Ob~0~0~1` in
+       let succ_b := bits_b + `USugar (UConstBits Ob~0~0~1)` in
        write0(rA,`UUnop (UConv (UUnpack (enum_t flag_sig))) {{neg_a}}`);
        write0(rB, `UUnop (UConv (UUnpack (enum_t flag_sig))) {{succ_b}}`)
     }}.
@@ -1011,13 +1012,13 @@ Definition gcd_start : uaction reg_t ext_fn_t  :=
   Definition sub  : UInternalFunction reg_t ext_fn_t :=
     {{
         fun (arg1 : bits_t 16) (arg2 : bits_t 16) : bits_t 16 =>
-          (arg1 + !arg2 + `UConstBits (Bits.of_nat 16 1)`)
+          (arg1 + !arg2 + `USugar (UConstBits (Bits.of_nat 16 1))`)
     }} .
 
   Definition lt16 : UInternalFunction reg_t ext_fn_t :=
     {{
         fun (arg1 : bits_t 16) (arg2 : bits_t 16) : bits_t 1 =>
-          (funcall sub (arg1, arg2))[`UConstBits (Bits.of_nat 4 15)`]
+          (funcall sub (arg1, arg2))[`USugar (UConstBits (Bits.of_nat 4 15))`]
     }}.
 
   Fixpoint lt (sz: nat) : UInternalFunction reg_t ext_fn_t :=

coq/Parsing.v

@@ -151,7 +151,7 @@ Notation "'funcall' method '(' args ')'" :=
 
 
 Notation "'call0' instance method " :=
-  (UCallModule instance id method nil)
+  (USugar (UCallModule instance id method nil))
     (in custom koika at level 98, instance constr at level 0, method constr at level 0).
 Notation "'funcall0' method " :=
   (UInternalCall method nil)
@@ -227,7 +227,7 @@ Module Type Tests.
   Definition test_16 : uaction reg_t := {{ !read0(data1) && !read0(data1) }}.
   Definition test_17 : uaction reg_t := {{ !read0(data1) && magic}}.
   Definition test_18 : uaction reg_t := {{ !read0(data1) && Yoyo }}.
-  Definition test_19 : uaction reg_t := {{ yoy [ oio && ab ] && `UConstBits Ob~1~0` }}.
+  Definition test_19 : uaction reg_t := {{ yoy [ oio && ab ] && `USugar (UConstBits Ob~1~0)` }}.
   Definition test_20 : uaction reg_t := {{ yoyo [ magic :+ 3 ] && yoyo }}.
   Definition test_20' : uaction reg_t := {{ {yoyo [ magic :+ 3 ], yoyo} && yoyo }}.
   Definition test_20'' : uaction reg_t := {{ { {yoyo [ magic :+ 3 ], yoyo},bla} && yoyo }}.

coq/Std.v

@@ -41,7 +41,7 @@ Module Fifo1 (f: Fifo).
   Definition deq :  UInternalFunction reg_t empty_ext_fn_t :=
     {{ fun _ : T =>
       if (read0(valid0)) then
-        write0(valid0,`UConstBits Ob~0`);
+        write0(valid0,`USugar (UConstBits Ob~0)`);
           read0(data0)
       else
         fail(5)}}.

coq/Syntax.v

@@ -39,8 +39,6 @@ Section Syntax.
                 (fn: InternalFunction fn_name_t var_t (@uaction module_reg_t module_ext_fn_t))
                 (args: list uaction).
 
-  Coercion USugar: usugar >-> uaction.
-
   Inductive uscheduler :=
   | UDone
   | UTry (r: rule_name_t) (s1 s2: uscheduler)

coq/SyntaxMacros.v

@@ -65,9 +65,12 @@ Module Display.
          int_body := USugar USkip |}.
 
     Fixpoint extend_printer f offset (printer: intfun) : intfun :=
-      let display_utf8 s := UUnop (UDisplay UDisplayUtf8) (UConstString s) in
-      let display_value arg := UUnop (UDisplay UDisplayValue) (UVar arg) in
-      let '(Build_InternalFunction int_name int_argspec int_retType int_body) := printer in
+      let display_utf8 s :=
+          UUnop (UDisplay UDisplayUtf8) (USugar (UConstString s)) in
+      let display_value arg :=
+          UUnop (UDisplay UDisplayValue) (UVar arg) in
+      let '(Build_InternalFunction int_name int_argspec int_retType int_body) :=
+          printer in
       match f with
       | Str s =>
         {| int_name := int_name;

coq/TypeInference.v

@@ -115,7 +115,7 @@ Section TypeInference.
       match e with
       | UError err => Failure err
       | USugar _ => Failure (mkerror pos SugaredConstructorInAst e)
-      | UFail n => Success (EX (Fail (bits_t n)))
+      | UFail tau => Success (EX (Fail tau))
       | UVar var =>
         let/res tau_m := opt_result (assoc var sig) (mkerror pos (UnboundVariable var) e) in
         Success (EX (Var ``tau_m))

coq/Types.v

@@ -188,7 +188,6 @@ Qed.
 
 (** * Coercions **)
 
-Coercion type_sz : type >-> nat.
 Coercion type_denote : type >-> Sortclass.
 
 (** * Anonymous function signatures **)