PAnnot does not introduce new type variables.

This commit is contained in:
Olivier 2023-03-15 09:26:42 +01:00
parent d930badf40
commit 0f2f30d6a2
4 changed files with 16 additions and 12 deletions

View File

@ -617,17 +617,12 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
| ML.PWildcard loc ->
k ([], pure (F.PWildcard loc))
| ML.PAnnot (loc, pat, (rigidity, vars, ty)) ->
| ML.PAnnot (loc, pat, (rigidity, [], ty)) ->
begin match rigidity with
| ML.Rigid ->
failwith "Rigid variables are not supported in pattern annotation"
| ML.Flexible ->
let@ params =
vars |> mapM_now (fun alpha k ->
let@ v = exist in k(alpha,v)
)
in
let@ v = convert typedecl_env rigid_env params ty in
let@ v = convert typedecl_env rigid_env [] ty in
let@ (pat_env, pat) = hastype_pat typedecl_env rigid_env pat v in
let+ () = v -- w
and+ res = k (pat_env,
@ -636,6 +631,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
in F.PAnnot(loc, pat, ty'))
in res
end
| ML.PAnnot (_, _, (_, _, _)) ->
assert false
| ML.PTuple (loc, pats) ->

View File

@ -53,6 +53,9 @@ let unit =
let for_ tyvars t =
ML.For (None, tyvars, t)
let some_ tyvars t =
ML.Some_ (None, tyvars, t)
let annot t ty_annot =
ML.Annot (None, t, ty_annot)
@ -180,12 +183,13 @@ let match_some = ML.(
)
let match_some_annotated = ML.(
some_ ["'a"] @@
Match (None, some, [
( PVariant (None, Datatype.Label "None", None), none );
( PAnnot (None,
PVariant (None, Datatype.Label "Some",
Some (PWildcard None)),
(Flexible, ["'a"], TyConstr (None, Datatype.Type "option",
(Flexible, [], TyConstr (None, Datatype.Type "option",
[ TyVar (None, "'a") ]))),
none );
])
@ -493,9 +497,10 @@ let test_match_some () =
let test_match_some_annotated () =
test_ok
~typedecl:option_env_str
{|match Some (fun x -> x) with
{| some 'a in
match Some (fun x -> x) with
| None -> None
| (Some _ : some 'a. option 'a) -> None
| (Some _ : option 'a) -> None
end|}
match_some_annotated

View File

@ -1,7 +1,8 @@
#use option.midml
let _ =
some 'a in
match Some (fun x -> x) with
| None -> None
| (Some _ : some 'a. option 'a) -> None
| (Some _ : option 'a) -> None
end

View File

@ -349,9 +349,10 @@ Variable scope escape
#use option.midml
let _ =
some 'a in
match Some (fun x -> x) with
| None -> None
| (Some _ : some 'a. option 'a) -> None
| (Some _ : option 'a) -> None
end
$ midml match-some-annotated.midml