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 /src | |
| 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.
Diffstat (limited to 'src')
| -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 |