Correct handling of type names in contracts

Variables in contracts can either be true type variables or simply names for
types thet are defined in the 'when' clauses. Consider the following example:

-spec foo(X, Options) -> {ok, X} | error when Options :: [{atom(), boolean()}].

Here X is a true variable whereas Options is a name for a type that is defined
in the when clause.

'when' clauses may further use names on the right side. These were not treated
properly by Dialyzer and could be generalized to the term() type. This patch
fixes this issue.

A further issue is the treatment of true type variables, but this is left for
another patch.

3 files changed, 361 insertions, 16 deletions

diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index 2b78b736ab..76f23d00b9 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -344,7 +344,7 @@ insert_constraints([{subtype, Type1, Type2}|Left], Dict) ->
     false ->
       %% A lot of things should change to add supertypes
       throw({error, io_lib:format("First argument of is_subtype constraint "
-				  "must be a type variable\n", [])})
+				  "must be a type variable: ~p\n", [Type1])})
   end;
 insert_constraints([], Dict) -> Dict.
 
@@ -385,9 +385,8 @@ contract_from_form([{type, _L1, bounded_fun,
 		   RecDict, FileLine, TypeAcc, FormAcc) ->
   TypeFun =
     fun(ExpTypes, AllRecords) ->
-	Constr1 = [constraint_from_form(C, RecDict, ExpTypes, AllRecords)
-                   || C <- Constr],
-	VarDict = insert_constraints(Constr1, dict:new()),
+	{Constr1, VarDict} =
+	  process_constraints(Constr, RecDict, ExpTypes, AllRecords),
 	Type = erl_types:t_from_form(Form, RecDict, VarDict),
 	NewType = erl_types:t_solve_remote(Type, ExpTypes, AllRecords),
 	{NewType, Constr1}
@@ -398,18 +397,66 @@ contract_from_form([{type, _L1, bounded_fun,
 contract_from_form([], _RecDict, _FileLine, TypeAcc, FormAcc) ->
   {lists:reverse(TypeAcc), lists:reverse(FormAcc)}.
 
-constraint_from_form({type, _, constraint, [{atom, _, is_subtype},
-					    [Type1, Type2]]}, RecDict,
-                     ExpTypes, AllRecords) ->
-  T1 = erl_types:t_from_form(Type1, RecDict),
-  T2 = erl_types:t_from_form(Type2, RecDict),
-  T3 = erl_types:t_solve_remote(T1, ExpTypes, AllRecords),
-  T4 = erl_types:t_solve_remote(T2, ExpTypes, AllRecords),
-  {subtype, T3, T4};
-constraint_from_form({type, _, constraint, [{atom,_,Name}, List]}, _RecDict,
-                     _ExpTypes, _AllRecords) ->
-  N = length(List),
-  throw({error, io_lib:format("Unsupported type guard ~w/~w\n", [Name, N])}).
+process_constraints(Constrs, RecDict, ExpTypes, AllRecords) ->
+  Init = initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords),
+  constraints_fixpoint(Init, RecDict, ExpTypes, AllRecords).
+
+initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords) ->
+  initialize_constraints(Constrs, RecDict, ExpTypes, AllRecords, []).
+
+initialize_constraints([], _RecDict, _ExpTypes, _AllRecords, Acc) ->
+  Acc;
+initialize_constraints([Constr|Rest], RecDict, ExpTypes, AllRecords, Acc) ->
+  case Constr of
+    {type, _, constraint, [{atom, _, is_subtype}, [Type1, Type2]]} ->
+      T1 = final_form(Type1, RecDict, ExpTypes, AllRecords, dict:new()),
+      Entry = {T1, Type2},
+      initialize_constraints(Rest, RecDict, ExpTypes, AllRecords, [Entry|Acc]);
+    {type, _, constraint, [{atom,_,Name}, List]} ->
+      N = length(List),
+      throw({error,
+	     io_lib:format("Unsupported type guard ~w/~w\n", [Name, N])})
+  end.
+
+constraints_fixpoint(Constrs, RecDict, ExpTypes, AllRecords) ->
+  VarDict =
+    constraints_to_dict(Constrs, RecDict, ExpTypes, AllRecords, dict:new()),
+  constraints_fixpoint(VarDict, Constrs, RecDict, ExpTypes, AllRecords).
+
+constraints_fixpoint(OldVarDict, Constrs, RecDict, ExpTypes, AllRecords) ->
+  NewVarDict =
+    constraints_to_dict(Constrs, RecDict, ExpTypes, AllRecords, OldVarDict),
+  case NewVarDict of
+    OldVarDict ->
+      DictFold =
+	fun(Key, Value, Acc) ->
+	    [{subtype, erl_types:t_var(Key), Value}|Acc]
+	end,
+      FinalConstrs = dict:fold(DictFold, [], NewVarDict),
+      {FinalConstrs, NewVarDict};
+    _Other ->
+      constraints_fixpoint(NewVarDict, Constrs, RecDict, ExpTypes, AllRecords)
+  end.
+
+-define(TYPE_LIMIT, 4).
+
+final_form(Form, RecDict, ExpTypes, AllRecords, VarDict) ->
+  T1 = erl_types:t_from_form(Form, RecDict, VarDict),
+  T2 = erl_types:t_solve_remote(T1, ExpTypes, AllRecords),
+  erl_types:t_limit(T2, ?TYPE_LIMIT).
+
+constraints_to_dict(Constrs, RecDict, ExpTypes, AllRecords, VarDict) ->
+  Subtypes =
+    constraints_to_subs(Constrs, RecDict, ExpTypes, AllRecords, VarDict, []),
+  insert_constraints(Subtypes, dict:new()).
+
+constraints_to_subs([], _RecDict, _ExpTypes, _AllRecords, _VarDict, Acc) ->
+  Acc;
+constraints_to_subs([C|Rest], RecDict, ExpTypes, AllRecords, VarDict, Acc) ->
+  {T1, Form2} = C,
+  T2 = final_form(Form2, RecDict, ExpTypes, AllRecords, VarDict),
+  NewAcc = [{subtype, T1, T2}|Acc],
+  constraints_to_subs(Rest, RecDict, ExpTypes, AllRecords, VarDict, NewAcc).
 
 %% Gets the most general domain of a list of domains of all
 %% the overloaded contracts
diff --git a/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes
new file mode 100644
index 0000000000..8dc0361b0d
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/results/contracts_with_subtypes
@@ -0,0 +1,31 @@
+
+contracts_with_subtypes.erl:106: The call contracts_with_subtypes:rec_arg({'a','b'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:107: The call contracts_with_subtypes:rec_arg({'b','a'}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:108: The call contracts_with_subtypes:rec_arg({'a',{'b','a'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:109: The call contracts_with_subtypes:rec_arg({'b',{'a','b'}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:110: The call contracts_with_subtypes:rec_arg({'a',{'b',{'a','b'}}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:111: The call contracts_with_subtypes:rec_arg({'b',{'a',{'b','a'}}}) breaks the contract (Arg) -> 'ok' when is_subtype(Arg,{'a',A} | {'b',B}), is_subtype(A,'a' | {'b',B}), is_subtype(B,'b' | {'a',A})
+contracts_with_subtypes.erl:142: The pattern 1 can never match the type binary() | string()
+contracts_with_subtypes.erl:145: The pattern 'alpha' can never match the type {'ok',X} | {'ok',X,binary() | string()}
+contracts_with_subtypes.erl:147: The pattern 42 can never match the type {'ok',_} | {'ok',_,binary() | string()}
+contracts_with_subtypes.erl:163: The pattern 'alpha' can never match the type {'ok',X}
+contracts_with_subtypes.erl:165: The pattern 42 can never match the type {'ok',X}
+contracts_with_subtypes.erl:183: The pattern 'alpha' can never match the type {'ok',X}
+contracts_with_subtypes.erl:185: The pattern 42 can never match the type {'ok',X}
+contracts_with_subtypes.erl:202: The pattern 1 can never match the type binary() | string()
+contracts_with_subtypes.erl:205: The pattern {'ok', _} can never match the type {'ok',X,binary() | string()}
+contracts_with_subtypes.erl:206: The pattern 'alpha' can never match the type {'ok',X,binary() | string()}
+contracts_with_subtypes.erl:207: The pattern {'ok', 42} can never match the type {'ok',X,binary() | string()}
+contracts_with_subtypes.erl:208: The pattern 42 can never match the type {'ok',X,binary() | string()}
+contracts_with_subtypes.erl:234: Function flat_ets_new_t/0 has no local return
+contracts_with_subtypes.erl:235: The call contracts_with_subtypes:flat_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,'set' | 'ordered_set' | 'bag' | 'duplicate_bag' | 'public' | 'protected' | 'private' | 'named_table' | {'keypos',integer()} | {'heir',pid(),term()} | {'heir','none'} | {'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed')
+contracts_with_subtypes.erl:23: Invalid type specification for function contracts_with_subtypes:extract2/0. The success typing is () -> 'something'
+contracts_with_subtypes.erl:261: Function factored_ets_new_t/0 has no local return
+contracts_with_subtypes.erl:262: The call contracts_with_subtypes:factored_ets_new(12,[]) breaks the contract (Name,Options) -> atom() when is_subtype(Name,atom()), is_subtype(Options,[Option]), is_subtype(Option,Type | Access | 'named_table' | {'keypos',Pos} | {'heir',Pid::pid(),HeirData} | {'heir','none'} | Tweaks), is_subtype(Type,type()), is_subtype(Access,access()), is_subtype(Tweaks,{'write_concurrency',boolean()} | {'read_concurrency',boolean()} | 'compressed'), is_subtype(Pos,pos_integer()), is_subtype(HeirData,term())
+contracts_with_subtypes.erl:77: The call contracts_with_subtypes:foo1(5) breaks the contract (Arg1) -> Res when is_subtype(Arg1,atom()), is_subtype(Res,atom())
+contracts_with_subtypes.erl:78: The call contracts_with_subtypes:foo2(5) breaks the contract (Arg1) -> Res when is_subtype(Arg1,Arg2), is_subtype(Arg2,atom()), is_subtype(Res,atom())
+contracts_with_subtypes.erl:79: The call contracts_with_subtypes:foo3(5) breaks the contract (Arg1) -> Res when is_subtype(Arg2,atom()), is_subtype(Arg1,Arg2), is_subtype(Res,atom())
+contracts_with_subtypes.erl:7: Invalid type specification for function contracts_with_subtypes:extract/0. The success typing is () -> 'something'
+contracts_with_subtypes.erl:80: The call contracts_with_subtypes:foo4(5) breaks the contract (Type) -> Type when is_subtype(Type,atom())
+contracts_with_subtypes.erl:81: The call contracts_with_subtypes:foo5(5) breaks the contract (Type::atom()) -> Type::atom()
+contracts_with_subtypes.erl:82: The call contracts_with_subtypes:foo6(5) breaks the contract (Type) -> Type when is_subtype(Type,atom())
diff --git a/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl
new file mode 100644
index 0000000000..d72138d509
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/src/contracts_with_subtypes.erl
@@ -0,0 +1,267 @@
+-module(contracts_with_subtypes).
+
+-compile(export_all).
+
+%===============================================================================
+
+-spec extract() -> 'ok'.
+
+extract() ->
+   case dz_extract() of
+       {ok, Val} -> Val;
+       error -> exit(boom)
+   end.
+
+-spec dz_extract() -> RetValue when
+     FileList :: something,
+     RetValue :: {ok, FileList} | error.
+
+dz_extract() -> get(foo).
+
+%-------------------------------------------------------------------------------
+
+-spec extract2() -> 'ok'.
+
+extract2() ->
+   case dz_extract2() of
+       {ok, Val} -> Val;
+       error -> exit(boom)
+   end.
+
+-spec dz_extract2() -> RetValue when
+     RetValue :: {ok, FileList} | error,
+     FileList :: something.
+
+dz_extract2() -> get(foo).
+
+%===============================================================================
+
+-spec foo1(Arg1) -> Res when
+      Arg1 :: atom(),
+      Res  :: atom().
+
+foo1(X) -> X.
+
+-spec foo2(Arg1) -> Res when
+      Arg1 :: Arg2,
+      Arg2 :: atom(),
+      Res  :: atom().
+
+foo2(X) -> X.
+
+-spec foo3(Arg1) -> Res when
+      Arg2 :: atom(),
+      Arg1 :: Arg2,
+      Res  :: atom().
+
+foo3(X) -> X.
+
+-spec foo4(Type) -> Type when is_subtype(Type, atom()).
+
+foo4(X) -> X.
+
+-spec foo5(Type :: atom()) -> Type :: atom().
+
+foo5(X) -> X.
+
+-spec foo6(Type) -> Type when Type :: atom().
+
+foo6(X) -> X.
+
+-spec foo7(Type) -> Type.
+
+foo7(X) -> X.
+
+%-------------------------------------------------------------------------------
+
+bar(1) -> foo1(5);
+bar(2) -> foo2(5);
+bar(3) -> foo3(5);
+bar(4) -> foo4(5);
+bar(5) -> foo5(5);
+bar(6) -> foo6(5);
+bar(7) -> foo7(5).
+
+wrong_foo6() ->
+    b = foo6(a).
+
+%===============================================================================
+
+-spec rec_arg(Arg) -> ok when
+      Arg :: {a, A} | {b, B},
+      A   :: a | {b, B},
+      B   :: b | {a, A}.
+
+rec_arg(X) -> get(X).
+
+c(aa) -> rec_arg({a, a});
+c(bb) -> rec_arg({b, b});
+c(abb) -> rec_arg({a, {b, b}});
+c(baa) -> rec_arg({b, {a, a}});
+c(abaa) -> rec_arg({a, {b, {a, a}}});
+c(babb) -> rec_arg({b, {a, {b, b}}});
+c(ababb) -> rec_arg({a, {b, {a, {b, b}}}});
+c(babaa) -> rec_arg({b, {a, {b, {a, a}}}}).
+
+w(ab) -> rec_arg({a, b});
+w(ba) -> rec_arg({b, a});
+w(aba) -> rec_arg({a, {b, a}});
+w(bab) -> rec_arg({b, {a, b}});
+w(abab) -> rec_arg({a, {b, {a, b}}});
+w(baba) -> rec_arg({b, {a, {b, a}}});
+w(ababa) -> rec_arg({a, {b, {a, {b, a}}}});
+w(babab) -> rec_arg({b, {a, {b, {a, b}}}}).
+
+%===============================================================================
+
+-type dublo(X) :: {X, X}.
+
+-type weird(X,Y) :: {X, Y, X, X}.
+
+-spec forfun(dublo(Var)) -> ok when Var :: atom().
+
+forfun(_) -> ok.
+
+-spec forfun2(weird(Var, Var)) -> ok when Var :: atom().
+
+forfun2(_) -> ok.
+
+%===============================================================================
+
+-spec shallow(X) -> {ok, X} | {ok, X, file:filename()} | err1 | err2.
+
+shallow(X) -> get(X).
+
+st(X) when is_atom(X) ->
+    case shallow(X) of
+	err1 -> ok;
+	err2 -> ok;
+	{ok, X} -> ok;
+	{ok, X, Res} ->
+	    case Res of
+		1      -> bad;
+		_Other -> ok
+	    end;
+	alpha -> bad;
+	{ok, 42} -> bad;
+	42 -> bad
+    end.
+
+%-------------------------------------------------------------------------------
+
+-spec deep(X) -> Ret when
+      Ret :: {ok, X} | Err,
+      Err :: err1 | err2.
+
+deep(X) -> get(X).
+
+dt(X) when is_atom(X) ->
+    case deep(X) of
+	err1 -> ok;
+	err2 -> ok;
+	{ok, X} -> ok;
+	alpha -> bad;
+	{ok, 42} -> bad;
+	42 -> bad
+    end.
+
+%-------------------------------------------------------------------------------
+
+-type local_errors() :: err1 | err2.
+
+-spec deep2(X) -> Ret when
+      Ret :: {ok, X} | Err,
+      Err :: local_errors().
+
+deep2(X) -> get(X).
+
+dt2(X) when is_atom(X) ->
+    case deep2(X) of
+	err1 -> ok;
+	err2 -> ok;
+	{ok, X} -> ok;
+	alpha -> bad;
+	{ok, 42} -> bad;
+	42 -> bad
+    end.
+
+%-------------------------------------------------------------------------------
+
+-spec deep3(X) -> Ret when
+      Ret :: {ok, X, file:filename()} | Err,
+      Err :: local_errors().
+
+deep3(X) -> get(X).
+
+dt3(X) when is_atom(X) ->
+    case deep3(X) of
+	err1 -> ok;
+	err2 -> ok;
+	{ok, X, Res} ->
+	    case Res of
+		1      -> bad;
+		_Other -> ok
+	    end;
+	{ok, X} -> bad;
+	alpha -> bad;
+	{ok, 42} -> bad;
+	42 -> bad
+    end.
+
+%===============================================================================
+
+-spec flat_ets_new(Name, Options) -> atom() when
+      Name :: atom(),
+      Options :: [Option],
+      Option :: set
+              | ordered_set
+              | bag
+              | duplicate_bag
+              | public
+              | protected
+              | private
+              | named_table
+              | {keypos, integer()}
+              | {heir, pid(), term()}
+              | {heir, none}
+              | {write_concurrency, boolean()}
+              | {read_concurrency, boolean()}
+              | compressed.
+
+flat_ets_new(Name, Options) ->
+    get({Name, Options}).
+
+flat_ets_new_t() ->
+    flat_ets_new(12,[]),
+    flat_ets_new({a,b},[]),
+    flat_ets_new(name,[foo]),
+    flat_ets_new(name,{bag}),
+    flat_ets_new(name,bag),
+    ok.
+
+-type access()     :: public | protected | private.
+-type type()       :: set | ordered_set | bag | duplicate_bag.
+
+-spec factored_ets_new(Name, Options) -> atom() when
+      Name :: atom(),
+      Options :: [Option],
+      Option :: Type | Access | named_table | {keypos,Pos}
+              | {heir, Pid :: pid(), HeirData} | {heir, none} | Tweaks,
+      Type :: type(),
+      Access :: access(),
+      Tweaks :: {write_concurrency, boolean()}
+              | {read_concurrency, boolean()}
+              | compressed,
+      Pos :: pos_integer(),
+      HeirData :: term().
+
+factored_ets_new(Name, Options) ->
+    get({Name, Options}).
+
+factored_ets_new_t() ->
+    factored_ets_new(12,[]),
+    factored_ets_new({a,b},[]),
+    factored_ets_new(name,[foo]),
+    factored_ets_new(name,{bag}),
+    factored_ets_new(name,bag),
+    ok.