Fix specialization bug involving function annotations not matching valspecs

Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.

While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:

Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)

In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.

What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.

1 files changed, 17 insertions, 7 deletions

diff --git a/src/specialize.ml b/src/specialize.ml
index eaef1231..646b92f7 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -351,8 +351,9 @@ let specialize_id_valspec spec instantiations id ast =
 
 (* When we specialize a function definition we also need to specialize
    all the types that appear as annotations within the function
-   body. *)
-let specialize_annotations instantiation =
+   body. Also remove any type-annotation from the fundef itself,
+   because at this point we have that as a separate valspec.*)
+let specialize_annotations instantiation fdef =
   let open Type_check in
   let rw_pat = {
       id_pat_alg with
@@ -364,11 +365,20 @@ let specialize_annotations instantiation =
       lEXP_cast = (fun (typ, lexp) -> LEXP_cast (subst_unifiers instantiation typ, lexp));
       pat_alg = rw_pat
     } in
-  rewrite_fun {
-      rewriters_base with
-      rewrite_exp = (fun _ -> fold_exp rw_exp);
-      rewrite_pat = (fun _ -> fold_pat rw_pat)
-    }
+  let fdef =
+    rewrite_fun {
+        rewriters_base with
+        rewrite_exp = (fun _ -> fold_exp rw_exp);
+        rewrite_pat = (fun _ -> fold_pat rw_pat)
+      } fdef
+  in
+  match fdef with
+  | FD_aux (FD_function (rec_opt, _, eff_opt, funcls), annot) ->
+     FD_aux (FD_function (rec_opt,
+                          Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown),
+                          eff_opt,
+                          funcls),
+             annot)
 
 let specialize_id_fundef instantiations id ast =
   match split_defs (is_fundef id) ast with