Better error messages

Probably if the lists are the same lengths, then we want to compare them
element-wise rather than all at once.  It's way too verbose to keep
expanding them, so we only do that when lists are not the same length.

We now get error messages such as
```
Unable to unify: [inr [378, 381, 384]] == [inr [101, 106, 108]]
Could not unify the values at index 0: [mit-plv#378, mit-plv#381, mit-plv#384] != [mit-plv#101, mit-plv#106, mit-plv#108]
index 0: mit-plv#378 != mit-plv#101
(slice 0 44, [mit-plv#377]) != (slice 0 44, [mit-plv#98])
index 0: mit-plv#377 != mit-plv#98
(add 64, [mit-plv#345, mit-plv#375]) != (add 64, [mit-plv#57, mit-plv#96])
index 0: mit-plv#345 != mit-plv#57
(slice 0 44, [mit-plv#337]) != (slice 0 44, [#44])
index 0: mit-plv#337 != #44
(add 64, [#41, mit-plv#334]) != (add 64, [#25, #41])
index 1: mit-plv#334 != #25
(mul 64, [#1, mit-plv#331]) != (mul 64, [#0, #1, #22])
[(add 64, [mit-plv#329, mit-plv#329])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [#7, mit-plv#328]), (mul 64, [#7, mit-plv#328])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])]), (mul 64, [(const 2, []), (add 64, [#0, mit-plv#327])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, mit-plv#326])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [#0, (mul 64, [#0, (const 4, [])])])])])] != [#0, (const 20, [])]
[(add 64, [(mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])]), (mul 64, [(const 2, []), (add 64, [(old 64 0, []), (mul 64, [(old 64 0, []), (const 4, [])])])])])] != [(old 64 0, []), (const 20, [])]
```

The second to last line is generally the one to look at; the last line
adds a bit more detail to it.  Perhaps we should instead list out the
values of indices rather than expanding one additional level?

src/Assembly/Equivalence.v

@@ -158,17 +158,26 @@ Fixpoint remove_common_indices {T} (eqb : T -> T -> bool) (xs ys : list T) (star
           else ((start_idx, x) :: xs', ys')
      end.
 
-Fixpoint explain_array_unification_error_without_commutativity
+Definition show_expr_node_lite : Show Symbolic.expr
+  := fix show_expr_node_lite (e : Symbolic.expr) : string
+    := match e with
+       | ExprRef i => "#" ++ show i
+       | ExprApp (op, e)
+         => "(" ++ show op ++ ", " ++ @show_list _ show_expr_node_lite e ++ ")"
+       end%string.
+
+Fixpoint explain_array_unification_error_single
          (singular plural : string)
          (left_descr right_descr : string)
          (explain_idx_unification_error : idx -> idx -> list string)
          (describe_idx : idx -> list string)
+         (modulo_commutativity : bool)
          (asm_array PHOAS_array : list idx) (start_idx : nat)
   : list string
-  := let recr := explain_array_unification_error_without_commutativity singular plural left_descr right_descr explain_idx_unification_error describe_idx in
+  := let recr := explain_array_unification_error_single singular plural left_descr right_descr explain_idx_unification_error describe_idx modulo_commutativity in
      match asm_array, PHOAS_array with
      | [], []
-       => ["Internal Error: Unifiable " ++ plural]
+       => ["Internal Error: Unifiable " ++ plural ++ (if modulo_commutativity then " modulo commutativity" else "")]
      | [], PHOAS_array
        => ((["The " ++ right_descr ++ " " ++ singular ++ " contains " ++ show (List.length PHOAS_array) ++ " more values than the " ++ left_descr ++ " " ++ singular ++ "."]%string)
              ++ List.flat_map describe_idx PHOAS_array)%list
@@ -179,9 +188,13 @@ Fixpoint explain_array_unification_error_without_commutativity
        => if Decidable.dec (asm_value = PHOAS_value)
           then recr asm_array PHOAS_array (S start_idx)
           else
-            ((["index " ++ show start_idx ++ ": #" ++ show asm_value ++ " != #" ++ show PHOAS_value]%string)
-               ++ explain_idx_unification_error asm_value PHOAS_value
-            )%list
+            if modulo_commutativity && List.existsb (N.eqb asm_value) PHOAS_array
+            then
+              recr asm_array (PHOAS_value :: List.removen (N.eqb asm_value) PHOAS_array 1) (S start_idx)
+            else
+              ((["index " ++ show start_idx ++ ": " ++ show_expr_node_lite (ExprRef asm_value) ++ " != " ++ show_expr_node_lite (ExprRef PHOAS_value)]%string)
+                 ++ explain_idx_unification_error asm_value PHOAS_value
+              )%list
      end%string%list%bool.
 
 Definition recursive_deps_list_step
@@ -256,14 +269,6 @@ Definition indices_at_leaves_map (ls : list Symbolic.expr) : list idx
 Definition indices_at_leaves (e : Symbolic.expr) : list idx
   := indices_at_leaves_map [e].
 
-Definition show_expr_node_lite : Show Symbolic.expr
-  := fix show_expr_node_lite (e : Symbolic.expr) : string
-    := match e with
-       | ExprRef i => "#" ++ show i
-       | ExprApp (op, e)
-         => "(" ++ show op ++ ", " ++ @show_list _ show_expr_node_lite e ++ ")"
-       end%string.
-
 Fixpoint make_iteratively_revealed_exprs
          (dag : dag)
          (max_depth : nat)
@@ -341,7 +346,7 @@ Definition explain_array_unification_error
            (modulo_commutativity : bool)
            (asm_array PHOAS_array : list idx)
   : list string
-  := if modulo_commutativity
+  := if (modulo_commutativity && negb (List.length asm_array =? List.length PHOAS_array))%nat%bool
      then
        match remove_common_indices N.eqb asm_array PHOAS_array 0 with
        | ([], [])
@@ -361,7 +366,7 @@ Definition explain_array_unification_error
          => iteratively_explain_array_unification_error_modulo_commutativity dag describe_idx asm_array PHOAS_array
        end%string%list%bool
      else
-       explain_array_unification_error_without_commutativity singular plural left_descr right_descr explain_idx_unification_error describe_idx asm_array PHOAS_array 0.
+       explain_array_unification_error_single singular plural left_descr right_descr explain_idx_unification_error describe_idx modulo_commutativity asm_array PHOAS_array 0.
 
 Definition explain_mismatch_from_state
            (left_descr right_descr : string)