Mark tvars as invariant

This commit is contained in:
Gaith Hallak 2022-02-24 17:17:15 +04:00
parent 1980eb30bf
commit 8e888430d9
2 changed files with 13 additions and 14 deletions

View File

@ -809,7 +809,7 @@ infer(Contracts, Options) ->
ets_new(defined_contracts, [bag]),
ets_new(type_vars, [set]),
ets_new(type_vars_variance, [set]),
ets_new(uvars_variance, [set]),
ets_new(type_vars_uvar, [set]),
ets_new(warnings, [bag]),
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
check_modifiers(Env, Contracts),
@ -1791,15 +1791,14 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
ResultType = fresh_uvar(Ann),
when_warning(warn_unused_functions,
fun() -> register_function_call(Namespace ++ qname(CurrentFun), Name) end),
% the uvars of tvars are stored so that no variance switching happens
% in between them (e.g. in TC('a => 'a), 'a should be a single type)
case FunType of
{fun_t, _, _, _, {app_t, _, QType, TArgs}} ->
case ets_lookup(type_vars_variance, qname(QType)) of
[{_, Vs}] ->
lists:foreach(fun({{uvar, _, URef}, Variance}) ->
ets_insert(uvars_variance, {URef, invariant})
end, lists:zip(TArgs, Vs));
_ -> ok
end;
{fun_t, _, _, _, {app_t, _, _, TArgs}} ->
lists:foreach(fun({uvar, _, URef}) ->
ets_insert(type_vars_uvar, {URef});
(_) -> ok
end, TArgs);
_ -> ok
end,
unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When),
@ -2716,9 +2715,9 @@ unify0(Env, A, B, Variance0, When) ->
B1 = dereference(unfold_types_in_type(Env, B, Options)),
Variance = case A of
{uvar, _,URef} ->
case ets_lookup(uvars_variance, URef) of
[{_, V}] -> V;
_ -> Variance0
case ets_lookup(type_vars_uvar, URef) of
[_] -> invariant;
_ -> Variance0
end;
_ -> Variance0
end,

View File

@ -105,11 +105,11 @@ main contract Main =
let vj1 : tj(Animal) = TJ(f_a_to_u_to_a) // success
let vj2 : tj(Animal) = TJ(f_a_to_u_to_c) // fail
let vj3 : tj(Animal) = TJ(f_c_to_u_to_a) // fail (TODO)
let vj3 : tj(Animal) = TJ(f_c_to_u_to_a) // fail
let vj4 : tj(Animal) = TJ(f_c_to_u_to_c) // success
let vj5 : tj(Cat) = TJ(f_a_to_u_to_a) // fail
let vj6 : tj(Cat) = TJ(f_a_to_u_to_c) // fail
let vj7 : tj(Cat) = TJ(f_c_to_u_to_a) // fail (TODO)
let vj7 : tj(Cat) = TJ(f_c_to_u_to_a) // fail
let vj8 : tj(Cat) = TJ(f_c_to_u_to_c) // success
let vk01 : tk(Animal, Animal) = TK(f_a_to_a_to_u) // success