diff options
| author | Brian Campbell | 2019-01-31 15:20:25 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-01-31 15:24:50 +0000 |
| commit | 88dda99529fd0e151c932ab1bf22b3c101dd8309 (patch) | |
| tree | 8f7ff9c05a65882eb55e71deb54545403fd87333 | |
| parent | 5010b667b59bbe0fbb13747a1d2409a2b859cd7a (diff) | |
Drop type annotations in top-level nexp rewriting in favour of valspecs
otherwise the valspec rewriting will be inconsistent with the type
annotation. Note that the type checker will have introduced valspecs
where necessary.
| -rw-r--r-- | src/monomorphise.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 20c4e386..0a26c8b0 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -4432,7 +4432,11 @@ let rewrite_toplevel_nexps (Defs defs) = | DEF_spec vs -> (match rewrite_valspec vs with | None -> spec_map, def | Some (id, nexp_map, vs) -> Bindings.add id nexp_map spec_map, DEF_spec vs) - | DEF_fundef (FD_aux (FD_function (recopt,tann,eff,funcls),ann)) -> + | DEF_fundef (FD_aux (FD_function (recopt,_,eff,funcls),ann)) -> + (* Type annotations on function definitions will have been turned into + valspecs by type checking, so it should be safe to drop them rather + than updating them. *) + let tann = Typ_annot_opt_aux (Typ_annot_opt_none,Generated Unknown) in spec_map, DEF_fundef (FD_aux (FD_function (recopt,tann,eff,List.map (rewrite_funcl spec_map) funcls),ann)) | _ -> spec_map, def |