dialyzer: Fix a bug in the translation of forms to types

A bug is fixed, but there are more problems.

Modify erl_types.erl like this:

  -define(EXPAND_LIMIT, 500).

and bogus warnings are output (again).

Callbacks and specs are compared (subtype) in dialyzer_behaviour. If
they are expanded to different depths, then invalid warnings can be
generated.

6 files changed, 4530 insertions, 0 deletions

diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/compile_flags.hrl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/compile_flags.hrl
new file mode 100644
index 0000000000..e5ee44ace1
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/compile_flags.hrl
@@ -0,0 +1,2 @@
+-define(AT_LEAST_19, 1).
+-define(AT_LEAST_17, 1).
diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_common.hrl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_common.hrl
new file mode 100644
index 0000000000..c10626c5cc
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_common.hrl
@@ -0,0 +1,55 @@
+%%% Copyright 2010-2013 Manolis Papadakis <[email protected]>,
+%%%                     Eirini Arvaniti <[email protected]>
+%%%                 and Kostis Sagonas <[email protected]>
+%%%
+%%% This file is part of PropEr.
+%%%
+%%% PropEr is free software: you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation, either version 3 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% PropEr is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%%% GNU General Public License for more details.
+%%%
+%%% You should have received a copy of the GNU General Public License
+%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
+
+%%% @copyright 2010-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
+%%% @version {@version}
+%%% @author Manolis Papadakis
+%%% @doc Common parts of user and internal header files
+
+
+%%------------------------------------------------------------------------------
+%% Test generation macros
+%%------------------------------------------------------------------------------
+
+-define(FORALL(X,RawType,Prop), proper:forall(RawType,fun(X) -> Prop end)).
+-define(IMPLIES(Pre,Prop), proper:implies(Pre,?DELAY(Prop))).
+-define(WHENFAIL(Action,Prop), proper:whenfail(?DELAY(Action),?DELAY(Prop))).
+-define(TRAPEXIT(Prop), proper:trapexit(?DELAY(Prop))).
+-define(TIMEOUT(Limit,Prop), proper:timeout(Limit,?DELAY(Prop))).
+%% TODO: -define(ALWAYS(Tests,Prop), proper:always(Tests,?DELAY(Prop))).
+%% TODO: -define(SOMETIMES(Tests,Prop), proper:sometimes(Tests,?DELAY(Prop))).
+
+
+%%------------------------------------------------------------------------------
+%% Generator macros
+%%------------------------------------------------------------------------------
+
+-define(FORCE(X), (X)()).
+-define(DELAY(X), fun() -> X end).
+-define(LAZY(X), proper_types:lazy(?DELAY(X))).
+-define(SIZED(SizeArg,Gen), proper_types:sized(fun(SizeArg) -> Gen end)).
+-define(LET(X,RawType,Gen), proper_types:bind(RawType,fun(X) -> Gen end,false)).
+-define(SHRINK(Gen,AltGens),
+	proper_types:shrinkwith(?DELAY(Gen),?DELAY(AltGens))).
+-define(LETSHRINK(Xs,RawType,Gen),
+	proper_types:bind(RawType,fun(Xs) -> Gen end,true)).
+-define(SUCHTHAT(X,RawType,Condition),
+	proper_types:add_constraint(RawType,fun(X) -> Condition end,true)).
+-define(SUCHTHATMAYBE(X,RawType,Condition),
+	proper_types:add_constraint(RawType,fun(X) -> Condition end,false)).
diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_gen.erl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_gen.erl
new file mode 100644
index 0000000000..b64a139e4d
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_gen.erl
@@ -0,0 +1,611 @@
+%%% Copyright 2010-2015 Manolis Papadakis <[email protected]>,
+%%%                     Eirini Arvaniti <[email protected]>
+%%%                 and Kostis Sagonas <[email protected]>
+%%%
+%%% This file is part of PropEr.
+%%%
+%%% PropEr is free software: you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation, either version 3 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% PropEr is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%%% GNU General Public License for more details.
+%%%
+%%% You should have received a copy of the GNU General Public License
+%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
+
+%%% @copyright 2010-2015 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
+%%% @version {@version}
+%%% @author Manolis Papadakis
+
+%%% @doc Generator subsystem and generators for basic types.
+%%%
+%%% You can use <a href="#index">these</a> functions to try out the random
+%%% instance generation and shrinking subsystems.
+%%%
+%%% CAUTION: These functions should never be used inside properties. They are
+%%% meant for demonstration purposes only.
+
+-module(proper_gen).
+-export([pick/1, pick/2, pick/3,
+	 sample/1, sample/3, sampleshrink/1, sampleshrink/2]).
+
+-export([safe_generate/1]).
+-export([generate/1, normal_gen/1, alt_gens/1, clean_instance/1,
+	 get_ret_type/1]).
+-export([integer_gen/3, float_gen/3, atom_gen/1, atom_rev/1, binary_gen/1,
+	 binary_rev/1, binary_len_gen/1, bitstring_gen/1, bitstring_rev/1,
+	 bitstring_len_gen/1, list_gen/2, distlist_gen/3, vector_gen/2,
+	 union_gen/1, weighted_union_gen/1, tuple_gen/1, loose_tuple_gen/2,
+	 loose_tuple_rev/2, exactly_gen/1, fixed_list_gen/1, function_gen/2,
+	 any_gen/1, native_type_gen/2, safe_weighted_union_gen/1,
+	 safe_union_gen/1]).
+
+-export_type([instance/0, imm_instance/0, sized_generator/0, nosize_generator/0,
+	      generator/0, reverse_gen/0, combine_fun/0, alt_gens/0]).
+
+-include("proper_internal.hrl").
+
+%%-----------------------------------------------------------------------------
+%% Types
+%%-----------------------------------------------------------------------------
+
+%% TODO: update imm_instance() when adding more types: be careful when reading
+%%	 anything that returns it
+%% @private_type
+-type imm_instance() :: proper_types:raw_type()
+		      | instance()
+		      | {'$used', imm_instance(), imm_instance()}
+		      | {'$to_part', imm_instance()}.
+-type instance() :: term().
+%% A value produced by the random instance generator.
+-type error_reason() :: 'arity_limit' | 'cant_generate' | {'typeserver',term()}.
+
+%% @private_type
+-type sized_generator() :: fun((size()) -> imm_instance()).
+%% @private_type
+-type typed_sized_generator() :: {'typed',
+                                  fun((proper_types:type(),size()) ->
+                                      imm_instance())}.
+%% @private_type
+-type nosize_generator() :: fun(() -> imm_instance()).
+%% @private_type
+-type typed_nosize_generator() :: {'typed',
+                                   fun((proper_types:type()) ->
+                                       imm_instance())}.
+%% @private_type
+-type generator() :: sized_generator()
+                   | typed_sized_generator()
+                   | nosize_generator()
+                   | typed_nosize_generator().
+%% @private_type
+-type plain_reverse_gen() :: fun((instance()) -> imm_instance()).
+%% @private_type
+-type typed_reverse_gen() :: {'typed',
+                              fun((proper_types:type(),instance()) ->
+                                  imm_instance())}.
+%% @private_type
+-type reverse_gen() :: plain_reverse_gen() | typed_reverse_gen().
+%% @private_type
+-type combine_fun() :: fun((instance()) -> imm_instance()).
+%% @private_type
+-type alt_gens() :: fun(() -> [imm_instance()]).
+%% @private_type
+-type fun_seed() :: {non_neg_integer(),non_neg_integer()}.
+
+
+%%-----------------------------------------------------------------------------
+%% Instance generation functions
+%%-----------------------------------------------------------------------------
+
+%% @private
+-spec safe_generate(proper_types:raw_type()) ->
+	  {'ok',imm_instance()} | {'error',error_reason()}.
+safe_generate(RawType) ->
+    try generate(RawType) of
+	ImmInstance -> {ok, ImmInstance}
+    catch
+	throw:'$arity_limit'            -> {error, arity_limit};
+	throw:'$cant_generate'          -> {error, cant_generate};
+	throw:{'$typeserver',SubReason} -> {error, {typeserver,SubReason}}
+    end.
+
+%% @private
+-spec generate(proper_types:raw_type()) -> imm_instance().
+generate(RawType) ->
+    Type = proper_types:cook_outer(RawType),
+    ok = add_parameters(Type),
+    Instance = generate(Type, get('$constraint_tries'), none),
+    ok = remove_parameters(Type),
+    Instance.
+
+-spec add_parameters(proper_types:type()) -> 'ok'.
+add_parameters(Type) ->
+    case proper_types:find_prop(parameters, Type) of
+	{ok, Params} ->
+	    OldParams = erlang:get('$parameters'),
+	    case OldParams of
+		undefined ->
+		    erlang:put('$parameters', Params);
+		_ ->
+		    erlang:put('$parameters', Params ++ OldParams)
+	    end,
+	    ok;
+	_ ->
+	    ok
+    end.
+
+-spec remove_parameters(proper_types:type()) -> 'ok'.
+remove_parameters(Type) ->
+    case proper_types:find_prop(parameters, Type) of
+	{ok, Params} ->
+	    AllParams = erlang:get('$parameters'),
+	    case AllParams of
+		Params->
+		    erlang:erase('$parameters');
+	        _ ->
+		    erlang:put('$parameters', AllParams -- Params)
+	    end,
+	    ok;
+	_ ->
+	    ok
+    end.
+
+-spec generate(proper_types:type(), non_neg_integer(),
+	       'none' | {'ok',imm_instance()}) -> imm_instance().
+generate(_Type, 0, none) ->
+    throw('$cant_generate');
+generate(_Type, 0, {ok,Fallback}) ->
+    Fallback;
+generate(Type, TriesLeft, Fallback) ->
+    ImmInstance =
+	case proper_types:get_prop(kind, Type) of
+	    constructed ->
+		PartsType = proper_types:get_prop(parts_type, Type),
+		Combine = proper_types:get_prop(combine, Type),
+		ImmParts = generate(PartsType),
+		Parts = clean_instance(ImmParts),
+		ImmInstance1 = Combine(Parts),
+		%% TODO: We can just generate the internal type: if it's not
+		%%       a type, it will turn into an exactly.
+		ImmInstance2 =
+		    case proper_types:is_raw_type(ImmInstance1) of
+			true  -> generate(ImmInstance1);
+			false -> ImmInstance1
+		    end,
+		{'$used',ImmParts,ImmInstance2};
+	    _ ->
+		ImmInstance1 = normal_gen(Type),
+		case proper_types:is_raw_type(ImmInstance1) of
+		    true  -> generate(ImmInstance1);
+		    false -> ImmInstance1
+		end
+	end,
+    case proper_types:satisfies_all(clean_instance(ImmInstance), Type) of
+	{_,true}      -> ImmInstance;
+	{true,false}  -> generate(Type, TriesLeft - 1, {ok,ImmInstance});
+	{false,false} -> generate(Type, TriesLeft - 1, Fallback)
+    end.
+
+%% @equiv pick(Type, 10)
+-spec pick(Type::proper_types:raw_type()) -> {'ok',instance()} | 'error'.
+pick(RawType) ->
+    pick(RawType, 10).
+
+%% @equiv pick(Type, Size, os:timestamp())
+-spec pick(Type::proper_types:raw_type(), size()) -> {'ok',instance()} | 'error'.
+pick(RawType, Size) ->
+    pick(RawType, Size, os:timestamp()).
+
+%% @doc Generates a random instance of `Type', of size `Size' with seed `Seed'.
+-spec pick(Type::proper_types:raw_type(), size(), seed()) ->
+	  {'ok',instance()} | 'error'.
+pick(RawType, Size, Seed) ->
+    proper:global_state_init_size_seed(Size, Seed),
+    case clean_instance(safe_generate(RawType)) of
+	{ok,Instance} = Result ->
+	    Msg = "WARNING: Some garbage has been left in the process registry "
+		  "and the code server~n"
+		  "to allow for the returned function(s) to run normally.~n"
+		  "Please run proper:global_state_erase() when done.~n",
+	    case contains_fun(Instance) of
+		true  -> io:format(Msg, []);
+		false -> proper:global_state_erase()
+	    end,
+	    Result;
+	{error,Reason} ->
+	    proper:report_error(Reason, fun io:format/2),
+	    proper:global_state_erase(),
+	    error
+    end.
+
+%% @equiv sample(Type, 10, 20)
+-spec sample(Type::proper_types:raw_type()) -> 'ok'.
+sample(RawType) ->
+    sample(RawType, 10, 20).
+
+%% @doc Generates and prints one random instance of `Type' for each size from
+%% `StartSize' up to `EndSize'.
+-spec sample(Type::proper_types:raw_type(), size(), size()) -> 'ok'.
+sample(RawType, StartSize, EndSize) when StartSize =< EndSize ->
+    Tests = EndSize - StartSize + 1,
+    Prop = ?FORALL(X, RawType, begin io:format("~p~n",[X]), true end),
+    Opts = [quiet,{start_size,StartSize},{max_size,EndSize},{numtests,Tests}],
+    _ = proper:quickcheck(Prop, Opts),
+    ok.
+
+%% @equiv sampleshrink(Type, 10)
+-spec sampleshrink(Type::proper_types:raw_type()) -> 'ok'.
+sampleshrink(RawType) ->
+    sampleshrink(RawType, 10).
+
+%% @doc Generates a random instance of `Type', of size `Size', then shrinks it
+%% as far as it goes. The value produced on each step of the shrinking process
+%% is printed on the screen.
+-spec sampleshrink(Type::proper_types:raw_type(), size()) -> 'ok'.
+sampleshrink(RawType, Size) ->
+    proper:global_state_init_size(Size),
+    Type = proper_types:cook_outer(RawType),
+    case safe_generate(Type) of
+	{ok,ImmInstance} ->
+	    Shrunk = keep_shrinking(ImmInstance, [], Type),
+	    PrintInst = fun(I) -> io:format("~p~n",[clean_instance(I)]) end,
+	    lists:foreach(PrintInst, Shrunk);
+	{error,Reason} ->
+	    proper:report_error(Reason, fun io:format/2)
+    end,
+    proper:global_state_erase(),
+    ok.
+
+-spec keep_shrinking(imm_instance(), [imm_instance()], proper_types:type()) ->
+	  [imm_instance(),...].
+keep_shrinking(ImmInstance, Acc, Type) ->
+    keep_shrinking(ImmInstance, Acc, Type, init).
+
+keep_shrinking(ImmInstance, Acc, Type, State) ->
+    case proper_shrink:shrink(ImmInstance, Type, State) of
+	{[], done} -> %% no more shrinkers
+	    lists:reverse([ImmInstance|Acc]);
+	{[], NewState} ->
+	    %% try next shrinker
+	    keep_shrinking(ImmInstance, Acc, Type, NewState);
+	{[Shrunk|_Rest], _NewState} ->
+        Acc2 = [ImmInstance|Acc],
+        case lists:member(Shrunk, Acc2) of
+            true ->
+                %% Avoid infinite loops
+                lists:reverse(Acc2);
+            false ->
+                keep_shrinking(Shrunk, Acc2, Type)
+        end
+    end.
+
+-spec contains_fun(term()) -> boolean().
+contains_fun(List) when is_list(List) ->
+    proper_arith:safe_any(fun contains_fun/1, List);
+contains_fun(Tuple) when is_tuple(Tuple) ->
+    contains_fun(tuple_to_list(Tuple));
+contains_fun(Fun) when is_function(Fun) ->
+    true;
+contains_fun(_Term) ->
+    false.
+
+
+%%-----------------------------------------------------------------------------
+%% Utility functions
+%%-----------------------------------------------------------------------------
+
+%% @private
+-spec normal_gen(proper_types:type()) -> imm_instance().
+normal_gen(Type) ->
+    case proper_types:get_prop(generator, Type) of
+        {typed, Gen} ->
+            if
+                is_function(Gen, 1) -> Gen(Type);
+                is_function(Gen, 2) -> Gen(Type, proper:get_size(Type))
+            end;
+        Gen ->
+            if
+                is_function(Gen, 0) -> Gen();
+                is_function(Gen, 1) -> Gen(proper:get_size(Type))
+            end
+    end.
+
+%% @private
+-spec alt_gens(proper_types:type()) -> [imm_instance()].
+alt_gens(Type) ->
+    case proper_types:find_prop(alt_gens, Type) of
+	{ok, AltGens} -> ?FORCE(AltGens);
+	error         -> []
+    end.
+
+%% @private
+-spec clean_instance(imm_instance()) -> instance().
+clean_instance({'$used',_ImmParts,ImmInstance}) ->
+    clean_instance(ImmInstance);
+clean_instance({'$to_part',ImmInstance}) ->
+    clean_instance(ImmInstance);
+clean_instance(ImmInstance) ->
+    if
+	is_list(ImmInstance) ->
+	    %% CAUTION: this must handle improper lists
+	    proper_arith:safe_map(fun clean_instance/1, ImmInstance);
+	is_tuple(ImmInstance) ->
+	    proper_arith:tuple_map(fun clean_instance/1, ImmInstance);
+	true ->
+	    ImmInstance
+    end.
+
+
+%%-----------------------------------------------------------------------------
+%% Basic type generators
+%%-----------------------------------------------------------------------------
+
+%% @private
+-spec integer_gen(size(), proper_types:extint(), proper_types:extint()) ->
+	  integer().
+integer_gen(Size, inf, inf) ->
+    proper_arith:rand_int(Size);
+integer_gen(Size, inf, High) ->
+    High - proper_arith:rand_non_neg_int(Size);
+integer_gen(Size, Low, inf) ->
+    Low + proper_arith:rand_non_neg_int(Size);
+integer_gen(Size, Low, High) ->
+    proper_arith:smart_rand_int(Size, Low, High).
+
+%% @private
+-spec float_gen(size(), proper_types:extnum(), proper_types:extnum()) ->
+	  float().
+float_gen(Size, inf, inf) ->
+    proper_arith:rand_float(Size);
+float_gen(Size, inf, High) ->
+    High - proper_arith:rand_non_neg_float(Size);
+float_gen(Size, Low, inf) ->
+    Low + proper_arith:rand_non_neg_float(Size);
+float_gen(_Size, Low, High) ->
+    proper_arith:rand_float(Low, High).
+
+%% @private
+-spec atom_gen(size()) -> proper_types:type().
+%% We make sure we never clash with internal atoms by checking that the first
+%% character is not '$'.
+atom_gen(Size) ->
+    ?LET(Str,
+	 ?SUCHTHAT(X,
+		   proper_types:resize(Size,
+				       proper_types:list(proper_types:byte())),
+		   X =:= [] orelse hd(X) =/= $$),
+	 list_to_atom(Str)).
+
+%% @private
+-spec atom_rev(atom()) -> imm_instance().
+atom_rev(Atom) ->
+    {'$used', atom_to_list(Atom), Atom}.
+
+%% @private
+-spec binary_gen(size()) -> proper_types:type().
+binary_gen(Size) ->
+    ?LET(Bytes,
+	 proper_types:resize(Size,
+			     proper_types:list(proper_types:byte())),
+	 list_to_binary(Bytes)).
+
+%% @private
+-spec binary_rev(binary()) -> imm_instance().
+binary_rev(Binary) ->
+    {'$used', binary_to_list(Binary), Binary}.
+
+%% @private
+-spec binary_len_gen(length()) -> proper_types:type().
+binary_len_gen(Len) ->
+    ?LET(Bytes,
+	 proper_types:vector(Len, proper_types:byte()),
+	 list_to_binary(Bytes)).
+
+%% @private
+-spec bitstring_gen(size()) -> proper_types:type().
+bitstring_gen(Size) ->
+    ?LET({BytesHead, NumBits, TailByte},
+	 {proper_types:resize(Size,proper_types:binary()),
+	  proper_types:range(0,7), proper_types:range(0,127)},
+	 <<BytesHead/binary, TailByte:NumBits>>).
+
+%% @private
+-spec bitstring_rev(bitstring()) -> imm_instance().
+bitstring_rev(BitString) ->
+    List = bitstring_to_list(BitString),
+    {BytesList, BitsTail} = lists:splitwith(fun erlang:is_integer/1, List),
+    {NumBits, TailByte} = case BitsTail of
+			      []     -> {0, 0};
+			      [Bits] -> N = bit_size(Bits),
+					<<Byte:N>> = Bits,
+					{N, Byte}
+			  end,
+    {'$used',
+     {{'$used',BytesList,list_to_binary(BytesList)}, NumBits, TailByte},
+     BitString}.
+
+%% @private
+-spec bitstring_len_gen(length()) -> proper_types:type().
+bitstring_len_gen(Len) ->
+    BytesLen = Len div 8,
+    BitsLen = Len rem 8,
+    ?LET({BytesHead, NumBits, TailByte},
+	 {proper_types:binary(BytesLen), BitsLen,
+	  proper_types:range(0, 1 bsl BitsLen - 1)},
+	  <<BytesHead/binary, TailByte:NumBits>>).
+
+%% @private
+-spec list_gen(size(), proper_types:type()) -> [imm_instance()].
+list_gen(Size, ElemType) ->
+    Len = proper_arith:rand_int(0, Size),
+    vector_gen(Len, ElemType).
+
+%% @private
+-spec distlist_gen(size(), sized_generator(), boolean()) -> [imm_instance()].
+distlist_gen(RawSize, Gen, NonEmpty) ->
+    Len = case NonEmpty of
+	      true  -> proper_arith:rand_int(1, erlang:max(1,RawSize));
+	      false -> proper_arith:rand_int(0, RawSize)
+	  end,
+    Size = case Len of
+	       1 -> RawSize - 1;
+	       _ -> RawSize
+	   end,
+    %% TODO: this produces a lot of types: maybe a simple 'div' is sufficient?
+    Sizes = proper_arith:distribute(Size, Len),
+    InnerTypes = [Gen(S) || S <- Sizes],
+    fixed_list_gen(InnerTypes).
+
+%% @private
+-spec vector_gen(length(), proper_types:type()) -> [imm_instance()].
+vector_gen(Len, ElemType) ->
+    vector_gen_tr(Len, ElemType, []).
+
+-spec vector_gen_tr(length(), proper_types:type(), [imm_instance()]) ->
+	  [imm_instance()].
+vector_gen_tr(0, _ElemType, AccList) ->
+    AccList;
+vector_gen_tr(Left, ElemType, AccList) ->
+    vector_gen_tr(Left - 1, ElemType, [generate(ElemType) | AccList]).
+
+%% @private
+-spec union_gen([proper_types:type(),...]) -> imm_instance().
+union_gen(Choices) ->
+    {_Choice,Type} = proper_arith:rand_choose(Choices),
+    generate(Type).
+
+%% @private
+-spec weighted_union_gen([{frequency(),proper_types:type()},...]) ->
+	  imm_instance().
+weighted_union_gen(FreqChoices) ->
+    {_Choice,Type} = proper_arith:freq_choose(FreqChoices),
+    generate(Type).
+
+%% @private
+-spec safe_union_gen([proper_types:type(),...]) -> imm_instance().
+safe_union_gen(Choices) ->
+    {Choice,Type} = proper_arith:rand_choose(Choices),
+    try generate(Type)
+    catch
+	error:_ ->
+	    safe_union_gen(proper_arith:list_remove(Choice, Choices))
+    end.
+
+%% @private
+-spec safe_weighted_union_gen([{frequency(),proper_types:type()},...]) ->
+         imm_instance().
+safe_weighted_union_gen(FreqChoices) ->
+    {Choice,Type} = proper_arith:freq_choose(FreqChoices),
+    try generate(Type)
+    catch
+	error:_ ->
+	    safe_weighted_union_gen(proper_arith:list_remove(Choice,
+							     FreqChoices))
+    end.
+
+%% @private
+-spec tuple_gen([proper_types:type()]) -> tuple().
+tuple_gen(Fields) ->
+    list_to_tuple(fixed_list_gen(Fields)).
+
+%% @private
+-spec loose_tuple_gen(size(), proper_types:type()) -> proper_types:type().
+loose_tuple_gen(Size, ElemType) ->
+    ?LET(L,
+	 proper_types:resize(Size, proper_types:list(ElemType)),
+	 list_to_tuple(L)).
+
+%% @private
+-spec loose_tuple_rev(tuple(), proper_types:type()) -> imm_instance().
+loose_tuple_rev(Tuple, ElemType) ->
+    CleanList = tuple_to_list(Tuple),
+    List = case proper_types:find_prop(reverse_gen, ElemType) of
+                {ok,{typed, ReverseGen}} ->
+                    [ReverseGen(ElemType,X) || X <- CleanList];
+                {ok,ReverseGen} -> [ReverseGen(X) || X <- CleanList];
+                error           -> CleanList
+            end,
+    {'$used', List, Tuple}.
+
+%% @private
+-spec exactly_gen(T) -> T.
+exactly_gen(X) ->
+    X.
+
+%% @private
+-spec fixed_list_gen([proper_types:type()]) -> imm_instance()
+		  ; ({[proper_types:type()],proper_types:type()}) ->
+	  maybe_improper_list(imm_instance(), imm_instance() | []).
+fixed_list_gen({ProperHead,ImproperTail}) ->
+    [generate(F) || F <- ProperHead] ++ generate(ImproperTail);
+fixed_list_gen(ProperFields) ->
+    [generate(F) || F <- ProperFields].
+
+%% @private
+-spec function_gen(arity(), proper_types:type()) -> function().
+function_gen(Arity, RetType) ->
+    FunSeed = {proper_arith:rand_int(0, ?SEED_RANGE - 1),
+	       proper_arith:rand_int(0, ?SEED_RANGE - 1)},
+    create_fun(Arity, RetType, FunSeed).
+
+%% @private
+-spec any_gen(size()) -> imm_instance().
+any_gen(Size) ->
+    case get('$any_type') of
+	undefined      -> real_any_gen(Size);
+	{type,AnyType} -> generate(proper_types:resize(Size, AnyType))
+    end.
+
+-spec real_any_gen(size()) -> imm_instance().
+real_any_gen(0) ->
+    SimpleTypes = [proper_types:integer(), proper_types:float(),
+		   proper_types:atom()],
+    union_gen(SimpleTypes);
+real_any_gen(Size) ->
+    FreqChoices = [{?ANY_SIMPLE_PROB,simple}, {?ANY_BINARY_PROB,binary},
+		   {?ANY_EXPAND_PROB,expand}],
+    case proper_arith:freq_choose(FreqChoices) of
+	{_,simple} ->
+	    real_any_gen(0);
+	{_,binary} ->
+	    generate(proper_types:resize(Size, proper_types:bitstring()));
+	{_,expand} ->
+	    %% TODO: statistics of produced terms?
+	    NumElems = proper_arith:rand_int(0, Size - 1),
+	    ElemSizes = proper_arith:distribute(Size - 1, NumElems),
+	    ElemTypes = [?LAZY(real_any_gen(S)) || S <- ElemSizes],
+	    case proper_arith:rand_int(1,2) of
+		1 -> fixed_list_gen(ElemTypes);
+		2 -> tuple_gen(ElemTypes)
+	    end
+    end.
+
+%% @private
+-spec native_type_gen(mod_name(), string()) -> proper_types:type().
+native_type_gen(Mod, TypeStr) ->
+    case proper_typeserver:translate_type({Mod,TypeStr}) of
+	{ok,Type}      -> Type;
+	{error,Reason} -> throw({'$typeserver',Reason})
+    end.
+
+
+%%------------------------------------------------------------------------------
+%% Function-generation functions
+%%------------------------------------------------------------------------------
+
+-spec create_fun(arity(), proper_types:type(), fun_seed()) -> function().
+create_fun(_Arity, _RetType, _FunSeed) ->
+    fun() -> throw('$arity_limit') end.
+
+%% @private
+-spec get_ret_type(function()) -> proper_types:type().
+get_ret_type(Fun) ->
+    {arity,Arity} = erlang:fun_info(Fun, arity),
+    put('$get_ret_type', true),
+    RetType = apply(Fun, lists:duplicate(Arity,dummy)),
+    erase('$get_ret_type'),
+    RetType.
diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_internal.hrl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_internal.hrl
new file mode 100644
index 0000000000..89e6b34296
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_internal.hrl
@@ -0,0 +1,98 @@
+%%% Copyright 2010-2013 Manolis Papadakis <[email protected]>,
+%%%                     Eirini Arvaniti <[email protected]>
+%%%                 and Kostis Sagonas <[email protected]>
+%%%
+%%% This file is part of PropEr.
+%%%
+%%% PropEr is free software: you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation, either version 3 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% PropEr is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%%% GNU General Public License for more details.
+%%%
+%%% You should have received a copy of the GNU General Public License
+%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
+
+%%% @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
+%%% @version {@version}
+%%% @author Manolis Papadakis
+%%% @doc Internal header file: This header is included in all PropEr source
+%%%      files.
+
+-include("compile_flags.hrl").
+-include("proper_common.hrl").
+
+
+%%------------------------------------------------------------------------------
+%% Activate strip_types parse transform
+%%------------------------------------------------------------------------------
+
+-ifdef(NO_TYPES).
+-compile({parse_transform, strip_types}).
+-endif.
+
+%%------------------------------------------------------------------------------
+%% Random generator selection
+%%------------------------------------------------------------------------------
+
+-ifdef(USE_SFMT).
+-define(RANDOM_MOD, sfmt).
+-define(SEED_NAME, sfmt_seed).
+-else.
+-define(RANDOM_MOD, random).
+-define(SEED_NAME, random_seed).
+-endif.
+
+%%------------------------------------------------------------------------------
+%% Macros
+%%------------------------------------------------------------------------------
+
+-define(PROPERTY_PREFIX, "prop_").
+
+
+%%------------------------------------------------------------------------------
+%% Constants
+%%------------------------------------------------------------------------------
+
+-define(SEED_RANGE, 4294967296).
+-define(MAX_ARITY, 20).
+-define(MAX_TRIES_FACTOR, 5).
+-define(ANY_SIMPLE_PROB, 3).
+-define(ANY_BINARY_PROB, 1).
+-define(ANY_EXPAND_PROB, 8).
+-define(SMALL_RANGE_THRESHOLD, 16#FFFF).
+
+
+%%------------------------------------------------------------------------------
+%% Common type aliases
+%%------------------------------------------------------------------------------
+
+%% TODO: Perhaps these should be moved inside modules.
+-type mod_name() :: atom().
+-type fun_name() :: atom().
+-type size() :: non_neg_integer().
+-type length() :: non_neg_integer().
+-type position() :: pos_integer().
+-type frequency() :: pos_integer().
+-type seed() :: {non_neg_integer(), non_neg_integer(), non_neg_integer()}.
+
+-type abs_form()   :: erl_parse:abstract_form().
+-type abs_expr()   :: erl_parse:abstract_expr().
+-type abs_clause() :: erl_parse:abstract_clause().
+
+%% TODO: Replace these with the appropriate types from stdlib.
+-ifdef(AT_LEAST_19).
+-type abs_type() :: erl_parse:abstract_type().
+-type abs_rec_field() :: term().	% erl_parse:af_field_decl().
+-else.
+-type abs_type() :: term().
+-type abs_rec_field() :: term().
+-endif.
+
+-type loose_tuple(T) :: {} | {T} | {T,T} | {T,T,T} | {T,T,T,T} | {T,T,T,T,T}
+		      | {T,T,T,T,T,T} | {T,T,T,T,T,T,T} | {T,T,T,T,T,T,T,T}
+		      | {T,T,T,T,T,T,T,T,T} | {T,T,T,T,T,T,T,T,T,T} | tuple().
diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_types.erl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_types.erl
new file mode 100644
index 0000000000..6b154b813b
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_types.erl
@@ -0,0 +1,1353 @@
+%%% Copyright 2010-2013 Manolis Papadakis <[email protected]>,
+%%%                     Eirini Arvaniti <[email protected]>
+%%%                 and Kostis Sagonas <[email protected]>
+%%%
+%%% This file is part of PropEr.
+%%%
+%%% PropEr is free software: you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation, either version 3 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% PropEr is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%%% GNU General Public License for more details.
+%%%
+%%% You should have received a copy of the GNU General Public License
+%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
+
+%%% @copyright 2010-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
+%%% @version {@version}
+%%% @author Manolis Papadakis
+
+%%% @doc Type manipulation functions and predefined types.
+%%%
+%%% == Basic types ==
+%%% This module defines all the basic types of the PropEr type system as
+%%% functions. See the <a href="#index">function index</a> for an overview.
+%%%
+%%% Types can be combined in tuples or lists to produce other types. Exact
+%%% values (such as exact numbers, atoms, binaries and strings) can be combined
+%%% with types inside such structures, like in this example of the type of a
+%%% tagged tuple: ``{'result', integer()}''.
+%%%
+%%% When including the PropEr header file, all
+%%% <a href="#index">API functions</a> of this module are automatically
+%%% imported, unless `PROPER_NO_IMPORTS' is defined.
+%%%
+%%% == Customized types ==
+%%% The following operators can be applied to basic types in order to produce
+%%% new ones:
+%%%
+%%% <dl>
+%%% <dt>`?LET(<Xs>, <Xs_type>, <In>)'</dt>
+%%% <dd>To produce an instance of this type, all appearances of the variables
+%%%   in `<Xs>' are replaced inside `<In>' by their corresponding values in a
+%%%   randomly generated instance of `<Xs_type>'. It's OK for the `<In>' part to
+%%%   evaluate to a type - in that case, an instance of the inner type is
+%%%   generated recursively.</dd>
+%%% <dt>`?SUCHTHAT(<X>, <Type>, <Condition>)'</dt>
+%%% <dd>This produces a specialization of `<Type>', which only includes those
+%%%   members of `<Type>' that satisfy the constraint `<Condition>' - that is,
+%%%   those members for which the function `fun(<X>) -> <Condition> end' returns
+%%%   `true'. If the constraint is very strict - that is, only a small
+%%%   percentage of instances of `<Type>' pass the test - it will take a lot of
+%%%   tries for the instance generation subsystem to randomly produce a valid
+%%%   instance. This will result in slower testing, and testing may even be
+%%%   stopped short, in case the `constraint_tries' limit is reached (see the
+%%%   "Options" section in the documentation of the {@link proper} module). If
+%%%   this is the case, it would be more appropriate to generate valid instances
+%%%   of the specialized type using the `?LET' macro. Also make sure that even
+%%%   small instances can satisfy the constraint, since PropEr will only try
+%%%   small instances at the start of testing. If this is not possible, you can
+%%%   instruct PropEr to start at a larger size, by supplying a suitable value
+%%%   for the `start_size' option (see the "Options" section in the
+%%%   documentation of the {@link proper} module).</dd>
+%%% <dt>`?SUCHTHATMAYBE(<X>, <Type>, <Condition>)'</dt>
+%%% <dd>Equivalent to the `?SUCHTHAT' macro, but the constraint `<Condition>'
+%%%   is considered non-strict: if the `constraint_tries' limit is reached, the
+%%%   generator will just return an instance of `<Type>' instead of failing,
+%%%   even if that instance doesn't satisfy the constraint.</dd>
+%%% <dt>`?SHRINK(<Generator>, <List_of_alt_gens>)'</dt>
+%%% <dd>This creates a type whose instances are generated by evaluating the
+%%%   statement block `<Generator>' (this may evaluate to a type, which will
+%%%   then be generated recursively). If an instance of such a type is to be
+%%%   shrunk, the generators in `<List_of_alt_gens>' are first run to produce
+%%%   hopefully simpler instances of the type. Thus, the generators in the
+%%%   second argument should be simpler than the default. The simplest ones
+%%%   should be at the front of the list, since those are the generators
+%%%   preferred by the shrinking subsystem. Like the main `<Generator>', the
+%%%   alternatives may also evaluate to a type, which is generated recursively.
+%%%   </dd>
+%%% <dt>`?LETSHRINK(<List_of_variables>, <List_of_types>, <Generator>)'</dt>
+%%% <dd>This is created by combining a `?LET' and a `?SHRINK' macro. Instances
+%%%   are generated by applying a randomly generated list of values inside
+%%%   `<Generator>' (just like a `?LET', with the added constraint that the
+%%%   variables and types must be provided in a list - alternatively,
+%%%   `<List_of_types>' may be a list or vector type). When shrinking instances
+%%%   of such a type, the sub-instances that were combined to produce it are
+%%%   first tried in place of the failing instance.</dd>
+%%% <dt>`?LAZY(<Generator>)'</dt>
+%%% <dd>This construct returns a type whose only purpose is to delay the
+%%%   evaluation of `<Generator>' (`<Generator>' can return a type, which will
+%%%   be generated recursively). Using this, you can simulate the lazy
+%%%   generation of instances:
+%%%   ``` stream() -> ?LAZY(frequency([ {1,[]}, {3,[0|stream()]} ])). '''
+%%%   The above type produces lists of zeroes with an average length of 3. Note
+%%%   that, had we not enclosed the generator with a `?LAZY' macro, the
+%%%   evaluation would continue indefinitely, due to the eager evaluation of
+%%%   the Erlang language.</dd>
+%%% <dt>`non_empty(<List_or_binary_type>)'</dt>
+%%% <dd>See the documentation for {@link non_empty/1}.</dd>
+%%% <dt>`noshrink(<Type>)'</dt>
+%%% <dd>See the documentation for {@link noshrink/1}.</dd>
+%%% <dt>`default(<Default_value>, <Type>)'</dt>
+%%% <dd>See the documentation for {@link default/2}.</dd>
+%%% <dt>`with_parameter(<Parameter>, <Value>, <Type>)'</dt>
+%%% <dd>See the documentation for {@link with_parameter/3}.</dd>
+%%% <dt>`with_parameters(<Param_value_pairs>, <Type>)'</dt>
+%%% <dd>See the documentation for {@link with_parameters/2}.</dd>
+%%% </dl>
+%%%
+%%% == Size manipulation ==
+%%% The following operators are related to the `size' parameter, which controls
+%%% the maximum size of produced instances. The actual size of a produced
+%%% instance is chosen randomly, but can never exceed the value of the `size'
+%%% parameter at the moment of generation. A more accurate definition is the
+%%% following: the maximum instance of `size S' can never be smaller than the
+%%% maximum instance of `size S-1'. The actual size of an instance is measured
+%%% differently for each type: the actual size of a list is its length, while
+%%% the actual size of a tree may be the number of its internal nodes. Some
+%%% types, e.g. unions, have no notion of size, thus their generation is not
+%%% influenced by the value of `size'. The `size' parameter starts at 1 and
+%%% grows automatically during testing.
+%%%
+%%% <dl>
+%%% <dt>`?SIZED(<S>, <Generator>)'</dt>
+%%% <dd>Creates a new type, whose instances are produced by replacing all
+%%%   appearances of the `<S>' parameter inside the statement block
+%%%   `<Generator>' with the value of the `size' parameter. It's OK for the
+%%%   `<Generator>' to return a type - in that case, an instance of the inner
+%%%   type is generated recursively.</dd>
+%%% <dt>`resize(<New_size>, <Type>)'</dt>
+%%% <dd>See the documentation for {@link resize/2}.</dd>
+%%% </dl>
+
+-module(proper_types).
+-export([is_inst/2, is_inst/3]).
+
+-export([integer/2, float/2, atom/0, binary/0, binary/1, bitstring/0,
+	 bitstring/1, list/1, vector/2, union/1, weighted_union/1, tuple/1,
+	 loose_tuple/1, exactly/1, fixed_list/1, function/2, any/0,
+	 shrink_list/1, safe_union/1, safe_weighted_union/1]).
+-export([integer/0, non_neg_integer/0, pos_integer/0, neg_integer/0, range/2,
+	 float/0, non_neg_float/0, number/0, boolean/0, byte/0, char/0,
+	 list/0, tuple/0, string/0, wunion/1, term/0, timeout/0, arity/0]).
+-export([int/0, nat/0, largeint/0, real/0, bool/0, choose/2, elements/1,
+	 oneof/1, frequency/1, return/1, default/2, orderedlist/1, function0/1,
+	 function1/1, function2/1, function3/1, function4/1,
+	 weighted_default/2]).
+-export([resize/2, non_empty/1, noshrink/1]).
+
+-export([cook_outer/1, is_type/1, equal_types/2, is_raw_type/1, to_binary/1,
+	 from_binary/1, get_prop/2, find_prop/2, safe_is_instance/2,
+	 is_instance/2, unwrap/1, weakly/1, strongly/1, satisfies_all/2,
+	 new_type/2, subtype/2]).
+-export([lazy/1, sized/1, bind/3, shrinkwith/2, add_constraint/3,
+	 native_type/2, distlist/3, with_parameter/3, with_parameters/2,
+	 parameter/1, parameter/2]).
+-export([le/2]).
+
+-export_type([type/0, raw_type/0, extint/0, extnum/0]).
+
+-include("proper_internal.hrl").
+
+
+%%------------------------------------------------------------------------------
+%% Comparison with erl_types
+%%------------------------------------------------------------------------------
+
+%% Missing types
+%% -------------------
+%% will do:
+%%	records, maybe_improper_list(T,S), nonempty_improper_list(T,S)
+%%	maybe_improper_list(), maybe_improper_list(T), iolist, iodata
+%% don't need:
+%%	nonempty_{list,string,maybe_improper_list}
+%% won't do:
+%%	pid, port, ref, identifier, none, no_return, module, mfa, node
+%%	array, dict, digraph, set, gb_tree, gb_set, queue, tid
+
+%% Missing type information
+%% ------------------------
+%% bin types:
+%%	other unit sizes? what about size info?
+%% functions:
+%%	generally some fun, unspecified number of arguments but specified
+%%	return type
+%% any:
+%%	doesn't cover functions and improper lists
+
+
+%%------------------------------------------------------------------------------
+%% Type declaration macros
+%%------------------------------------------------------------------------------
+
+-define(BASIC(PropList), new_type(PropList,basic)).
+-define(WRAPPER(PropList), new_type(PropList,wrapper)).
+-define(CONSTRUCTED(PropList), new_type(PropList,constructed)).
+-define(CONTAINER(PropList), new_type(PropList,container)).
+-define(SUBTYPE(Type,PropList), subtype(PropList,Type)).
+
+
+%%------------------------------------------------------------------------------
+%% Types
+%%------------------------------------------------------------------------------
+
+-type type_kind() :: 'basic' | 'wrapper' | 'constructed' | 'container' | atom().
+-type instance_test() :: fun((proper_gen:imm_instance()) -> boolean())
+                       | {'typed',
+                          fun((proper_types:type(),
+                               proper_gen:imm_instance()) -> boolean())}.
+-type index() :: pos_integer().
+%% @alias
+-type value() :: term().
+%% @private_type
+%% @alias
+-type extint()  :: integer() | 'inf'.
+%% @private_type
+%% @alias
+-type extnum()  :: number()  | 'inf'.
+-type constraint_fun() :: fun((proper_gen:instance()) -> boolean()).
+
+-opaque type() :: {'$type', [type_prop()]}.
+%% A type of the PropEr type system
+%% @type raw_type(). You can consider this as an equivalent of {@type type()}.
+-type raw_type() :: type() | [raw_type()] | loose_tuple(raw_type()) | term().
+-type type_prop_name() :: 'kind' | 'generator' | 'reverse_gen' | 'parts_type'
+			| 'combine' | 'alt_gens' | 'shrink_to_parts'
+			| 'size_transform' | 'is_instance' | 'shrinkers'
+			| 'noshrink' | 'internal_type' | 'internal_types'
+			| 'get_length' | 'split' | 'join' | 'get_indices'
+			| 'remove' | 'retrieve' | 'update' | 'constraints'
+			| 'parameters' | 'env' | 'subenv'.
+
+-type type_prop_value() :: term().
+-type type_prop() ::
+      {'kind', type_kind()}
+    | {'generator', proper_gen:generator()}
+    | {'reverse_gen', proper_gen:reverse_gen()}
+    | {'parts_type', type()}
+    | {'combine', proper_gen:combine_fun()}
+    | {'alt_gens', proper_gen:alt_gens()}
+    | {'shrink_to_parts', boolean()}
+    | {'size_transform', fun((size()) -> size())}
+    | {'is_instance', instance_test()}
+    | {'shrinkers', [proper_shrink:shrinker()]}
+    | {'noshrink', boolean()}
+    | {'internal_type', raw_type()}
+    | {'internal_types', tuple() | maybe_improper_list(type(),type() | [])}
+      %% The items returned by 'remove' must be of this type.
+    | {'get_length', fun((proper_gen:imm_instance()) -> length())}
+      %% If this is a container type, this should return the number of elements
+      %% it contains.
+    | {'split', fun((proper_gen:imm_instance()) -> [proper_gen:imm_instance()])
+	      | fun((length(),proper_gen:imm_instance()) ->
+		    {proper_gen:imm_instance(),proper_gen:imm_instance()})}
+      %% If present, the appropriate form depends on whether get_length is
+      %% defined: if get_length is undefined, this must be in the one-argument
+      %% form (e.g. a tree should be split into its subtrees), else it must be
+      %% in the two-argument form (e.g. a list should be split in two at the
+      %% index provided).
+    | {'join', fun((proper_gen:imm_instance(),proper_gen:imm_instance()) ->
+		   proper_gen:imm_instance())}
+    | {'get_indices', fun((proper_types:type(),
+                           proper_gen:imm_instance()) -> [index()])}
+      %% If this is a container type, this should return a list of indices we
+      %% can use to remove or insert elements from the given instance.
+    | {'remove', fun((index(),proper_gen:imm_instance()) ->
+		     proper_gen:imm_instance())}
+    | {'retrieve', fun((index(), proper_gen:imm_instance() | tuple()
+			       | maybe_improper_list(type(),type() | [])) ->
+		       value() | type())}
+    | {'update', fun((index(),value(),proper_gen:imm_instance()) ->
+		     proper_gen:imm_instance())}
+    | {'constraints', [{constraint_fun(), boolean()}]}
+      %% A list of constraints on instances of this type: each constraint is a
+      %% tuple of a fun that must return 'true' for each valid instance and a
+      %% boolean field that specifies whether the condition is strict.
+    | {'parameters', [{atom(),value()}]}
+    | {'env', term()}
+    | {'subenv', term()}.
+
+
+%%------------------------------------------------------------------------------
+%% Type manipulation functions
+%%------------------------------------------------------------------------------
+
+%% TODO: We shouldn't need the fully qualified type name in the range of these
+%%       functions.
+
+%% @private
+%% TODO: just cook/1 ?
+-spec cook_outer(raw_type()) -> proper_types:type().
+cook_outer(Type = {'$type',_Props}) ->
+    Type;
+cook_outer(RawType) ->
+    if
+	is_tuple(RawType) -> tuple(tuple_to_list(RawType));
+	%% CAUTION: this must handle improper lists
+	is_list(RawType)  -> fixed_list(RawType);
+	%% default case (covers integers, floats, atoms, binaries, ...):
+	true              -> exactly(RawType)
+    end.
+
+%% @private
+-spec is_type(term()) -> boolean().
+is_type({'$type',_Props}) ->
+    true;
+is_type(_) ->
+    false.
+
+%% @private
+-spec equal_types(proper_types:type(), proper_types:type()) -> boolean().
+equal_types(SameType, SameType) ->
+    true;
+equal_types(_, _) ->
+    false.
+
+%% @private
+-spec is_raw_type(term()) -> boolean().
+is_raw_type({'$type',_TypeProps}) ->
+    true;
+is_raw_type(X) ->
+    if
+	is_tuple(X) -> is_raw_type_list(tuple_to_list(X));
+	is_list(X)  -> is_raw_type_list(X);
+	true        -> false
+    end.
+
+-spec is_raw_type_list(maybe_improper_list()) -> boolean().
+%% CAUTION: this must handle improper lists
+is_raw_type_list(List) ->
+    proper_arith:safe_any(fun is_raw_type/1, List).
+
+%% @private
+-spec to_binary(proper_types:type()) -> binary().
+to_binary(Type) ->
+    term_to_binary(Type).
+
+%% @private
+-ifdef(AT_LEAST_17).
+-spec from_binary(binary()) -> proper_types:type().
+-endif.
+from_binary(Binary) ->
+    binary_to_term(Binary).
+
+-spec type_from_list([type_prop()]) -> proper_types:type().
+type_from_list(KeyValueList) ->
+    {'$type',KeyValueList}.
+
+-spec add_prop(type_prop_name(), type_prop_value(), proper_types:type()) ->
+	  proper_types:type().
+add_prop(PropName, Value, {'$type',Props}) ->
+    {'$type',lists:keystore(PropName, 1, Props, {PropName, Value})}.
+
+-spec add_props([type_prop()], proper_types:type()) -> proper_types:type().
+add_props(PropList, {'$type',OldProps}) ->
+    {'$type', lists:foldl(fun({N,_}=NV,Acc) ->
+                    lists:keystore(N, 1, Acc, NV)
+                end, OldProps, PropList)}.
+
+-spec append_to_prop(type_prop_name(), type_prop_value(),
+		     proper_types:type()) -> proper_types:type().
+append_to_prop(PropName, Value, {'$type',Props}) ->
+    Val = case lists:keyfind(PropName, 1, Props) of
+        {PropName, V} ->
+            V;
+        _ ->
+            []
+    end,
+    {'$type', lists:keystore(PropName, 1, Props,
+                             {PropName, lists:reverse([Value|Val])})}.
+
+-spec append_list_to_prop(type_prop_name(), [type_prop_value()],
+			  proper_types:type()) -> proper_types:type().
+append_list_to_prop(PropName, List, {'$type',Props}) ->
+    {PropName, Val} = lists:keyfind(PropName, 1, Props),
+    {'$type', lists:keystore(PropName, 1, Props, {PropName, Val++List})}.
+
+%% @private
+-spec get_prop(type_prop_name(), proper_types:type()) -> type_prop_value().
+get_prop(PropName, {'$type',Props}) ->
+    {_PropName, Val} = lists:keyfind(PropName, 1, Props),
+    Val.
+
+%% @private
+-spec find_prop(type_prop_name(), proper_types:type()) ->
+	  {'ok',type_prop_value()} | 'error'.
+find_prop(PropName, {'$type',Props}) ->
+    case lists:keyfind(PropName, 1, Props) of
+        {PropName, Value} ->
+            {ok, Value};
+        _ ->
+            error
+    end.
+
+%% @private
+-spec new_type([type_prop()], type_kind()) -> proper_types:type().
+new_type(PropList, Kind) ->
+    Type = type_from_list(PropList),
+    add_prop(kind, Kind, Type).
+
+%% @private
+-spec subtype([type_prop()], proper_types:type()) -> proper_types:type().
+%% TODO: should the 'is_instance' function etc. be reset for subtypes?
+subtype(PropList, Type) ->
+    add_props(PropList, Type).
+
+%% @private
+-spec is_inst(proper_gen:instance(), raw_type()) ->
+	  boolean() | {'error',{'typeserver',term()}}.
+is_inst(Instance, RawType) ->
+    is_inst(Instance, RawType, 10).
+
+%% @private
+-spec is_inst(proper_gen:instance(), raw_type(), size()) ->
+	  boolean() | {'error',{'typeserver',term()}}.
+is_inst(Instance, RawType, Size) ->
+    proper:global_state_init_size(Size),
+    Result = safe_is_instance(Instance, RawType),
+    proper:global_state_erase(),
+    Result.
+
+%% @private
+-spec safe_is_instance(proper_gen:imm_instance(), raw_type()) ->
+	  boolean() | {'error',{'typeserver',term()}}.
+safe_is_instance(ImmInstance, RawType) ->
+    try is_instance(ImmInstance, RawType) catch
+	throw:{'$typeserver',SubReason} -> {error, {typeserver,SubReason}}
+    end.
+
+%% @private
+-spec is_instance(proper_gen:imm_instance(), raw_type()) -> boolean().
+%% TODO: If the second argument is not a type, let it pass (don't even check for
+%%	 term equality?) - if it's a raw type, don't cook it, instead recurse
+%%	 into it.
+is_instance(ImmInstance, RawType) ->
+    CleanInstance = proper_gen:clean_instance(ImmInstance),
+    Type = cook_outer(RawType),
+    (case get_prop(kind, Type) of
+	 wrapper     -> wrapper_test(ImmInstance, Type);
+	 constructed -> constructed_test(ImmInstance, Type);
+	 _           -> false
+     end
+     orelse
+     case find_prop(is_instance, Type) of
+	 {ok,{typed, IsInstance}} -> IsInstance(Type, ImmInstance);
+	 {ok,IsInstance} -> IsInstance(ImmInstance);
+	 error           -> false
+     end)
+    andalso weakly(satisfies_all(CleanInstance, Type)).
+
+-spec wrapper_test(proper_gen:imm_instance(), proper_types:type()) -> boolean().
+wrapper_test(ImmInstance, Type) ->
+    %% TODO: check if it's actually a raw type that's returned?
+    lists:any(fun(T) -> is_instance(ImmInstance, T) end, unwrap(Type)).
+
+%% @private
+-ifdef(AT_LEAST_17).
+-spec unwrap(proper_types:type()) -> [proper_types:type(),...].
+-endif.
+%% TODO: check if it's actually a raw type that's returned?
+unwrap(Type) ->
+    RawInnerTypes = proper_gen:alt_gens(Type) ++ [proper_gen:normal_gen(Type)],
+    [cook_outer(T) || T <- RawInnerTypes].
+
+-spec constructed_test(proper_gen:imm_instance(), proper_types:type()) ->
+	  boolean().
+constructed_test({'$used',ImmParts,ImmInstance}, Type) ->
+    PartsType = get_prop(parts_type, Type),
+    Combine = get_prop(combine, Type),
+    is_instance(ImmParts, PartsType) andalso
+    begin
+	%% TODO: check if it's actually a raw type that's returned?
+	%% TODO: move construction code to proper_gen
+	%% TODO: non-type => should we check for strict term equality?
+	RawInnerType = Combine(proper_gen:clean_instance(ImmParts)),
+	is_instance(ImmInstance, RawInnerType)
+    end;
+constructed_test({'$to_part',ImmInstance}, Type) ->
+    PartsType = get_prop(parts_type, Type),
+    get_prop(shrink_to_parts, Type) =:= true andalso
+    %% TODO: we reject non-container types
+    get_prop(kind, PartsType) =:= container andalso
+    case {find_prop(internal_type,PartsType),
+	  find_prop(internal_types,PartsType)} of
+	{{ok,EachPartType},error} ->
+	    %% The parts are in a list or a vector.
+	    is_instance(ImmInstance, EachPartType);
+	{error,{ok,PartTypesList}} ->
+	    %% The parts are in a fixed list.
+	    %% TODO: It should always be a proper list.
+	    lists:any(fun(T) -> is_instance(ImmInstance,T) end, PartTypesList)
+    end;
+constructed_test(_CleanInstance, _Type) ->
+    %% TODO: can we do anything better?
+    false.
+
+%% @private
+-spec weakly({boolean(),boolean()}) -> boolean().
+weakly({B1,_B2}) -> B1.
+
+%% @private
+-spec strongly({boolean(),boolean()}) -> boolean().
+strongly({_B1,B2}) -> B2.
+
+-spec satisfies(proper_gen:instance(), {constraint_fun(),boolean()})
+	  -> {boolean(),boolean()}.
+satisfies(Instance, {Test,false}) ->
+    {true,Test(Instance)};
+satisfies(Instance, {Test,true}) ->
+    Result = Test(Instance),
+    {Result,Result}.
+
+%% @private
+-spec satisfies_all(proper_gen:instance(), proper_types:type()) ->
+	  {boolean(),boolean()}.
+satisfies_all(Instance, Type) ->
+    case find_prop(constraints, Type) of
+	{ok, Constraints} ->
+	    L = [satisfies(Instance, C) || C <- Constraints],
+	    {L1,L2} = lists:unzip(L),
+	    {lists:all(fun(B) -> B end, L1), lists:all(fun(B) -> B end, L2)};
+	error ->
+	    {true,true}
+    end.
+
+
+%%------------------------------------------------------------------------------
+%% Type definition functions
+%%------------------------------------------------------------------------------
+
+%% @private
+-spec lazy(proper_gen:nosize_generator()) -> proper_types:type().
+lazy(Gen) ->
+    ?WRAPPER([
+	{generator, Gen}
+    ]).
+
+%% @private
+-spec sized(proper_gen:sized_generator()) -> proper_types:type().
+sized(Gen) ->
+    ?WRAPPER([
+        {generator, Gen}
+    ]).
+
+%% @private
+-spec bind(raw_type(), proper_gen:combine_fun(), boolean()) ->
+	  proper_types:type().
+bind(RawPartsType, Combine, ShrinkToParts) ->
+    PartsType = cook_outer(RawPartsType),
+    ?CONSTRUCTED([
+	{parts_type, PartsType},
+	{combine, Combine},
+	{shrink_to_parts, ShrinkToParts}
+    ]).
+
+%% @private
+-spec shrinkwith(proper_gen:nosize_generator(), proper_gen:alt_gens()) ->
+	  proper_types:type().
+shrinkwith(Gen, DelaydAltGens) ->
+    ?WRAPPER([
+	{generator, Gen},
+	{alt_gens, DelaydAltGens}
+    ]).
+
+%% @private
+-spec add_constraint(raw_type(), constraint_fun(), boolean()) ->
+	  proper_types:type().
+add_constraint(RawType, Condition, IsStrict) ->
+    Type = cook_outer(RawType),
+    append_to_prop(constraints, {Condition,IsStrict}, Type).
+
+%% @private
+-spec native_type(mod_name(), string()) -> proper_types:type().
+native_type(Mod, TypeStr) ->
+    ?WRAPPER([
+	{generator, fun() ->  proper_gen:native_type_gen(Mod,TypeStr) end}
+    ]).
+
+
+%%------------------------------------------------------------------------------
+%% Basic types
+%%------------------------------------------------------------------------------
+
+%% @doc All integers between `Low' and `High', bounds included.
+%% `Low' and `High' must be Erlang expressions that evaluate to integers, with
+%% `Low =< High'. Additionally, `Low' and `High' may have the value `inf', in
+%% which case they represent minus infinity and plus infinity respectively.
+%% Instances shrink towards 0 if `Low =< 0 =< High', or towards the bound with
+%% the smallest absolute value otherwise.
+-spec integer(extint(), extint()) -> proper_types:type().
+integer(Low, High) ->
+    ?BASIC([
+	{env, {Low, High}},
+	{generator, {typed, fun integer_gen/2}},
+	{is_instance, {typed, fun integer_is_instance/2}},
+	{shrinkers, [fun number_shrinker/3]}
+    ]).
+
+integer_gen(Type, Size) ->
+    {Low, High} = get_prop(env, Type),
+    proper_gen:integer_gen(Size, Low, High).
+
+integer_is_instance(Type, X) ->
+    {Low, High} = get_prop(env, Type),
+    is_integer(X) andalso le(Low, X) andalso le(X, High).
+
+number_shrinker(X, Type, S) ->
+    {Low, High} = get_prop(env, Type),
+    proper_shrink:number_shrinker(X, Low, High, S).
+
+%% @doc All floats between `Low' and `High', bounds included.
+%% `Low' and `High' must be Erlang expressions that evaluate to floats, with
+%% `Low =< High'. Additionally, `Low' and `High' may have the value `inf', in
+%% which case they represent minus infinity and plus infinity respectively.
+%% Instances shrink towards 0.0 if `Low =< 0.0 =< High', or towards the bound
+%% with the smallest absolute value otherwise.
+-spec float(extnum(), extnum()) -> proper_types:type().
+float(Low, High) ->
+    ?BASIC([
+	{env, {Low, High}},
+	{generator, {typed, fun float_gen/2}},
+	{is_instance, {typed, fun float_is_instance/2}},
+	{shrinkers, [fun number_shrinker/3]}
+    ]).
+
+float_gen(Type, Size) ->
+    {Low, High} = get_prop(env, Type),
+    proper_gen:float_gen(Size, Low, High).
+
+float_is_instance(Type, X) ->
+    {Low, High} = get_prop(env, Type),
+    is_float(X) andalso le(Low, X) andalso le(X, High).
+
+%% @private
+-spec le(extnum(), extnum()) -> boolean().
+le(inf, _B) -> true;
+le(_A, inf) -> true;
+le(A, B)    -> A =< B.
+
+%% @doc All atoms. All atoms used internally by PropEr start with a '`$'', so
+%% such atoms will never be produced as instances of this type. You should also
+%% refrain from using such atoms in your code, to avoid a potential clash.
+%% Instances shrink towards the empty atom, ''.
+-spec atom() -> proper_types:type().
+atom() ->
+    ?WRAPPER([
+	{generator, fun proper_gen:atom_gen/1},
+	{reverse_gen, fun proper_gen:atom_rev/1},
+	{size_transform, fun(Size) -> erlang:min(Size,255) end},
+	{is_instance, fun atom_is_instance/1}
+    ]).
+
+atom_is_instance(X) ->
+    is_atom(X)
+    %% We return false for atoms starting with '$', since these are
+    %% atoms used internally and never produced by the atom generator.
+    andalso (X =:= '' orelse hd(atom_to_list(X)) =/= $$).
+
+%% @doc All binaries. Instances shrink towards the empty binary, `<<>>'.
+-spec binary() -> proper_types:type().
+binary() ->
+    ?WRAPPER([
+	{generator, fun proper_gen:binary_gen/1},
+	{reverse_gen, fun proper_gen:binary_rev/1},
+	{is_instance, fun erlang:is_binary/1}
+    ]).
+
+%% @doc All binaries with a byte size of `Len'.
+%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
+%% Instances shrink towards binaries of zeroes.
+-spec binary(length()) -> proper_types:type().
+binary(Len) ->
+    ?WRAPPER([
+	{env, Len},
+	{generator, {typed, fun binary_len_gen/1}},
+	{reverse_gen, fun proper_gen:binary_rev/1},
+	{is_instance, {typed, fun binary_len_is_instance/2}}
+    ]).
+
+binary_len_gen(Type) ->
+    Len = get_prop(env, Type),
+    proper_gen:binary_len_gen(Len).
+
+binary_len_is_instance(Type, X) ->
+    Len = get_prop(env, Type),
+    is_binary(X) andalso byte_size(X) =:= Len.
+
+%% @doc All bitstrings. Instances shrink towards the empty bitstring, `<<>>'.
+-spec bitstring() -> proper_types:type().
+bitstring() ->
+    ?WRAPPER([
+	{generator, fun proper_gen:bitstring_gen/1},
+	{reverse_gen, fun proper_gen:bitstring_rev/1},
+	{is_instance, fun erlang:is_bitstring/1}
+    ]).
+
+%% @doc All bitstrings with a bit size of `Len'.
+%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
+%% Instances shrink towards bitstrings of zeroes
+-spec bitstring(length()) -> proper_types:type().
+bitstring(Len) ->
+    ?WRAPPER([
+	{env, Len},
+	{generator, {typed, fun bitstring_len_gen/1}},
+	{reverse_gen, fun proper_gen:bitstring_rev/1},
+	{is_instance, {typed, fun bitstring_len_is_instance/2}}
+    ]).
+
+bitstring_len_gen(Type) ->
+    Len = get_prop(env, Type),
+    proper_gen:bitstring_len_gen(Len).
+
+bitstring_len_is_instance(Type, X) ->
+    Len = get_prop(env, Type),
+    is_bitstring(X) andalso bit_size(X) =:= Len.
+
+%% @doc All lists containing elements of type `ElemType'.
+%% Instances shrink towards the empty list, `[]'.
+-spec list(ElemType::raw_type()) -> proper_types:type().
+% TODO: subtyping would be useful here (list, vector, fixed_list)
+list(RawElemType) ->
+    ElemType = cook_outer(RawElemType),
+    ?CONTAINER([
+	{generator, {typed, fun list_gen/2}},
+	{is_instance, {typed, fun list_is_instance/2}},
+	{internal_type, ElemType},
+	{get_length, fun erlang:length/1},
+	{split, fun lists:split/2},
+	{join, fun lists:append/2},
+	{get_indices, fun list_get_indices/2},
+	{remove, fun proper_arith:list_remove/2},
+	{retrieve, fun lists:nth/2},
+	{update, fun proper_arith:list_update/3}
+    ]).
+
+list_gen(Type, Size) ->
+    ElemType = get_prop(internal_type, Type),
+    proper_gen:list_gen(Size, ElemType).
+
+list_is_instance(Type, X) ->
+    ElemType = get_prop(internal_type, Type),
+    list_test(X, ElemType).
+
+%% @doc A type that generates exactly the list `List'. Instances shrink towards
+%% shorter sublists of the original list.
+-spec shrink_list([term()]) -> proper_types:type().
+shrink_list(List) ->
+    ?CONTAINER([
+	{env, List},
+	{generator, {typed, fun shrink_list_gen/1}},
+	{is_instance, {typed, fun shrink_list_is_instance/2}},
+	{get_length, fun erlang:length/1},
+	{split, fun lists:split/2},
+	{join, fun lists:append/2},
+	{get_indices, fun list_get_indices/2},
+	{remove, fun proper_arith:list_remove/2}
+    ]).
+
+shrink_list_gen(Type) ->
+    get_prop(env, Type).
+
+shrink_list_is_instance(Type, X) ->
+    List = get_prop(env, Type),
+    is_sublist(X, List).
+
+-spec is_sublist([term()], [term()]) -> boolean().
+is_sublist([], _) -> true;
+is_sublist(_, []) -> false;
+is_sublist([H|T1], [H|T2]) -> is_sublist(T1, T2);
+is_sublist(Slice, [_|T2]) -> is_sublist(Slice, T2).
+
+-spec list_test(proper_gen:imm_instance(), proper_types:type()) -> boolean().
+list_test(X, ElemType) ->
+    is_list(X) andalso lists:all(fun(E) -> is_instance(E, ElemType) end, X).
+
+%% @private
+-spec list_get_indices(proper_gen:generator(), list()) -> [position()].
+list_get_indices(_, List) ->
+    lists:seq(1, length(List)).
+
+%% @private
+%% This assumes that:
+%% - instances of size S are always valid instances of size >S
+%% - any recursive calls inside Gen are lazy
+-spec distlist(size(), proper_gen:sized_generator(), boolean()) ->
+	  proper_types:type().
+distlist(Size, Gen, NonEmpty) ->
+    ParentType = case NonEmpty of
+		     true  -> non_empty(list(Gen(Size)));
+		     false -> list(Gen(Size))
+		 end,
+    ?SUBTYPE(ParentType, [
+	{subenv, {Size, Gen, NonEmpty}},
+	{generator, {typed, fun distlist_gen/1}}
+    ]).
+
+distlist_gen(Type) ->
+    {Size, Gen, NonEmpty} = get_prop(subenv, Type),
+    proper_gen:distlist_gen(Size, Gen, NonEmpty).
+
+%% @doc All lists of length `Len' containing elements of type `ElemType'.
+%% `Len' must be an Erlang expression that evaluates to a non-negative integer.
+-spec vector(length(), ElemType::raw_type()) -> proper_types:type().
+vector(Len, RawElemType) ->
+    ElemType = cook_outer(RawElemType),
+    ?CONTAINER([
+	{env, Len},
+	{generator, {typed, fun vector_gen/1}},
+	{is_instance, {typed, fun vector_is_instance/2}},
+	{internal_type, ElemType},
+	{get_indices, fun vector_get_indices/2},
+	{retrieve, fun lists:nth/2},
+	{update, fun proper_arith:list_update/3}
+    ]).
+
+vector_gen(Type) ->
+    Len = get_prop(env, Type),
+    ElemType = get_prop(internal_type, Type),
+    proper_gen:vector_gen(Len, ElemType).
+
+vector_is_instance(Type, X) ->
+    Len = get_prop(env, Type),
+    ElemType = get_prop(internal_type, Type),
+    is_list(X)
+    andalso length(X) =:= Len
+    andalso lists:all(fun(E) -> is_instance(E, ElemType) end, X).
+
+vector_get_indices(Type, _X) ->
+    lists:seq(1, get_prop(env, Type)).
+
+%% @doc The union of all types in `ListOfTypes'. `ListOfTypes' can't be empty.
+%% The random instance generator is equally likely to choose any one of the
+%% types in `ListOfTypes'. The shrinking subsystem will always try to shrink an
+%% instance of a type union to an instance of the first type in `ListOfTypes',
+%% thus you should write the simplest case first.
+-spec union(ListOfTypes::[raw_type(),...]) -> proper_types:type().
+union(RawChoices) ->
+    Choices = [cook_outer(C) || C <- RawChoices],
+    ?BASIC([
+	{env, Choices},
+	{generator, {typed, fun union_gen/1}},
+	{is_instance, {typed, fun union_is_instance/2}},
+	{shrinkers, [fun union_shrinker_1/3, fun union_shrinker_2/3]}
+    ]).
+
+union_gen(Type) ->
+    Choices = get_prop(env,Type),
+    proper_gen:union_gen(Choices).
+
+union_is_instance(Type, X) ->
+    Choices = get_prop(env, Type),
+    lists:any(fun(C) -> is_instance(X, C) end, Choices).
+
+union_shrinker_1(X, Type, S) ->
+    Choices = get_prop(env, Type),
+    proper_shrink:union_first_choice_shrinker(X, Choices, S).
+
+union_shrinker_2(X, Type, S) ->
+    Choices = get_prop(env, Type),
+    proper_shrink:union_recursive_shrinker(X, Choices, S).
+
+%% @doc A specialization of {@link union/1}, where each type in `ListOfTypes' is
+%% assigned a frequency. Frequencies must be Erlang expressions that evaluate to
+%% positive integers. Types with larger frequencies are more likely to be chosen
+%% by the random instance generator. The shrinking subsystem will ignore the
+%% frequencies and try to shrink towards the first type in the list.
+-spec weighted_union(ListOfTypes::[{frequency(),raw_type()},...]) ->
+          proper_types:type().
+weighted_union(RawFreqChoices) ->
+    CookFreqType = fun({Freq,RawType}) -> {Freq,cook_outer(RawType)} end,
+    FreqChoices = lists:map(CookFreqType, RawFreqChoices),
+    Choices = [T || {_F,T} <- FreqChoices],
+    ?SUBTYPE(union(Choices), [
+	{subenv, FreqChoices},
+	{generator, {typed, fun weighted_union_gen/1}}
+    ]).
+
+weighted_union_gen(Gen) ->
+    FreqChoices = get_prop(subenv, Gen),
+    proper_gen:weighted_union_gen(FreqChoices).
+
+%% @private
+-spec safe_union([raw_type(),...]) -> proper_types:type().
+safe_union(RawChoices) ->
+    Choices = [cook_outer(C) || C <- RawChoices],
+    subtype(
+      [{subenv, Choices},
+       {generator, {typed, fun safe_union_gen/1}}],
+      union(Choices)).
+
+safe_union_gen(Type) ->
+    Choices = get_prop(subenv, Type),
+    proper_gen:safe_union_gen(Choices).
+
+%% @private
+-spec safe_weighted_union([{frequency(),raw_type()},...]) ->
+         proper_types:type().
+safe_weighted_union(RawFreqChoices) ->
+    CookFreqType = fun({Freq,RawType}) ->
+			   {Freq,cook_outer(RawType)} end,
+    FreqChoices = lists:map(CookFreqType, RawFreqChoices),
+    Choices = [T || {_F,T} <- FreqChoices],
+    subtype([{subenv, FreqChoices},
+             {generator, {typed, fun safe_weighted_union_gen/1}}],
+            union(Choices)).
+
+safe_weighted_union_gen(Type) ->
+    FreqChoices = get_prop(subenv, Type),
+    proper_gen:safe_weighted_union_gen(FreqChoices).
+
+%% @doc All tuples whose i-th element is an instance of the type at index i of
+%% `ListOfTypes'. Also written simply as a tuple of types.
+-spec tuple(ListOfTypes::[raw_type()]) -> proper_types:type().
+tuple(RawFields) ->
+    Fields = [cook_outer(F) || F <- RawFields],
+    ?CONTAINER([
+	{env, Fields},
+	{generator, {typed, fun tuple_gen/1}},
+	{is_instance, {typed, fun tuple_is_instance/2}},
+	{internal_types, list_to_tuple(Fields)},
+	{get_indices, fun tuple_get_indices/2},
+	{retrieve, fun erlang:element/2},
+	{update, fun tuple_update/3}
+    ]).
+
+tuple_gen(Type) ->
+    Fields = get_prop(env, Type),
+    proper_gen:tuple_gen(Fields).
+
+tuple_is_instance(Type, X) ->
+    Fields = get_prop(env, Type),
+    is_tuple(X) andalso fixed_list_test(tuple_to_list(X), Fields).
+
+tuple_get_indices(Type, _X) ->
+    lists:seq(1, length(get_prop(env, Type))).
+
+-spec tuple_update(index(), value(), tuple()) -> tuple().
+tuple_update(Index, NewElem, Tuple) ->
+    setelement(Index, Tuple, NewElem).
+
+%% @doc Tuples whose elements are all of type `ElemType'.
+%% Instances shrink towards the 0-size tuple, `{}'.
+-spec loose_tuple(ElemType::raw_type()) -> proper_types:type().
+loose_tuple(RawElemType) ->
+    ElemType = cook_outer(RawElemType),
+    ?WRAPPER([
+	{env, ElemType},
+	{generator, {typed, fun loose_tuple_gen/2}},
+	{reverse_gen, {typed, fun loose_tuple_rev/2}},
+	{is_instance, {typed, fun loose_tuple_is_instance/2}}
+    ]).
+
+loose_tuple_gen(Type, Size) ->
+    ElemType = get_prop(env, Type),
+    proper_gen:loose_tuple_gen(Size, ElemType).
+
+loose_tuple_rev(Type, X) ->
+    ElemType = get_prop(env, Type),
+    proper_gen:loose_tuple_rev(X, ElemType).
+
+loose_tuple_is_instance(Type, X) ->
+    ElemType = get_prop(env, Type),
+    is_tuple(X) andalso list_test(tuple_to_list(X), ElemType).
+
+%% @doc Singleton type consisting only of `E'. `E' must be an evaluated term.
+%% Also written simply as `E'.
+-spec exactly(term()) -> proper_types:type().
+exactly(E) ->
+    ?BASIC([
+	{env, E},
+	{generator, {typed, fun exactly_gen/1}},
+	{is_instance, {typed, fun exactly_is_instance/2}}
+    ]).
+
+exactly_gen(Type) ->
+    E = get_prop(env, Type),
+    proper_gen:exactly_gen(E).
+
+exactly_is_instance(Type, X) ->
+    E = get_prop(env, Type),
+    X =:= E.
+
+%% @doc All lists whose i-th element is an instance of the type at index i of
+%% `ListOfTypes'. Also written simply as a list of types.
+-spec fixed_list(ListOfTypes::maybe_improper_list(raw_type(),raw_type()|[])) ->
+	  proper_types:type().
+fixed_list(MaybeImproperRawFields) ->
+    %% CAUTION: must handle improper lists
+    {Fields, Internal, Len, Retrieve, Update} =
+	case proper_arith:cut_improper_tail(MaybeImproperRawFields) of
+	    % TODO: have cut_improper_tail return the length and use it in test?
+	    {ProperRawHead, ImproperRawTail} ->
+		HeadLen = length(ProperRawHead),
+		CookedHead = [cook_outer(F) || F <- ProperRawHead],
+		CookedTail = cook_outer(ImproperRawTail),
+		{{CookedHead,CookedTail},
+		 CookedHead ++ CookedTail,
+		 HeadLen + 1,
+		 fun(I,L) -> improper_list_retrieve(I, L, HeadLen) end,
+		 fun(I,V,L) -> improper_list_update(I, V, L, HeadLen) end};
+	    ProperRawFields ->
+		LocalFields = [cook_outer(F) || F <- ProperRawFields],
+		{LocalFields,
+		 LocalFields,
+		 length(ProperRawFields),
+		 fun lists:nth/2,
+		 fun proper_arith:list_update/3}
+	end,
+    ?CONTAINER([
+	{env, {Fields, Len}},
+	{generator, {typed, fun fixed_list_gen/1}},
+	{is_instance, {typed, fun fixed_list_is_instance/2}},
+	{internal_types, Internal},
+	{get_indices, fun fixed_list_get_indices/2},
+	{retrieve, Retrieve},
+	{update, Update}
+    ]).
+
+fixed_list_gen(Type) ->
+    {Fields, _} = get_prop(env, Type),
+    proper_gen:fixed_list_gen(Fields).
+
+fixed_list_is_instance(Type, X) ->
+    {Fields, _} = get_prop(env, Type),
+    fixed_list_test(X, Fields).
+
+fixed_list_get_indices(Type, _X) ->
+    {_, Len} = get_prop(env, Type),
+    lists:seq(1, Len).
+
+-spec fixed_list_test(proper_gen:imm_instance(),
+		      [proper_types:type()] | {[proper_types:type()],
+					       proper_types:type()}) ->
+	  boolean().
+fixed_list_test(X, {ProperHead,ImproperTail}) ->
+    is_list(X) andalso
+    begin
+	ProperHeadLen = length(ProperHead),
+	proper_arith:head_length(X) >= ProperHeadLen andalso
+	begin
+	    {XHead,XTail} = lists:split(ProperHeadLen, X),
+	    fixed_list_test(XHead, ProperHead)
+	    andalso is_instance(XTail, ImproperTail)
+	end
+    end;
+fixed_list_test(X, ProperFields) ->
+    is_list(X)
+    andalso length(X) =:= length(ProperFields)
+    andalso lists:all(fun({E,T}) -> is_instance(E, T) end,
+		      lists:zip(X, ProperFields)).
+
+%% TODO: Move these 2 functions to proper_arith?
+-spec improper_list_retrieve(index(), nonempty_improper_list(value(),value()),
+			     pos_integer()) -> value().
+improper_list_retrieve(Index, List, HeadLen) ->
+    case Index =< HeadLen of
+	true  -> lists:nth(Index, List);
+	false -> lists:nthtail(HeadLen, List)
+    end.
+
+-spec improper_list_update(index(), value(),
+			   nonempty_improper_list(value(),value()),
+			   pos_integer()) ->
+	  nonempty_improper_list(value(),value()).
+improper_list_update(Index, Value, List, HeadLen) ->
+    case Index =< HeadLen of
+	%% TODO: This happens to work, but is not implied by list_update's spec.
+	true  -> proper_arith:list_update(Index, Value, List);
+	false -> lists:sublist(List, HeadLen) ++ Value
+    end.
+
+%% @doc All pure functions that map instances of `ArgTypes' to instances of
+%% `RetType'. The syntax `function(Arity, RetType)' is also acceptable.
+-spec function(ArgTypes::[raw_type()] | arity(), RetType::raw_type()) ->
+          proper_types:type().
+function(Arity, RawRetType) when is_integer(Arity), Arity >= 0, Arity =< 255 ->
+    RetType = cook_outer(RawRetType),
+    ?BASIC([
+	{env, {Arity, RetType}},
+	{generator, {typed, fun function_gen/1}},
+	{is_instance, {typed, fun function_is_instance/2}}
+    ]);
+function(RawArgTypes, RawRetType) ->
+    function(length(RawArgTypes), RawRetType).
+
+function_gen(Type) ->
+    {Arity, RetType} = get_prop(env, Type),
+    proper_gen:function_gen(Arity, RetType).
+
+function_is_instance(Type, X) ->
+    {Arity, RetType} = get_prop(env, Type),
+    is_function(X, Arity)
+    %% TODO: what if it's not a function we produced?
+    andalso equal_types(RetType, proper_gen:get_ret_type(X)).
+
+%% @doc All Erlang terms (that PropEr can produce). For reasons of efficiency,
+%% functions are never produced as instances of this type.<br />
+%% CAUTION: Instances of this type are expensive to produce, shrink and instance-
+%% check, both in terms of processing time and consumed memory. Only use this
+%% type if you are certain that you need it.
+-spec any() -> proper_types:type().
+any() ->
+    AllTypes = [integer(),float(),atom(),bitstring(),?LAZY(loose_tuple(any())),
+		?LAZY(list(any()))],
+    ?SUBTYPE(union(AllTypes), [
+	{generator, fun proper_gen:any_gen/1}
+    ]).
+
+
+%%------------------------------------------------------------------------------
+%% Type aliases
+%%------------------------------------------------------------------------------
+
+%% @equiv integer(inf, inf)
+-spec integer() -> proper_types:type().
+integer() -> integer(inf, inf).
+
+%% @equiv integer(0, inf)
+-spec non_neg_integer() -> proper_types:type().
+non_neg_integer() -> integer(0, inf).
+
+%% @equiv integer(1, inf)
+-spec pos_integer() -> proper_types:type().
+pos_integer() -> integer(1, inf).
+
+%% @equiv integer(inf, -1)
+-spec neg_integer() -> proper_types:type().
+neg_integer() -> integer(inf, -1).
+
+%% @equiv integer(Low, High)
+-spec range(extint(), extint()) -> proper_types:type().
+range(Low, High) -> integer(Low, High).
+
+%% @equiv float(inf, inf)
+-spec float() -> proper_types:type().
+float() -> float(inf, inf).
+
+%% @equiv float(0.0, inf)
+-spec non_neg_float() -> proper_types:type().
+non_neg_float() -> float(0.0, inf).
+
+%% @equiv union([integer(), float()])
+-spec number() -> proper_types:type().
+number() -> union([integer(), float()]).
+
+%% @doc The atoms `true' and `false'. Instances shrink towards `false'.
+-spec boolean() -> proper_types:type().
+boolean() -> union(['false', 'true']).
+
+%% @equiv integer(0, 255)
+-spec byte() -> proper_types:type().
+byte() -> integer(0, 255).
+
+%% @equiv integer(0, 16#10ffff)
+-spec char() -> proper_types:type().
+char() -> integer(0, 16#10ffff).
+
+%% @equiv list(any())
+-spec list() -> proper_types:type().
+list() -> list(any()).
+
+%% @equiv loose_tuple(any())
+-spec tuple() -> proper_types:type().
+tuple() -> loose_tuple(any()).
+
+%% @equiv list(char())
+-spec string() -> proper_types:type().
+string() -> list(char()).
+
+%% @equiv weighted_union(FreqChoices)
+-spec wunion([{frequency(),raw_type()},...]) -> proper_types:type().
+wunion(FreqChoices) -> weighted_union(FreqChoices).
+
+%% @equiv any()
+-spec term() -> proper_types:type().
+term() -> any().
+
+%% @equiv union([non_neg_integer() | infinity])
+-spec timeout() -> proper_types:type().
+timeout() -> union([non_neg_integer(), 'infinity']).
+
+%% @equiv integer(0, 255)
+-spec arity() -> proper_types:type().
+arity() -> integer(0, 255).
+
+
+%%------------------------------------------------------------------------------
+%% QuickCheck compatibility types
+%%------------------------------------------------------------------------------
+
+%% @doc Small integers (bound by the current value of the `size' parameter).
+%% Instances shrink towards `0'.
+-spec int() -> proper_types:type().
+int() -> ?SIZED(Size, integer(-Size,Size)).
+
+%% @doc Small non-negative integers (bound by the current value of the `size'
+%% parameter). Instances shrink towards `0'.
+-spec nat() -> proper_types:type().
+nat() -> ?SIZED(Size, integer(0,Size)).
+
+%% @equiv integer()
+-spec largeint() -> proper_types:type().
+largeint() -> integer().
+
+%% @equiv float()
+-spec real() -> proper_types:type().
+real() -> float().
+
+%% @equiv boolean()
+-spec bool() -> proper_types:type().
+bool() -> boolean().
+
+%% @equiv integer(Low, High)
+-spec choose(extint(), extint()) -> proper_types:type().
+choose(Low, High) -> integer(Low, High).
+
+%% @equiv union(Choices)
+-spec elements([raw_type(),...]) -> proper_types:type().
+elements(Choices) -> union(Choices).
+
+%% @equiv union(Choices)
+-spec oneof([raw_type(),...]) -> proper_types:type().
+oneof(Choices) -> union(Choices).
+
+%% @equiv weighted_union(Choices)
+-spec frequency([{frequency(),raw_type()},...]) -> proper_types:type().
+frequency(FreqChoices) -> weighted_union(FreqChoices).
+
+%% @equiv exactly(E)
+-spec return(term()) -> proper_types:type().
+return(E) -> exactly(E).
+
+%% @doc Adds a default value, `Default', to `Type'.
+%% The default serves as a primary shrinking target for instances, while it
+%% is also chosen by the random instance generation subsystem half the time.
+-spec default(raw_type(), raw_type()) -> proper_types:type().
+default(Default, Type) ->
+    union([Default, Type]).
+
+%% @doc All sorted lists containing elements of type `ElemType'.
+%% Instances shrink towards the empty list, `[]'.
+-spec orderedlist(ElemType::raw_type()) -> proper_types:type().
+orderedlist(RawElemType) ->
+    ?LET(L, list(RawElemType), lists:sort(L)).
+
+%% @equiv function(0, RetType)
+-spec function0(raw_type()) -> proper_types:type().
+function0(RetType) ->
+    function(0, RetType).
+
+%% @equiv function(1, RetType)
+-spec function1(raw_type()) -> proper_types:type().
+function1(RetType) ->
+    function(1, RetType).
+
+%% @equiv function(2, RetType)
+-spec function2(raw_type()) -> proper_types:type().
+function2(RetType) ->
+    function(2, RetType).
+
+%% @equiv function(3, RetType)
+-spec function3(raw_type()) -> proper_types:type().
+function3(RetType) ->
+    function(3, RetType).
+
+%% @equiv function(4, RetType)
+-spec function4(raw_type()) -> proper_types:type().
+function4(RetType) ->
+    function(4, RetType).
+
+%% @doc A specialization of {@link default/2}, where `Default' and `Type' are
+%% assigned weights to be considered by the random instance generator. The
+%% shrinking subsystem will ignore the weights and try to shrink using the
+%% default value.
+-spec weighted_default({frequency(),raw_type()}, {frequency(),raw_type()}) ->
+	  proper_types:type().
+weighted_default(Default, Type) ->
+    weighted_union([Default, Type]).
+
+
+%%------------------------------------------------------------------------------
+%% Additional type specification functions
+%%------------------------------------------------------------------------------
+
+%% @doc Overrides the `size' parameter used when generating instances of
+%% `Type' with `NewSize'. Has no effect on size-less types, such as unions.
+%% Also, this will not affect the generation of any internal types contained in
+%% `Type', such as the elements of a list - those will still be generated
+%% using the test-wide value of `size'. One use of this function is to modify
+%% types to produce instances that grow faster or slower, like so:
+%% ```?SIZED(Size, resize(Size * 2, list(integer()))'''
+%% The above specifies a list type that grows twice as fast as normal lists.
+-spec resize(size(), Type::raw_type()) -> proper_types:type().
+resize(NewSize, RawType) ->
+    Type = cook_outer(RawType),
+    case find_prop(size_transform, Type) of
+	{ok,Transform} ->
+	    add_prop(size_transform, fun(_S) -> Transform(NewSize) end, Type);
+	error ->
+	    add_prop(size_transform, fun(_S) -> NewSize end, Type)
+    end.
+
+%% @doc This is a predefined constraint that can be applied to random-length
+%% list and binary types to ensure that the produced values are never empty.
+%%
+%% e.g. {@link list/0}, {@link string/0}, {@link binary/0})
+-spec non_empty(ListType::raw_type()) -> proper_types:type().
+non_empty(RawListType) ->
+    ?SUCHTHAT(L, RawListType, L =/= [] andalso L =/= <<>>).
+
+%% @doc Creates a new type which is equivalent to `Type', but whose instances
+%% are never shrunk by the shrinking subsystem.
+-spec noshrink(Type::raw_type()) -> proper_types:type().
+noshrink(RawType) ->
+    add_prop(noshrink, true, cook_outer(RawType)).
+
+%% @doc Associates the atom key `Parameter' with the value `Value' while
+%% generating instances of `Type'.
+-spec with_parameter(atom(), value(), Type::raw_type()) -> proper_types:type().
+with_parameter(Parameter, Value, RawType) ->
+    with_parameters([{Parameter,Value}], RawType).
+
+%% @doc Similar to {@link with_parameter/3}, but accepts a list of
+%% `{Parameter, Value}' pairs.
+-spec with_parameters([{atom(),value()}], Type::raw_type()) ->
+          proper_types:type().
+with_parameters(PVlist, RawType) ->
+    Type = cook_outer(RawType),
+    case find_prop(parameters, Type) of
+	{ok,Params} when is_list(Params) ->
+	    append_list_to_prop(parameters, PVlist, Type);
+	error ->
+	    add_prop(parameters, PVlist, Type)
+    end.
+
+%% @doc Returns the value associated with `Parameter', or `Default' in case
+%% `Parameter' is not associated with any value.
+-spec parameter(atom(), value()) -> value().
+parameter(Parameter, Default) ->
+    Parameters =
+	case erlang:get('$parameters') of
+	    undefined -> [];
+	    List -> List
+	end,
+    proplists:get_value(Parameter, Parameters, Default).
+
+%% @equiv parameter(Parameter, undefined)
+-spec parameter(atom()) -> value().
+parameter(Parameter) ->
+    parameter(Parameter, undefined).
diff --git a/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_typeserver.erl b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_typeserver.erl
new file mode 100644
index 0000000000..b16075763f
--- /dev/null
+++ b/lib/dialyzer/test/behaviour_SUITE_data/src/proper/proper_typeserver.erl
@@ -0,0 +1,2411 @@
+%%% Copyright 2010-2016 Manolis Papadakis <[email protected]>,
+%%%                     Eirini Arvaniti <[email protected]>
+%%%                 and Kostis Sagonas <[email protected]>
+%%%
+%%% This file is part of PropEr.
+%%%
+%%% PropEr is free software: you can redistribute it and/or modify
+%%% it under the terms of the GNU General Public License as published by
+%%% the Free Software Foundation, either version 3 of the License, or
+%%% (at your option) any later version.
+%%%
+%%% PropEr is distributed in the hope that it will be useful,
+%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
+%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%%% GNU General Public License for more details.
+%%%
+%%% You should have received a copy of the GNU General Public License
+%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.
+
+%%% @copyright 2010-2016 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
+%%% @version {@version}
+%%% @author Manolis Papadakis
+
+%%% @doc Erlang type system - PropEr type system integration module.
+%%%
+%%% PropEr can parse types expressed in Erlang's type language and convert them
+%%% to its own type format. Such expressions can be used instead of regular type
+%%% constructors in the second argument of `?FORALL's. No extra notation is
+%%% required; PropEr will detect which calls correspond to native types by
+%%% applying a parse transform during compilation. This parse transform is
+%%% automatically applied to any module that includes the `proper.hrl' header
+%%% file. You can disable this feature by compiling your modules with
+%%% `-DPROPER_NO_TRANS'. Note that this will currently also disable the
+%%% automatic exporting of properties.
+%%%
+%%% The use of native types in properties is subject to the following usage
+%%% rules:
+%%% <ul>
+%%% <li>Native types cannot be used outside of `?FORALL's.</li>
+%%% <li>Inside `?FORALL's, native types can be combined with other native
+%%%   types, and even with PropEr types, inside tuples and lists (the constructs
+%%%   `[...]', `{...}' and `++' are all allowed).</li>
+%%% <li>All other constructs of Erlang's built-in type system (e.g. `|' for
+%%%   union, `_' as an alias of `any()', `<<_:_>>' binary type syntax and
+%%%   `fun((...) -> ...)' function type syntax) are not allowed in `?FORALL's,
+%%%   because they are rejected by the Erlang parser.</li>
+%%% <li>Anything other than a tuple constructor, list constructor, `++'
+%%%   application, local or remote call will automatically be considered a
+%%%   PropEr type constructor and not be processed further by the parse
+%%%   transform.</li>
+%%% <li>Parametric native types are fully supported; of course, they can only
+%%%   appear instantiated in a `?FORALL'. The arguments of parametric native
+%%%   types are always interpreted as native types.</li>
+%%% <li>Parametric PropEr types, on the other hand, can take any kind of
+%%%   argument. You can even mix native and PropEr types in the arguments of a
+%%%   PropEr type. For example, assuming that the following declarations are
+%%%   present:
+%%%   ``` my_proper_type() -> ?LET(...).
+%%%       -type my_native_type() :: ... .'''
+%%%   Then the following expressions are all legal:
+%%%   ``` vector(2, my_native_type())
+%%%       function(0, my_native_type())
+%%%       union([my_proper_type(), my_native_type()])''' </li>
+%%% <li>Some type constructors can take native types as arguments (but only
+%%%   inside `?FORALL's):
+%%%   <ul>
+%%%   <li>`?SUCHTHAT', `?SUCHTHATMAYBE', `non_empty', `noshrink': these work
+%%%     with native types too</li>
+%%%   <li>`?LAZY', `?SHRINK', `resize', `?SIZED': these don't work with native
+%%%     types</li>
+%%%   <li>`?LET', `?LETSHRINK': only the top-level base type can be a native
+%%%     type</li>
+%%%   </ul></li>
+%%% <li>Native type declarations in the `?FORALL's of a module can reference any
+%%%   custom type declared in a `-type' or `-opaque' attribute of the same
+%%%   module, as long as no module identifier is used.</li>
+%%% <li>Typed records cannot be referenced inside `?FORALL's using the
+%%%   `#rec_name{}' syntax. To use a typed record in a `?FORALL', enclose the
+%%%   record in a custom type like so:
+%%%   ``` -type rec_name() :: #rec_name{}. '''
+%%%   and use the custom type instead.</li>
+%%% <li>`?FORALL's may contain references to self-recursive or mutually
+%%%   recursive native types, so long as each type in the hierarchy has a clear
+%%%   base case.
+%%%   Currently, PropEr requires that the toplevel of any recursive type
+%%%   declaration is either a (maybe empty) list or a union containing at least
+%%%   one choice that doesn't reference the type directly (it may, however,
+%%%   reference any of the types that are mutually recursive with it). This
+%%%   means, for example, that some valid recursive type declarations, such as
+%%%   this one:
+%%%   ``` ?FORALL(..., a(), ...) '''
+%%%   where:
+%%%   ``` -type a() :: {'a','none' | a()}. '''
+%%%   are not accepted by PropEr. However, such types can be rewritten in a way
+%%%   that allows PropEr to parse them:
+%%%   ``` ?FORALL(..., a(), ...) '''
+%%%   where:
+%%%   ``` -type a() :: {'a','none'} | {'a',a()}. '''
+%%%   This also means that recursive record declarations are not allowed:
+%%%   ``` ?FORALL(..., rec(), ...) '''
+%%%   where:
+%%%   ``` -type rec() :: #rec{}.
+%%%       -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}). '''
+%%%   A little rewritting can usually remedy this problem as well:
+%%%   ``` ?FORALL(..., rec(), ...) '''
+%%%   where:
+%%%   ``` -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
+%%%       -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}). '''
+%%%   </li>
+%%% <li>Remote types may be referenced in a `?FORALL', so long as they are
+%%%   exported from the remote module. Currently, PropEr requires that any
+%%%   remote modules whose types are directly referenced from within properties
+%%%   are present in the code path at compile time, either compiled with
+%%%   `debug_info' enabled or in source form. If PropEr cannot find a remote
+%%%   module at all, finds only a compiled object file with no debug
+%%%   information or fails to compile the source file, all calls to that module
+%%%   will automatically be considered calls to PropEr type constructors.</li>
+%%% <li>For native types to be translated correctly, both the module that
+%%%   contains the `?FORALL' declaration as well as any module that contains
+%%%   the declaration of a type referenced (directly or indirectly) from inside
+%%%   a `?FORALL' must be present in the code path at runtime, either compiled
+%%%   with `debug_info' enabled or in source form.</li>
+%%% <li>Local types with the same name as an auto-imported BIF are not accepted
+%%%   by PropEr, unless the BIF in question has been declared in a
+%%%   `no_auto_import' option.</li>
+%%% <li>When an expression can be interpreted both as a PropEr type and as a
+%%%   native type, the former takes precedence. This means that a function
+%%%   `foo()' will shadow a type `foo()' if they are both present in the module.
+%%%   The same rule applies to remote functions and types as well.</li>
+%%% <li>The above may cause some confusion when list syntax is used:
+%%%   <ul>
+%%%   <li>The expression `[integer()]' can be interpreted both ways, so the
+%%%     PropEr way applies. Therefore, instances of this type will always be
+%%%     lists of length 1, not arbitrary integer lists, as would be expected
+%%%     when interpreting the expression as a native type.</li>
+%%%   <li>Assuming that a custom type foo/1 has been declared, the expression
+%%%     `foo([integer()])' can only be interpreted as a native type declaration,
+%%%     which means that the generic type of integer lists will be passed to
+%%%     `foo/1'.</li>
+%%%   </ul></li>
+%%% <li>Currently, PropEr does not detect the following mistakes:
+%%%   <ul>
+%%%   <li>inline record-field specializations that reference non-existent
+%%%     fields</li>
+%%%   <li>type parameters that are not present in the RHS of a `-type'
+%%%     declaration</li>
+%%%   <li>using `_' as a type variable in the LHS of a `-type' declaration</li>
+%%%   <li>using the same variable in more than one position in the LHS of a
+%%%     `-type' declaration</li>
+%%%   </ul>
+%%% </li>
+%%% </ul>
+%%%
+%%% You can use <a href="#index">these</a> functions to try out the type
+%%% translation subsystem.
+%%%
+%%% CAUTION: These functions should never be used inside properties. They are
+%%% meant for demonstration purposes only.
+
+-module(proper_typeserver).
+-behaviour(gen_server).
+-export([demo_translate_type/2, demo_is_instance/3]).
+
+-export([start/0, restart/0, stop/0, create_spec_test/3, get_exp_specced/1,
+	 is_instance/3, translate_type/1]).
+-export([init/1, handle_call/3, handle_cast/2, handle_info/2, terminate/2,
+	 code_change/3]).
+-export([get_exp_info/1, match/2]).
+
+-export_type([imm_type/0, mod_exp_types/0, mod_exp_funs/0]).
+
+-include("proper_internal.hrl").
+
+
+%%------------------------------------------------------------------------------
+%% Macros
+%%------------------------------------------------------------------------------
+
+-define(SRC_FILE_EXT, ".erl").
+
+-ifdef(AT_LEAST_19).
+-define(anno(L), erl_anno:new(L)).
+-else.
+-define(anno(L), L).
+-endif.
+
+%% Starting with 18.0 we need to handle both 'type' and 'user_type' tags;
+%% prior Erlang/OTP releases had only 'type' as a tag.
+-define(IS_TYPE_TAG(T), (T =:= type orelse T =:= user_type)).
+
+%% CAUTION: all these must be sorted
+-define(STD_TYPES_0,
+	[any,arity,atom,binary,bitstring,bool,boolean,byte,char,float,integer,
+	 list,neg_integer,non_neg_integer,number,pos_integer,string,term,
+	 timeout]).
+-define(HARD_ADTS,
+	%% gb_trees:iterator and gb_sets:iterator are NOT hardcoded
+	[{{array,0},array},      {{array,1},proper_array},
+	 {{dict,0},dict},        {{dict,2},proper_dict},
+	 {{gb_set,0},gb_sets},   {{gb_set,1},proper_gb_sets},
+	 {{gb_tree,0},gb_trees}, {{gb_tree,2},proper_gb_trees},
+	                         {{orddict,2},proper_orddict},
+	                         {{ordset,1},proper_ordsets},
+	 {{queue,0},queue},      {{queue,1},proper_queue},
+	 {{set,0},sets},         {{set,1},proper_sets}]).
+-define(HARD_ADT_MODS,
+	[{array, [{{array,0},
+		   {{type,0,record,[{atom,0,array}]},[]}}]},
+	 {dict, [{{dict,0},
+		  {{type,0,record,[{atom,0,dict}]},[]}}]},
+	 {gb_sets, [{{gb_set,0},
+		     {{type,0,tuple,[{type,0,non_neg_integer,[]},
+				     {type,0,gb_set_node,[]}]},[]}}]},
+	 {gb_trees, [{{gb_tree,0},
+		      {{type,0,tuple,[{type,0,non_neg_integer,[]},
+				      {type,0,gb_tree_node,[]}]},[]}}]},
+	 %% Our parametric ADTs are already declared as normal types, we just
+	 %% need to change them to opaques.
+	 {proper_array, [{{array,1},already_declared}]},
+	 {proper_dict, [{{dict,2},already_declared}]},
+	 {proper_gb_sets, [{{gb_set,1},already_declared},
+			   {{iterator,1},already_declared}]},
+	 {proper_gb_trees, [{{gb_tree,2},already_declared},
+			    {{iterator,2},already_declared}]},
+	 {proper_orddict, [{{orddict,2},already_declared}]},
+	 {proper_ordsets, [{{ordset,1},already_declared}]},
+	 {proper_queue, [{{queue,1},already_declared}]},
+	 {proper_sets, [{{set,1},already_declared}]},
+	 {queue, [{{queue,0},
+		   {{type,0,tuple,[{type,0,list,[]},{type,0,list,[]}]},[]}}]},
+	 {sets, [{{set,0},
+		  {{type,0,record,[{atom,0,set}]},[]}}]}]).
+
+
+%%------------------------------------------------------------------------------
+%% Types
+%%------------------------------------------------------------------------------
+
+-type type_name() :: atom().
+-type var_name() :: atom(). %% TODO: also integers?
+-type field_name() :: atom().
+
+-type type_kind() :: 'type' | 'record'.
+-type type_ref() :: {type_kind(),type_name(),arity()}.
+-ifdef(NO_MODULES_IN_OPAQUES).
+-type substs_dict() :: dict(). %% dict(field_name(),ret_type())
+-else.
+-type substs_dict() :: dict:dict(field_name(),ret_type()).
+-endif.
+-type full_type_ref() :: {mod_name(),type_kind(),type_name(),
+			  [ret_type()] | substs_dict()}.
+-type symb_info() :: 'not_symb' | {'orig_abs',abs_type()}.
+-type type_repr() :: {'abs_type',abs_type(),[var_name()],symb_info()}
+		   | {'cached',fin_type(),abs_type(),symb_info()}
+		   | {'abs_record',[{field_name(),abs_type()}]}.
+-type gen_fun() :: fun((size()) -> fin_type()).
+-type rec_fun() :: fun(([gen_fun()],size()) -> fin_type()).
+-type rec_arg() :: {boolean() | {'list',boolean(),rec_fun()},full_type_ref()}.
+-type rec_args() :: [rec_arg()].
+-type ret_type() :: {'simple',fin_type()} | {'rec',rec_fun(),rec_args()}.
+-type rec_fun_info() :: {pos_integer(),pos_integer(),[arity(),...],
+			 [rec_fun(),...]}.
+
+-type imm_type_ref() :: {type_name(),arity()}.
+-type hard_adt_repr() :: {abs_type(),[var_name()]} | 'already_declared'.
+-type fun_ref() :: {fun_name(),arity()}.
+-type fun_repr() :: fun_clause_repr().
+-type fun_clause_repr() :: {[abs_type()],abs_type()}.
+-type proc_fun_ref() :: {fun_name(),[abs_type()],abs_type()}.
+-type full_imm_type_ref() :: {mod_name(),type_name(),arity()}.
+-type imm_stack() :: [full_imm_type_ref()].
+-type pat_field() :: 0 | 1 | atom().
+-type pattern() :: loose_tuple(pat_field()).
+-type next_step() :: 'none' | 'take_head' | {'match_with',pattern()}.
+
+-ifdef(NO_MODULES_IN_OPAQUES).
+%% @private_type
+-type mod_exp_types() :: set(). %% set(imm_type_ref())
+-type mod_types() :: dict(). %% dict(type_ref(),type_repr())
+%% @private_type
+-type mod_exp_funs() :: set(). %% set(fun_ref())
+-type mod_specs() :: dict(). %% dict(fun_ref(),fun_repr())
+-else.
+%% @private_type
+-type mod_exp_types() :: sets:set(imm_type_ref()).
+-type mod_types() :: dict:dict(type_ref(),type_repr()).
+%% @private_type
+-type mod_exp_funs() :: sets:set(fun_ref()).
+-type mod_specs() :: dict:dict(fun_ref(),fun_repr()).
+-endif.
+
+-ifdef(NO_MODULES_IN_OPAQUES).
+-record(state,
+	{cached    = dict:new() :: dict(),   %% dict(imm_type(),fin_type())
+	 exp_types = dict:new() :: dict(),   %% dict(mod_name(),mod_exp_types())
+	 types     = dict:new() :: dict(),   %% dict(mod_name(),mod_types())
+	 exp_specs = dict:new() :: dict()}). %% dict(mod_name(),mod_specs())
+-else.
+-record(state,
+	{cached    = dict:new() :: dict:dict(imm_type(),fin_type()),
+	 exp_types = dict:new() :: dict:dict(mod_name(),mod_exp_types()),
+	 types     = dict:new() :: dict:dict(mod_name(),mod_types()),
+	 exp_specs = dict:new() :: dict:dict(mod_name(),mod_specs())}).
+-endif.
+-type state() :: #state{}.
+
+-record(mod_info,
+	{mod_exp_types = sets:new() :: mod_exp_types(),
+	 mod_types     = dict:new() :: mod_types(),
+	 mod_opaques   = sets:new() :: mod_exp_types(),
+	 mod_exp_funs  = sets:new() :: mod_exp_funs(),
+	 mod_specs     = dict:new() :: mod_specs()}).
+-type mod_info() :: #mod_info{}.
+
+-type stack() :: [full_type_ref() | 'tuple' | 'list' | 'union' | 'fun'].
+-ifdef(NO_MODULES_IN_OPAQUES).
+-type var_dict() :: dict(). %% dict(var_name(),ret_type())
+-else.
+-type var_dict() :: dict:dict(var_name(),ret_type()).
+-endif.
+%% @private_type
+-type imm_type() :: {mod_name(),string()}.
+%% @alias
+-type fin_type() :: proper_types:type().
+-type tagged_result(T) :: {'ok',T} | 'error'.
+-type tagged_result2(T,S) :: {'ok',T,S} | 'error'.
+%% @alias
+-type rich_result(T) :: {'ok',T} | {'error',term()}.
+-type rich_result2(T,S) :: {'ok',T,S} | {'error',term()}.
+-type false_positive_mfas() :: proper:false_positive_mfas().
+
+-type server_call() :: {'create_spec_test',mfa(),timeout(),false_positive_mfas()}
+		     | {'get_exp_specced',mod_name()}
+		     | {'get_type_repr',mod_name(),type_ref(),boolean()}
+		     | {'translate_type',imm_type()}.
+-type server_response() :: rich_result(proper:test())
+			 | rich_result([mfa()])
+			 | rich_result(type_repr())
+			 | rich_result(fin_type()).
+
+
+%%------------------------------------------------------------------------------
+%% Server interface functions
+%%------------------------------------------------------------------------------
+
+%% @private
+-spec start() -> 'ok'.
+start() ->
+    {ok,TypeserverPid} = gen_server:start_link(?MODULE, dummy, []),
+    put('$typeserver_pid', TypeserverPid),
+    ok.
+
+%% @private
+-spec restart() -> 'ok'.
+restart() ->
+    TypeserverPid = get('$typeserver_pid'),
+    case (TypeserverPid =:= undefined orelse not is_process_alive(TypeserverPid)) of
+        true -> start();
+        false -> ok
+    end.
+
+%% @private
+-spec stop() -> 'ok'.
+stop() ->
+    TypeserverPid = get('$typeserver_pid'),
+    erase('$typeserver_pid'),
+    gen_server:cast(TypeserverPid, stop).
+
+%% @private
+-spec create_spec_test(mfa(), timeout(), false_positive_mfas()) -> rich_result(proper:test()).
+create_spec_test(MFA, SpecTimeout, FalsePositiveMFAs) ->
+    TypeserverPid = get('$typeserver_pid'),
+    gen_server:call(TypeserverPid, {create_spec_test,MFA,SpecTimeout,FalsePositiveMFAs}).
+
+%% @private
+-spec get_exp_specced(mod_name()) -> rich_result([mfa()]).
+get_exp_specced(Mod) ->
+    TypeserverPid = get('$typeserver_pid'),
+    gen_server:call(TypeserverPid, {get_exp_specced,Mod}).
+
+-spec get_type_repr(mod_name(), type_ref(), boolean()) ->
+	  rich_result(type_repr()).
+get_type_repr(Mod, TypeRef, IsRemote) ->
+    TypeserverPid = get('$typeserver_pid'),
+    gen_server:call(TypeserverPid, {get_type_repr,Mod,TypeRef,IsRemote}).
+
+%% @private
+-spec translate_type(imm_type()) -> rich_result(fin_type()).
+translate_type(ImmType) ->
+    TypeserverPid = get('$typeserver_pid'),
+    gen_server:call(TypeserverPid, {translate_type,ImmType}).
+
+%% @doc Translates the native type expression `TypeExpr' (which should be
+%% provided inside a string) into a PropEr type, which can then be passed to any
+%% of the demo functions defined in the {@link proper_gen} module. PropEr acts
+%% as if it found this type expression inside the code of module `Mod'.
+-spec demo_translate_type(mod_name(), string()) -> rich_result(fin_type()).
+demo_translate_type(Mod, TypeExpr) ->
+    start(),
+    Result = translate_type({Mod,TypeExpr}),
+    stop(),
+    Result.
+
+%% @doc Checks if `Term' is a valid instance of native type `TypeExpr' (which
+%% should be provided inside a string). PropEr acts as if it found this type
+%% expression inside the code of module `Mod'.
+-spec demo_is_instance(term(), mod_name(), string()) ->
+	  boolean() | {'error',term()}.
+demo_is_instance(Term, Mod, TypeExpr) ->
+    case parse_type(TypeExpr) of
+	{ok,TypeForm} ->
+	    start(),
+	    Result =
+		%% Force the typeserver to load the module.
+		case translate_type({Mod,"integer()"}) of
+		    {ok,_FinType} ->
+			try is_instance(Term, Mod, TypeForm)
+			catch
+			    throw:{'$typeserver',Reason} -> {error, Reason}
+			end;
+		    {error,_Reason} = Error ->
+			Error
+		end,
+	    stop(),
+	    Result;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+
+%%------------------------------------------------------------------------------
+%% Implementation of gen_server interface
+%%------------------------------------------------------------------------------
+
+%% @private
+-spec init(_) -> {'ok',state()}.
+init(_) ->
+    {ok, #state{}}.
+
+%% @private
+-spec handle_call(server_call(), _, state()) ->
+	  {'reply',server_response(),state()}.
+handle_call({create_spec_test,MFA,SpecTimeout,FalsePositiveMFAs}, _From, State) ->
+    case create_spec_test(MFA, SpecTimeout, FalsePositiveMFAs, State) of
+	{ok,Test,NewState} ->
+	    {reply, {ok,Test}, NewState};
+	{error,_Reason} = Error ->
+	    {reply, Error, State}
+    end;
+handle_call({get_exp_specced,Mod}, _From, State) ->
+    case get_exp_specced(Mod, State) of
+	{ok,MFAs,NewState} ->
+	    {reply, {ok,MFAs}, NewState};
+	{error,_Reason} = Error ->
+	    {reply, Error, State}
+    end;
+handle_call({get_type_repr,Mod,TypeRef,IsRemote}, _From, State) ->
+    case get_type_repr(Mod, TypeRef, IsRemote, State) of
+	{ok,TypeRepr,NewState} ->
+	    {reply, {ok,TypeRepr}, NewState};
+	{error,_Reason} = Error ->
+	    {reply, Error, State}
+    end;
+handle_call({translate_type,ImmType}, _From, State) ->
+    case translate_type(ImmType, State) of
+	{ok,FinType,NewState} ->
+	    {reply, {ok,FinType}, NewState};
+	{error,_Reason} = Error ->
+	    {reply, Error, State}
+    end.
+
+%% @private
+-spec handle_cast('stop', state()) -> {'stop','normal',state()}.
+handle_cast(stop, State) ->
+    {stop, normal, State}.
+
+%% @private
+-spec handle_info(term(), state()) -> {'stop',{'received_info',term()},state()}.
+handle_info(Info, State) ->
+    {stop, {received_info,Info}, State}.
+
+%% @private
+-spec terminate(term(), state()) -> 'ok'.
+terminate(_Reason, _State) ->
+    ok.
+
+%% @private
+-spec code_change(term(), state(), _) -> {'ok',state()}.
+code_change(_OldVsn, State, _) ->
+    {ok, State}.
+
+
+%%------------------------------------------------------------------------------
+%% Top-level interface
+%%------------------------------------------------------------------------------
+
+-spec create_spec_test(mfa(), timeout(), false_positive_mfas(), state()) ->
+	  rich_result2(proper:test(),state()).
+create_spec_test(MFA, SpecTimeout, FalsePositiveMFAs, State) ->
+    case get_exp_spec(MFA, State) of
+	{ok,FunRepr,NewState} ->
+	    make_spec_test(MFA, FunRepr, SpecTimeout, FalsePositiveMFAs, NewState);
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec get_exp_spec(mfa(), state()) -> rich_result2(fun_repr(),state()).
+get_exp_spec({Mod,Fun,Arity} = MFA, State) ->
+    case add_module(Mod, State) of
+	{ok,#state{exp_specs = ExpSpecs} = NewState} ->
+	    ModExpSpecs = dict:fetch(Mod, ExpSpecs),
+	    case dict:find({Fun,Arity}, ModExpSpecs) of
+		{ok,FunRepr} ->
+		    {ok, FunRepr, NewState};
+		error ->
+		    {error, {function_not_exported_or_specced,MFA}}
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec make_spec_test(mfa(), fun_repr(), timeout(), false_positive_mfas(), state()) ->
+	  rich_result2(proper:test(),state()).
+make_spec_test({Mod,_Fun,_Arity}=MFA, {Domain,_Range}=FunRepr, SpecTimeout, FalsePositiveMFAs, State) ->
+    case convert(Mod, {type,?anno(0),'$fixed_list',Domain}, State) of
+	{ok,FinType,NewState} ->
+            Test = ?FORALL(Args, FinType, apply_spec_test(MFA, FunRepr, SpecTimeout, FalsePositiveMFAs, Args)),
+            {ok, Test, NewState};
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec apply_spec_test(mfa(), fun_repr(), timeout(), false_positive_mfas(), term()) -> proper:test().
+apply_spec_test({Mod,Fun,_Arity}=MFA, {_Domain,Range}, SpecTimeout, FalsePositiveMFAs, Args) ->
+    ?TIMEOUT(SpecTimeout,
+             begin
+                 %% NOTE: only call apply/3 inside try/catch (do not trust ?MODULE:is_instance/3)
+                 Result =
+                     try apply(Mod, Fun, Args) of
+                         X -> {ok, X}
+                     catch
+                         X:Y -> {X, Y}
+                     end,
+                 case Result of
+                     {ok, Z} ->
+                         case ?MODULE:is_instance(Z, Mod, Range) of
+                             true ->
+                                 true;
+                             false when is_function(FalsePositiveMFAs) ->
+                                 FalsePositiveMFAs(MFA, Args, {fail, Z});
+                             false ->
+                                 false
+                         end;
+                     Exception when is_function(FalsePositiveMFAs) ->
+                         case FalsePositiveMFAs(MFA, Args, Exception) of
+                             true ->
+                                 true;
+                             false ->
+                                 error(Exception, erlang:get_stacktrace())
+                         end;
+                     Exception ->
+                         error(Exception, erlang:get_stacktrace())
+                 end
+             end).
+
+-spec get_exp_specced(mod_name(), state()) -> rich_result2([mfa()],state()).
+get_exp_specced(Mod, State) ->
+    case add_module(Mod, State) of
+	{ok,#state{exp_specs = ExpSpecs} = NewState} ->
+	    ModExpSpecs = dict:fetch(Mod, ExpSpecs),
+	    ExpSpecced = [{Mod,F,A} || {F,A} <- dict:fetch_keys(ModExpSpecs)],
+	    {ok, ExpSpecced, NewState};
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec get_type_repr(mod_name(), type_ref(), boolean(), state()) ->
+	  rich_result2(type_repr(),state()).
+get_type_repr(Mod, {type,Name,Arity} = TypeRef, true, State) ->
+    case prepare_for_remote(Mod, Name, Arity, State) of
+	{ok,NewState} ->
+	    get_type_repr(Mod, TypeRef, false, NewState);
+	{error,_Reason} = Error ->
+	    Error
+    end;
+get_type_repr(Mod, TypeRef, false, #state{types = Types} = State) ->
+    ModTypes = dict:fetch(Mod, Types),
+    case dict:find(TypeRef, ModTypes) of
+	{ok,TypeRepr} ->
+	    {ok, TypeRepr, State};
+	error ->
+	    {error, {missing_type,Mod,TypeRef}}
+    end.
+
+-spec prepare_for_remote(mod_name(), type_name(), arity(), state()) ->
+	  rich_result(state()).
+prepare_for_remote(RemMod, Name, Arity, State) ->
+    case add_module(RemMod, State) of
+	{ok,#state{exp_types = ExpTypes} = NewState} ->
+	    RemModExpTypes = dict:fetch(RemMod, ExpTypes),
+	    case sets:is_element({Name,Arity}, RemModExpTypes) of
+		true  -> {ok, NewState};
+		false -> {error, {type_not_exported,{RemMod,Name,Arity}}}
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec translate_type(imm_type(), state()) -> rich_result2(fin_type(),state()).
+translate_type({Mod,Str} = ImmType, #state{cached = Cached} = State) ->
+    case dict:find(ImmType, Cached) of
+	{ok,Type} ->
+	    {ok, Type, State};
+	error ->
+	    case parse_type(Str) of
+		{ok,TypeForm} ->
+		    case add_module(Mod, State) of
+			{ok,NewState} ->
+			    case convert(Mod, TypeForm, NewState) of
+				{ok,FinType,
+				 #state{cached = Cached} = FinalState} ->
+				    NewCached = dict:store(ImmType, FinType,
+							   Cached),
+				    {ok, FinType,
+				     FinalState#state{cached = NewCached}};
+				{error,_Reason} = Error ->
+				    Error
+			    end;
+			{error,_Reason} = Error ->
+			    Error
+		    end;
+		{error,Reason} ->
+		    {error, {parse_error,Str,Reason}}
+	    end
+    end.
+
+-spec parse_type(string()) -> rich_result(abs_type()).
+parse_type(Str) ->
+    TypeStr = "-type mytype() :: " ++ Str ++ ".",
+    case erl_scan:string(TypeStr) of
+	{ok,Tokens,_EndLocation} ->
+	    case erl_parse:parse_form(Tokens) of
+		{ok,{attribute,_Line,type,{mytype,TypeExpr,[]}}} ->
+		    {ok, TypeExpr};
+		{error,_ErrorInfo} = Error ->
+		    Error
+	    end;
+	{error,ErrorInfo,_EndLocation} ->
+	    {error, ErrorInfo}
+    end.
+
+-spec add_module(mod_name(), state()) -> rich_result(state()).
+add_module(Mod, #state{exp_types = ExpTypes} = State) ->
+    case dict:is_key(Mod, ExpTypes) of
+	true ->
+	    {ok, State};
+	false ->
+	    case get_code_and_exports(Mod) of
+		{ok,AbsCode,ModExpFuns} ->
+		    RawModInfo = get_mod_info(Mod, AbsCode, ModExpFuns),
+		    ModInfo = process_adts(Mod, RawModInfo),
+		    {ok, store_mod_info(Mod, ModInfo, State)};
+		{error,Reason} ->
+		    {error, {cant_load_code,Mod,Reason}}
+	    end
+    end.
+
+%% @private
+-spec get_exp_info(mod_name()) -> rich_result2(mod_exp_types(),mod_exp_funs()).
+get_exp_info(Mod) ->
+    case get_code_and_exports(Mod) of
+	{ok,AbsCode,ModExpFuns} ->
+	    RawModInfo = get_mod_info(Mod, AbsCode, ModExpFuns),
+	    {ok, RawModInfo#mod_info.mod_exp_types, ModExpFuns};
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec get_code_and_exports(mod_name()) ->
+	  rich_result2([abs_form()],mod_exp_funs()).
+get_code_and_exports(Mod) ->
+    case code:get_object_code(Mod) of
+	{Mod, ObjBin, _ObjFileName} ->
+	    case get_chunks(ObjBin) of
+		{ok,_AbsCode,_ModExpFuns} = Result ->
+		    Result;
+		{error,Reason} ->
+		    get_code_and_exports_from_source(Mod, Reason)
+	    end;
+	error ->
+	    get_code_and_exports_from_source(Mod, cant_find_object_file)
+    end.
+
+-spec get_code_and_exports_from_source(mod_name(), term()) ->
+	  rich_result2([abs_form()],mod_exp_funs()).
+get_code_and_exports_from_source(Mod, ObjError) ->
+    SrcFileName = atom_to_list(Mod) ++ ?SRC_FILE_EXT,
+    case code:where_is_file(SrcFileName) of
+	FullSrcFileName when is_list(FullSrcFileName) ->
+	    Opts = [binary,debug_info,return_errors,{d,'PROPER_REMOVE_PROPS'}],
+	    case compile:file(FullSrcFileName, Opts) of
+		{ok,Mod,Binary} ->
+		    get_chunks(Binary);
+		{error,Errors,_Warnings} ->
+		    {error, {ObjError,{cant_compile_source_file,Errors}}}
+	    end;
+	non_existing ->
+	    {error, {ObjError,cant_find_source_file}}
+    end.
+
+-spec get_chunks(string() | binary()) ->
+	  rich_result2([abs_form()],mod_exp_funs()).
+get_chunks(ObjFile) ->
+    case beam_lib:chunks(ObjFile, [abstract_code,exports]) of
+	{ok,{_Mod,[{abstract_code,AbsCodeChunk},{exports,ExpFunsList}]}} ->
+	    case AbsCodeChunk of
+		{raw_abstract_v1,AbsCode} ->
+		    %% HACK: Add a declaration for iolist() to every module
+		    {ok, add_iolist(AbsCode), sets:from_list(ExpFunsList)};
+		no_abstract_code ->
+		    {error, no_abstract_code};
+		_ ->
+		    {error, unsupported_abstract_code_format}
+	    end;
+	{error,beam_lib,Reason} ->
+	    {error, Reason}
+    end.
+
+-spec add_iolist([abs_form()]) -> [abs_form()].
+add_iolist(Forms) ->
+    IOListDef =
+	{type,0,maybe_improper_list,
+	 [{type,0,union,[{type,0,byte,[]},{type,0,binary,[]},
+			 {type,0,iolist,[]}]},
+	  {type,0,binary,[]}]},
+    IOListDecl = {attribute,0,type,{iolist,IOListDef,[]}},
+    [IOListDecl | Forms].
+
+-spec get_mod_info(mod_name(), [abs_form()], mod_exp_funs()) -> mod_info().
+get_mod_info(Mod, AbsCode, ModExpFuns) ->
+    StartModInfo = #mod_info{mod_exp_funs = ModExpFuns},
+    ImmModInfo = lists:foldl(fun add_mod_info/2, StartModInfo, AbsCode),
+    #mod_info{mod_specs = AllModSpecs} = ImmModInfo,
+    IsExported = fun(FunRef,_FunRepr) -> sets:is_element(FunRef,ModExpFuns) end,
+    ModExpSpecs = dict:filter(IsExported, AllModSpecs),
+    ModInfo = ImmModInfo#mod_info{mod_specs = ModExpSpecs},
+    case orddict:find(Mod, ?HARD_ADT_MODS) of
+	{ok,ModADTs} ->
+	    #mod_info{mod_exp_types = ModExpTypes, mod_types = ModTypes,
+		      mod_opaques = ModOpaques} = ModInfo,
+	    ModADTsSet =
+		sets:from_list([ImmTypeRef
+				|| {ImmTypeRef,_HardADTRepr} <- ModADTs]),
+	    NewModExpTypes = sets:union(ModExpTypes, ModADTsSet),
+	    NewModTypes = lists:foldl(fun store_hard_adt/2, ModTypes, ModADTs),
+	    NewModOpaques = sets:union(ModOpaques, ModADTsSet),
+	    ModInfo#mod_info{mod_exp_types = NewModExpTypes,
+			     mod_types = NewModTypes,
+			     mod_opaques = NewModOpaques};
+	error ->
+	    ModInfo
+    end.
+
+-spec store_hard_adt({imm_type_ref(),hard_adt_repr()}, mod_types()) ->
+	  mod_types().
+store_hard_adt({_ImmTypeRef,already_declared}, ModTypes) ->
+    ModTypes;
+store_hard_adt({{Name,Arity},{TypeForm,VarNames}}, ModTypes) ->
+    TypeRef = {type,Name,Arity},
+    TypeRepr = {abs_type,TypeForm,VarNames,not_symb},
+    dict:store(TypeRef, TypeRepr, ModTypes).
+
+-spec add_mod_info(abs_form(), mod_info()) -> mod_info().
+add_mod_info({attribute,_Line,export_type,TypesList},
+	     #mod_info{mod_exp_types = ModExpTypes} = ModInfo) ->
+    NewModExpTypes = sets:union(sets:from_list(TypesList), ModExpTypes),
+    ModInfo#mod_info{mod_exp_types = NewModExpTypes};
+add_mod_info({attribute,_Line,type,{{record,RecName},Fields,[]}},
+	     #mod_info{mod_types = ModTypes} = ModInfo) ->
+    FieldInfo = [process_rec_field(F) || F <- Fields],
+    NewModTypes = dict:store({record,RecName,0}, {abs_record,FieldInfo},
+			     ModTypes),
+    ModInfo#mod_info{mod_types = NewModTypes};
+add_mod_info({attribute,Line,record,{RecName,Fields}},
+	     #mod_info{mod_types = ModTypes} = ModInfo) ->
+    case dict:is_key(RecName, ModTypes) of
+	true ->
+	    ModInfo;
+	false ->  % fake an opaque term by using the same Line as annotation
+	    TypedRecord = {attribute,Line,type,{{record,RecName},Fields,[]}},
+	    add_mod_info(TypedRecord, ModInfo)
+    end;
+add_mod_info({attribute,_Line,Kind,{Name,TypeForm,VarForms}},
+	     #mod_info{mod_types = ModTypes,
+		       mod_opaques = ModOpaques} = ModInfo)
+	when Kind =:= type; Kind =:= opaque ->
+    Arity = length(VarForms),
+    VarNames = [V || {var,_,V} <- VarForms],
+    %% TODO: No check whether variables are different, or non-'_'.
+    NewModTypes = dict:store({type,Name,Arity},
+			     {abs_type,TypeForm,VarNames,not_symb}, ModTypes),
+    NewModOpaques =
+	case Kind of
+	    type   -> ModOpaques;
+	    opaque -> sets:add_element({Name,Arity}, ModOpaques)
+	end,
+    ModInfo#mod_info{mod_types = NewModTypes, mod_opaques = NewModOpaques};
+add_mod_info({attribute,_Line,spec,{RawFunRef,[RawFirstClause | _Rest]}},
+	     #mod_info{mod_specs = ModSpecs} = ModInfo) ->
+    FunRef = case RawFunRef of
+		 {_Mod,Name,Arity}  -> {Name,Arity};
+		 {_Name,_Arity} = F -> F
+	     end,
+    %% TODO: We just take the first function clause.
+    FirstClause = process_fun_clause(RawFirstClause),
+    NewModSpecs = dict:store(FunRef, FirstClause, ModSpecs),
+    ModInfo#mod_info{mod_specs = NewModSpecs};
+add_mod_info(_Form, ModInfo) ->
+    ModInfo.
+
+-spec process_rec_field(abs_rec_field()) -> {field_name(),abs_type()}.
+process_rec_field({record_field,_,{atom,_,FieldName}}) ->
+    {FieldName, {type,0,any,[]}};
+process_rec_field({record_field,_,{atom,_,FieldName},_Initialization}) ->
+    {FieldName, {type,0,any,[]}};
+process_rec_field({typed_record_field,RecField,FieldType}) ->
+    {FieldName,_} = process_rec_field(RecField),
+    {FieldName, FieldType}.
+
+-spec process_fun_clause(abs_type()) -> fun_clause_repr().
+process_fun_clause({type,_,'fun',[{type,_,product,Domain},Range]}) ->
+    {Domain, Range};
+process_fun_clause({type,_,bounded_fun,[MainClause,Constraints]}) ->
+    {RawDomain,RawRange} = process_fun_clause(MainClause),
+    VarSubsts = [{V,T} || {type,_,constraint,
+			   [{atom,_,is_subtype},[{var,_,V},T]]} <- Constraints,
+			  V =/= '_'],
+    VarSubstsDict = dict:from_list(VarSubsts),
+    Domain = [update_vars(A, VarSubstsDict, false) || A <- RawDomain],
+    Range = update_vars(RawRange, VarSubstsDict, false),
+    {Domain, Range}.
+
+-spec store_mod_info(mod_name(), mod_info(), state()) -> state().
+store_mod_info(Mod, #mod_info{mod_exp_types = ModExpTypes, mod_types = ModTypes,
+			      mod_specs = ImmModExpSpecs},
+	       #state{exp_types = ExpTypes, types = Types,
+		      exp_specs = ExpSpecs} = State) ->
+    NewExpTypes = dict:store(Mod, ModExpTypes, ExpTypes),
+    NewTypes = dict:store(Mod, ModTypes, Types),
+    ModExpSpecs = dict:map(fun unbound_to_any/2, ImmModExpSpecs),
+    NewExpSpecs = dict:store(Mod, ModExpSpecs, ExpSpecs),
+    State#state{exp_types = NewExpTypes, types = NewTypes,
+		exp_specs = NewExpSpecs}.
+
+-spec unbound_to_any(fun_ref(), fun_repr()) -> fun_repr().
+unbound_to_any(_FunRef, {Domain,Range}) ->
+    EmptySubstsDict = dict:new(),
+    NewDomain = [update_vars(A,EmptySubstsDict,true) || A <- Domain],
+    NewRange = update_vars(Range, EmptySubstsDict, true),
+    {NewDomain, NewRange}.
+
+
+%%------------------------------------------------------------------------------
+%% ADT translation functions
+%%------------------------------------------------------------------------------
+
+-spec process_adts(mod_name(), mod_info()) -> mod_info().
+process_adts(Mod,
+	     #mod_info{mod_exp_types = ModExpTypes, mod_opaques = ModOpaques,
+		       mod_specs = ModExpSpecs} = ModInfo) ->
+    %% TODO: No warning on unexported opaques.
+    case sets:to_list(sets:intersection(ModExpTypes,ModOpaques)) of
+	[] ->
+	    ModInfo;
+	ModADTs ->
+	    %% TODO: No warning on unexported API functions.
+	    ModExpSpecsList = [{Name,Domain,Range}
+			       || {{Name,_Arity},{Domain,Range}}
+				  <- dict:to_list(ModExpSpecs)],
+	    AddADT = fun(ADT,Acc) -> add_adt(Mod,ADT,Acc,ModExpSpecsList) end,
+	    lists:foldl(AddADT, ModInfo, ModADTs)
+    end.
+
+-spec add_adt(mod_name(), imm_type_ref(), mod_info(), [proc_fun_ref()]) ->
+	  mod_info().
+add_adt(Mod, {Name,Arity}, #mod_info{mod_types = ModTypes} = ModInfo,
+	ModExpFunSpecs) ->
+    ADTRef = {type,Name,Arity},
+    {abs_type,InternalRepr,VarNames,not_symb} = dict:fetch(ADTRef, ModTypes),
+    FullADTRef = {Mod,Name,Arity},
+    %% TODO: No warning on unsuitable range.
+    SymbCalls1 = [get_symb_call(FullADTRef,Spec) || Spec <- ModExpFunSpecs],
+    %% TODO: No warning on bad use of variables.
+    SymbCalls2 = [fix_vars(FullADTRef,Call,RangeVars,VarNames)
+		  || {ok,Call,RangeVars} <- SymbCalls1],
+    case [Call || {ok,Call} <- SymbCalls2] of
+	[] ->
+	    %% TODO: No warning on no acceptable spec.
+	    ModInfo;
+	SymbCalls3 ->
+	    NewADTRepr = {abs_type,{type,0,union,SymbCalls3},VarNames,
+			  {orig_abs,InternalRepr}},
+	    NewModTypes = dict:store(ADTRef, NewADTRepr, ModTypes),
+	    ModInfo#mod_info{mod_types = NewModTypes}
+    end.
+
+-spec get_symb_call(full_imm_type_ref(), proc_fun_ref()) ->
+	  tagged_result2(abs_type(),[var_name()]).
+get_symb_call({Mod,_TypeName,_Arity} = FullADTRef, {FunName,Domain,Range}) ->
+    A = ?anno(0),
+    BaseCall = {type,A,tuple,[{atom,A,'$call'},{atom,A,Mod},{atom,A,FunName},
+			      {type,A,'$fixed_list',Domain}]},
+    unwrap_range(FullADTRef, BaseCall, Range, false).
+
+-spec unwrap_range(full_imm_type_ref(), abs_type() | next_step(), abs_type(),
+		   boolean()) ->
+	  tagged_result2(abs_type() | next_step(),[var_name()]).
+unwrap_range(FullADTRef, Call, {paren_type,_,[Type]}, TestRun) ->
+    unwrap_range(FullADTRef, Call, Type, TestRun);
+unwrap_range(FullADTRef, Call, {ann_type,_,[_Var,Type]}, TestRun) ->
+    unwrap_range(FullADTRef, Call, Type, TestRun);
+unwrap_range(FullADTRef, Call, {type,_,list,[ElemType]}, TestRun) ->
+    unwrap_list(FullADTRef, Call, ElemType, TestRun);
+unwrap_range(FullADTRef, Call, {type,_,maybe_improper_list,[Cont,_Term]},
+	     TestRun) ->
+    unwrap_list(FullADTRef, Call, Cont, TestRun);
+unwrap_range(FullADTRef, Call, {type,_,nonempty_list,[ElemType]}, TestRun) ->
+    unwrap_list(FullADTRef, Call, ElemType, TestRun);
+unwrap_range(FullADTRef, Call, {type,_,nonempty_improper_list,[Cont,_Term]},
+	     TestRun) ->
+    unwrap_list(FullADTRef, Call, Cont, TestRun);
+unwrap_range(FullADTRef, Call,
+	     {type,_,nonempty_maybe_improper_list,[Cont,_Term]}, TestRun) ->
+    unwrap_list(FullADTRef, Call, Cont, TestRun);
+unwrap_range(_FullADTRef, _Call, {type,_,tuple,any}, _TestRun) ->
+    error;
+unwrap_range(FullADTRef, Call, {type,_,tuple,FieldForms}, TestRun) ->
+    Translates = fun(T) -> unwrap_range(FullADTRef,none,T,true) =/= error end,
+    case proper_arith:find_first(Translates, FieldForms) of
+	none ->
+	    error;
+	{TargetPos,TargetElem} ->
+	    Pattern = get_pattern(TargetPos, FieldForms),
+	    case TestRun of
+		true ->
+		    NewCall =
+			case Call of
+			    none -> {match_with,Pattern};
+			    _    -> Call
+			end,
+		    {ok, NewCall, []};
+		false ->
+		    AbsPattern = term_to_singleton_type(Pattern),
+		    A = ?anno(0),
+		    NewCall =
+			{type,A,tuple,
+			 [{atom,A,'$call'},{atom,A,?MODULE},{atom,A,match},
+			  {type,A,'$fixed_list',[AbsPattern,Call]}]},
+		    unwrap_range(FullADTRef, NewCall, TargetElem, TestRun)
+	    end
+    end;
+unwrap_range(FullADTRef, Call, {type,_,union,Choices}, TestRun) ->
+    TestedChoices = [unwrap_range(FullADTRef,none,C,true) || C <- Choices],
+    NotError = fun(error) -> false; (_) -> true end,
+    case proper_arith:find_first(NotError, TestedChoices) of
+	none ->
+	    error;
+	{_ChoicePos,{ok,none,_RangeVars}} ->
+	    error;
+	{ChoicePos,{ok,NextStep,_RangeVars}} ->
+	    {A, [ChoiceElem|B]} = lists:split(ChoicePos-1, Choices),
+	    OtherChoices = A ++ B,
+	    DistinctChoice =
+		case NextStep of
+		    take_head ->
+			fun cant_have_head/1;
+		    {match_with,Pattern} ->
+			fun(C) -> cant_match(Pattern, C) end
+		end,
+	    case {lists:all(DistinctChoice,OtherChoices), TestRun} of
+		{true,true} ->
+		    {ok, NextStep, []};
+		{true,false} ->
+		    unwrap_range(FullADTRef, Call, ChoiceElem, TestRun);
+		{false,_} ->
+		    error
+	    end
+    end;
+unwrap_range({_Mod,SameName,Arity}, Call, {type,_,SameName,ArgForms},
+	     _TestRun) ->
+    RangeVars = [V || {var,_,V} <- ArgForms, V =/= '_'],
+    case length(ArgForms) =:= Arity andalso length(RangeVars) =:= Arity of
+	true  -> {ok, Call, RangeVars};
+	false -> error
+    end;
+unwrap_range({SameMod,SameName,_Arity} = FullADTRef, Call,
+	     {remote_type,_,[{atom,_,SameMod},{atom,_,SameName},ArgForms]},
+	     TestRun) ->
+    unwrap_range(FullADTRef, Call, {type,?anno(0),SameName,ArgForms}, TestRun);
+unwrap_range(_FullADTRef, _Call, _Range, _TestRun) ->
+    error.
+
+-spec unwrap_list(full_imm_type_ref(), abs_type() | next_step(), abs_type(),
+		  boolean()) ->
+	  tagged_result2(abs_type() | next_step(),[var_name()]).
+unwrap_list(FullADTRef, Call, HeadType, TestRun) ->
+    NewCall =
+	case TestRun of
+	    true ->
+		case Call of
+		    none -> take_head;
+		    _    -> Call
+		end;
+	    false ->
+		{type,0,tuple,[{atom,0,'$call'},{atom,0,erlang},{atom,0,hd},
+			       {type,0,'$fixed_list',[Call]}]}
+	end,
+    unwrap_range(FullADTRef, NewCall, HeadType, TestRun).
+
+-spec fix_vars(full_imm_type_ref(), abs_type(), [var_name()], [var_name()]) ->
+	  tagged_result(abs_type()).
+fix_vars(FullADTRef, Call, RangeVars, VarNames) ->
+    NotAnyVar = fun(V) -> V =/= '_' end,
+    case no_duplicates(VarNames) andalso lists:all(NotAnyVar,VarNames) of
+	true ->
+	    RawUsedVars =
+		collect_vars(FullADTRef, Call, [[V] || V <- RangeVars]),
+	    UsedVars = [lists:usort(L) || L <- RawUsedVars],
+	    case correct_var_use(UsedVars) of
+		true ->
+		    PairAll = fun(L,Y) -> [{X,{var,0,Y}} || X <- L] end,
+		    VarSubsts =
+			lists:flatten(lists:zipwith(PairAll,UsedVars,VarNames)),
+		    VarSubstsDict = dict:from_list(VarSubsts),
+		    {ok, update_vars(Call,VarSubstsDict,true)};
+		false ->
+		    error
+	    end;
+	false ->
+	    error
+    end.
+
+-spec no_duplicates(list()) -> boolean().
+no_duplicates(L) ->
+    length(lists:usort(L)) =:= length(L).
+
+-spec correct_var_use([[var_name() | 0]]) -> boolean().
+correct_var_use(UsedVars) ->
+    NoNonVarArgs = fun([0|_]) -> false; (_) -> true end,
+    lists:all(NoNonVarArgs, UsedVars)
+    andalso no_duplicates(lists:flatten(UsedVars)).
+
+-spec collect_vars(full_imm_type_ref(), abs_type(), [[var_name() | 0]]) ->
+	  [[var_name() | 0]].
+collect_vars(FullADTRef, {paren_type,_,[Type]}, UsedVars) ->
+    collect_vars(FullADTRef, Type, UsedVars);
+collect_vars(FullADTRef, {ann_type,_,[_Var,Type]}, UsedVars) ->
+    collect_vars(FullADTRef, Type, UsedVars);
+collect_vars(_FullADTRef, {type,_,tuple,any}, UsedVars) ->
+    UsedVars;
+collect_vars({_Mod,SameName,Arity} = FullADTRef, {type,_,SameName,ArgForms},
+	     UsedVars) ->
+    case length(ArgForms) =:= Arity of
+	true ->
+	    VarArgs = [V || {var,_,V} <- ArgForms, V =/= '_'],
+	    case length(VarArgs) =:= Arity of
+		true ->
+		    AddToList = fun(X,L) -> [X | L] end,
+		    lists:zipwith(AddToList, VarArgs, UsedVars);
+		false ->
+		    [[0|L] || L <- UsedVars]
+	    end;
+	false ->
+	    multi_collect_vars(FullADTRef, ArgForms, UsedVars)
+    end;
+collect_vars(FullADTRef, {type,_,_Name,ArgForms}, UsedVars) ->
+    multi_collect_vars(FullADTRef, ArgForms, UsedVars);
+collect_vars({SameMod,SameName,_Arity} = FullADTRef,
+	     {remote_type,_,[{atom,_,SameMod},{atom,_,SameName},ArgForms]},
+	     UsedVars) ->
+    collect_vars(FullADTRef, {type,?anno(0),SameName,ArgForms}, UsedVars);
+collect_vars(FullADTRef, {remote_type,_,[_RemModForm,_NameForm,ArgForms]},
+	     UsedVars) ->
+    multi_collect_vars(FullADTRef, ArgForms, UsedVars);
+collect_vars(_FullADTRef, _Call, UsedVars) ->
+    UsedVars.
+
+-spec multi_collect_vars(full_imm_type_ref(), [abs_type()],
+			 [[var_name() | 0]]) -> [[var_name() | 0]].
+multi_collect_vars({_Mod,_Name,Arity} = FullADTRef, Forms, UsedVars) ->
+    NoUsedVars = lists:duplicate(Arity, []),
+    MoreUsedVars = [collect_vars(FullADTRef,T,NoUsedVars) || T <- Forms],
+    CombineVars = fun(L1,L2) -> lists:zipwith(fun erlang:'++'/2, L1, L2) end,
+    lists:foldl(CombineVars, UsedVars, MoreUsedVars).
+
+-ifdef(NO_MODULES_IN_OPAQUES).
+-type var_substs_dict() :: dict().
+-else.
+-type var_substs_dict() :: dict:dict(var_name(),abs_type()).
+-endif.
+-spec update_vars(abs_type(), var_substs_dict(), boolean()) -> abs_type().
+update_vars({paren_type,Line,[Type]}, VarSubstsDict, UnboundToAny) ->
+    {paren_type, Line, [update_vars(Type,VarSubstsDict,UnboundToAny)]};
+update_vars({ann_type,Line,[Var,Type]}, VarSubstsDict, UnboundToAny) ->
+    {ann_type, Line, [Var,update_vars(Type,VarSubstsDict,UnboundToAny)]};
+update_vars({var,Line,VarName} = Call, VarSubstsDict, UnboundToAny) ->
+    case dict:find(VarName, VarSubstsDict) of
+	{ok,SubstType} ->
+	    SubstType;
+	error when UnboundToAny =:= false ->
+	    Call;
+	error when UnboundToAny =:= true ->
+	    {type,Line,any,[]}
+    end;
+update_vars({remote_type,Line,[RemModForm,NameForm,ArgForms]}, VarSubstsDict,
+	    UnboundToAny) ->
+    NewArgForms = [update_vars(A,VarSubstsDict,UnboundToAny) || A <- ArgForms],
+    {remote_type, Line, [RemModForm,NameForm,NewArgForms]};
+update_vars({T,_,tuple,any} = Call, _VarSubstsDict, _UnboundToAny) when ?IS_TYPE_TAG(T) ->
+    Call;
+update_vars({T,Line,Name,ArgForms}, VarSubstsDict, UnboundToAny) when ?IS_TYPE_TAG(T) ->
+    NewArgForms = [update_vars(A,VarSubstsDict,UnboundToAny) || A <- ArgForms],
+    {T, Line, Name, NewArgForms};
+update_vars(Call, _VarSubstsDict, _UnboundToAny) ->
+    Call.
+
+
+%%------------------------------------------------------------------------------
+%% Match-related functions
+%%------------------------------------------------------------------------------
+
+-spec get_pattern(position(), [abs_type()]) -> pattern().
+get_pattern(TargetPos, FieldForms) ->
+    {0,RevPattern} = lists:foldl(fun add_field/2, {TargetPos,[]}, FieldForms),
+    list_to_tuple(lists:reverse(RevPattern)).
+
+-spec add_field(abs_type(), {non_neg_integer(),[pat_field()]}) ->
+	  {non_neg_integer(),[pat_field(),...]}.
+add_field(_Type, {1,Acc}) ->
+    {0, [1|Acc]};
+add_field({atom,_,Tag}, {Left,Acc}) ->
+    {erlang:max(0,Left-1), [Tag|Acc]};
+add_field(_Type, {Left,Acc}) ->
+    {erlang:max(0,Left-1), [0|Acc]}.
+
+%% @private
+-spec match(pattern(), tuple()) -> term().
+match(Pattern, Term) when tuple_size(Pattern) =:= tuple_size(Term) ->
+    match(tuple_to_list(Pattern), tuple_to_list(Term), none, false);
+match(_Pattern, _Term) ->
+    throw(no_match).
+
+-spec match([pat_field()], [term()], 'none' | {'ok',T}, boolean()) -> T.
+match([], [], {ok,Target}, _TypeMode) ->
+    Target;
+match([0|PatRest], [_|ToMatchRest], Acc, TypeMode) ->
+    match(PatRest, ToMatchRest, Acc, TypeMode);
+match([1|PatRest], [Target|ToMatchRest], none, TypeMode) ->
+    match(PatRest, ToMatchRest, {ok,Target}, TypeMode);
+match([Tag|PatRest], [X|ToMatchRest], Acc, TypeMode) when is_atom(Tag) ->
+    MatchesTag =
+	case TypeMode of
+	    true  -> can_be_tag(Tag, X);
+	    false -> Tag =:= X
+	end,
+    case MatchesTag of
+	true  -> match(PatRest, ToMatchRest, Acc, TypeMode);
+	false -> throw(no_match)
+    end.
+
+%% CAUTION: these must be sorted
+-define(NON_ATOM_TYPES,
+	[arity,binary,bitstring,byte,char,float,'fun',function,integer,iodata,
+	 iolist,list,maybe_improper_list,mfa,neg_integer,nil,no_return,
+	 non_neg_integer,none,nonempty_improper_list,nonempty_list,
+	 nonempty_maybe_improper_list,nonempty_string,number,pid,port,
+	 pos_integer,range,record,reference,string,tuple]).
+-define(NON_TUPLE_TYPES,
+	[arity,atom,binary,bitstring,bool,boolean,byte,char,float,'fun',
+	 function,identifier,integer,iodata,iolist,list,maybe_improper_list,
+	 neg_integer,nil,no_return,node,non_neg_integer,none,
+	 nonempty_improper_list,nonempty_list,nonempty_maybe_improper_list,
+	 nonempty_string,number,pid,port,pos_integer,range,reference,string,
+	 timeout]).
+-define(NO_HEAD_TYPES,
+	[arity,atom,binary,bitstring,bool,boolean,byte,char,float,'fun',
+	 function,identifier,integer,mfa,module,neg_integer,nil,no_return,node,
+	 non_neg_integer,none,number,pid,port,pos_integer,range,record,
+	 reference,timeout,tuple]).
+
+-spec can_be_tag(atom(), abs_type()) -> boolean().
+can_be_tag(Tag, {ann_type,_,[_Var,Type]}) ->
+    can_be_tag(Tag, Type);
+can_be_tag(Tag, {paren_type,_,[Type]}) ->
+    can_be_tag(Tag, Type);
+can_be_tag(Tag, {atom,_,Atom}) ->
+    Tag =:= Atom;
+can_be_tag(_Tag, {integer,_,_Int}) ->
+    false;
+can_be_tag(_Tag, {op,_,_Op,_Arg}) ->
+    false;
+can_be_tag(_Tag, {op,_,_Op,_Arg1,_Arg2}) ->
+    false;
+can_be_tag(Tag, {type,_,BName,[]}) when BName =:= bool; BName =:= boolean ->
+    is_boolean(Tag);
+can_be_tag(Tag, {type,_,timeout,[]}) ->
+    Tag =:= infinity;
+can_be_tag(Tag, {type,_,union,Choices}) ->
+    lists:any(fun(C) -> can_be_tag(Tag,C) end, Choices);
+can_be_tag(_Tag, {type,_,Name,_Args}) ->
+    not ordsets:is_element(Name, ?NON_ATOM_TYPES);
+can_be_tag(_Tag, _Type) ->
+    true.
+
+-spec cant_match(pattern(), abs_type()) -> boolean().
+cant_match(Pattern, {ann_type,_,[_Var,Type]}) ->
+    cant_match(Pattern, Type);
+cant_match(Pattern, {paren_type,_,[Type]}) ->
+    cant_match(Pattern, Type);
+cant_match(_Pattern, {atom,_,_Atom}) ->
+    true;
+cant_match(_Pattern, {integer,_,_Int}) ->
+    true;
+cant_match(_Pattern, {op,_,_Op,_Arg}) ->
+    true;
+cant_match(_Pattern, {op,_,_Op,_Arg1,_Arg2}) ->
+    true;
+cant_match(Pattern, {type,Anno,mfa,[]}) ->
+    MFA_Ts = [{type,Anno,atom,[]}, {type,Anno,atom,[]}, {type,Anno,arity,[]}],
+    cant_match(Pattern, {type,Anno,tuple,MFA_Ts});
+cant_match(Pattern, {type,_,union,Choices}) ->
+    lists:all(fun(C) -> cant_match(Pattern,C) end, Choices);
+cant_match(_Pattern, {type,_,tuple,any}) ->
+    false;
+cant_match(Pattern, {type,_,tuple,Fields}) ->
+    tuple_size(Pattern) =/= length(Fields) orelse
+    try match(tuple_to_list(Pattern), Fields, none, true) of
+	_ -> false
+    catch
+	throw:no_match -> true
+    end;
+cant_match(_Pattern, {type,_,Name,_Args}) ->
+    ordsets:is_element(Name, ?NON_TUPLE_TYPES);
+cant_match(_Pattern, _Type) ->
+    false.
+
+-spec cant_have_head(abs_type()) -> boolean().
+cant_have_head({ann_type,_,[_Var,Type]}) ->
+    cant_have_head(Type);
+cant_have_head({paren_type,_,[Type]}) ->
+    cant_have_head(Type);
+cant_have_head({atom,_,_Atom}) ->
+    true;
+cant_have_head({integer,_,_Int}) ->
+    true;
+cant_have_head({op,_,_Op,_Arg}) ->
+    true;
+cant_have_head({op,_,_Op,_Arg1,_Arg2}) ->
+    true;
+cant_have_head({type,_,union,Choices}) ->
+    lists:all(fun cant_have_head/1, Choices);
+cant_have_head({type,_,Name,_Args}) ->
+    ordsets:is_element(Name, ?NO_HEAD_TYPES);
+cant_have_head(_Type) ->
+    false.
+
+%% Only covers atoms, integers and tuples, i.e. those that can be specified
+%% through singleton types.
+-spec term_to_singleton_type(atom() | integer()
+			     | loose_tuple(atom() | integer())) -> abs_type().
+term_to_singleton_type(Atom) when is_atom(Atom) ->
+    {atom,?anno(0),Atom};
+term_to_singleton_type(Int) when is_integer(Int), Int >= 0 ->
+    {integer,?anno(0),Int};
+term_to_singleton_type(Int) when is_integer(Int), Int < 0 ->
+    A = ?anno(0),
+    {op,A,'-',{integer,A,-Int}};
+term_to_singleton_type(Tuple) when is_tuple(Tuple) ->
+    Fields = tuple_to_list(Tuple),
+    {type,?anno(0),tuple,[term_to_singleton_type(F) || F <- Fields]}.
+
+
+%%------------------------------------------------------------------------------
+%% Instance testing functions
+%%------------------------------------------------------------------------------
+
+%% CAUTION: this must be sorted
+-define(EQUIV_TYPES,
+	[{arity, {type,0,range,[{integer,0,0},{integer,0,255}]}},
+	 {bool, {type,0,boolean,[]}},
+	 {byte, {type,0,range,[{integer,0,0},{integer,0,255}]}},
+	 {char, {type,0,range,[{integer,0,0},{integer,0,16#10ffff}]}},
+	 {function, {type,0,'fun',[]}},
+	 {identifier, {type,0,union,[{type,0,pid,[]},{type,0,port,[]},
+				     {type,0,reference,[]}]}},
+	 {iodata, {type,0,union,[{type,0,binary,[]},{type,0,iolist,[]}]}},
+	 {iolist, {type,0,maybe_improper_list,
+		   [{type,0,union,[{type,0,byte,[]},{type,0,binary,[]},
+				   {type,0,iolist,[]}]},
+		    {type,0,binary,[]}]}},
+	 {list, {type,0,list,[{type,0,any,[]}]}},
+	 {maybe_improper_list, {type,0,maybe_improper_list,[{type,0,any,[]},
+							    {type,0,any,[]}]}},
+	 {mfa, {type,0,tuple,[{type,0,atom,[]},{type,0,atom,[]},
+			      {type,0,arity,[]}]}},
+	 {node, {type,0,atom,[]}},
+	 {nonempty_list, {type,0,nonempty_list,[{type,0,any,[]}]}},
+	 {nonempty_maybe_improper_list, {type,0,nonempty_maybe_improper_list,
+					 [{type,0,any,[]},{type,0,any,[]}]}},
+	 {nonempty_string, {type,0,nonempty_list,[{type,0,char,[]}]}},
+	 {string, {type,0,list,[{type,0,char,[]}]}},
+	 {term, {type,0,any,[]}},
+	 {timeout, {type,0,union,[{atom,0,infinity},
+				  {type,0,non_neg_integer,[]}]}}]).
+
+%% @private
+%% TODO: Most of these functions accept an extended form of abs_type(), namely
+%%	 the addition of a custom wrapper: {'from_mod',mod_name(),...}
+-spec is_instance(term(), mod_name(), abs_type()) -> boolean().
+is_instance(X, Mod, TypeForm) ->
+    is_instance(X, Mod, TypeForm, []).
+
+-spec is_instance(term(), mod_name(), abs_type(), imm_stack()) -> boolean().
+is_instance(X, _Mod, {from_mod,OrigMod,Type}, Stack) ->
+    is_instance(X, OrigMod, Type, Stack);
+is_instance(_X, _Mod, {var,_,'_'}, _Stack) ->
+    true;
+is_instance(_X, _Mod, {var,_,Name}, _Stack) ->
+    %% All unconstrained spec vars have been replaced by 'any()' and we always
+    %% replace the variables on the RHS of types before recursing into them.
+    %% Provided that '-type' declarations contain no unbound variables, we
+    %% don't expect to find any non-'_' variables while recursing.
+    throw({'$typeserver',{unbound_var_in_type_declaration,Name}});
+is_instance(X, Mod, {ann_type,_,[_Var,Type]}, Stack) ->
+    is_instance(X, Mod, Type, Stack);
+is_instance(X, Mod, {paren_type,_,[Type]}, Stack) ->
+    is_instance(X, Mod, Type, Stack);
+is_instance(X, Mod, {remote_type,_,[{atom,_,RemMod},{atom,_,Name},ArgForms]},
+	    Stack) ->
+    is_custom_instance(X, Mod, RemMod, Name, ArgForms, true, Stack);
+is_instance(SameAtom, _Mod, {atom,_,SameAtom}, _Stack) ->
+    true;
+is_instance(SameInt, _Mod, {integer,_,SameInt}, _Stack) ->
+    true;
+is_instance(X, _Mod, {op,_,_Op,_Arg} = Expr, _Stack) ->
+    is_int_const(X, Expr);
+is_instance(X, _Mod, {op,_,_Op,_Arg1,_Arg2} = Expr, _Stack) ->
+    is_int_const(X, Expr);
+is_instance(_X, _Mod, {type,_,any,[]}, _Stack) ->
+    true;
+is_instance(X, _Mod, {type,_,atom,[]}, _Stack) ->
+    is_atom(X);
+is_instance(X, _Mod, {type,_,binary,[]}, _Stack) ->
+    is_binary(X);
+is_instance(X, _Mod, {type,_,binary,[BaseExpr,UnitExpr]}, _Stack) ->
+    %% <<_:X,_:_*Y>> means "bitstrings of X + k*Y bits, k >= 0"
+    case eval_int(BaseExpr) of
+	{ok,Base} when Base >= 0 ->
+	    case eval_int(UnitExpr) of
+		{ok,Unit} when Unit >= 0 ->
+		    case is_bitstring(X) of
+			true ->
+			    BitSizeX = bit_size(X),
+			    case Unit =:= 0 of
+				true ->
+				    BitSizeX =:= Base;
+			        false ->
+				    BitSizeX >= Base
+					andalso
+					  (BitSizeX - Base) rem Unit =:= 0
+			    end;
+			false -> false
+		    end;
+		_ ->
+		    abs_expr_error(invalid_unit, UnitExpr)
+	    end;
+	_ ->
+	    abs_expr_error(invalid_base, BaseExpr)
+    end;
+is_instance(X, _Mod, {type,_,bitstring,[]}, _Stack) ->
+    is_bitstring(X);
+is_instance(X, _Mod, {type,_,boolean,[]}, _Stack) ->
+    is_boolean(X);
+is_instance(X, _Mod, {type,_,float,[]}, _Stack) ->
+    is_float(X);
+is_instance(X, _Mod, {type,_,'fun',[]}, _Stack) ->
+    is_function(X);
+%% TODO: how to check range type? random inputs? special case for 0-arity?
+is_instance(X, _Mod, {type,_,'fun',[{type,_,any,[]},_Range]}, _Stack) ->
+    is_function(X);
+is_instance(X, _Mod, {type,_,'fun',[{type,_,product,Domain},_Range]}, _Stack) ->
+    is_function(X, length(Domain));
+is_instance(X, _Mod, {type,_,integer,[]}, _Stack) ->
+    is_integer(X);
+is_instance(X, Mod, {type,_,list,[Type]}, _Stack) ->
+    list_test(X, Mod, Type, dummy, true, true, false);
+is_instance(X, Mod, {type,_,maybe_improper_list,[Cont,Term]}, _Stack) ->
+    list_test(X, Mod, Cont, Term, true, true, true);
+is_instance(X, _Mod, {type,_,module,[]}, _Stack) ->
+    is_atom(X) orelse
+    is_tuple(X) andalso X =/= {} andalso is_atom(element(1,X));
+is_instance([], _Mod, {type,_,nil,[]}, _Stack) ->
+    true;
+is_instance(X, _Mod, {type,_,neg_integer,[]}, _Stack) ->
+    is_integer(X) andalso X < 0;
+is_instance(X, _Mod, {type,_,non_neg_integer,[]}, _Stack) ->
+    is_integer(X) andalso X >= 0;
+is_instance(X, Mod, {type,_,nonempty_list,[Type]}, _Stack) ->
+    list_test(X, Mod, Type, dummy, false, true, false);
+is_instance(X, Mod, {type,_,nonempty_improper_list,[Cont,Term]}, _Stack) ->
+    list_test(X, Mod, Cont, Term, false, false, true);
+is_instance(X, Mod, {type,_,nonempty_maybe_improper_list,[Cont,Term]},
+	    _Stack) ->
+    list_test(X, Mod, Cont, Term, false, true, true);
+is_instance(X, _Mod, {type,_,number,[]}, _Stack) ->
+    is_number(X);
+is_instance(X, _Mod, {type,_,pid,[]}, _Stack) ->
+    is_pid(X);
+is_instance(X, _Mod, {type,_,port,[]}, _Stack) ->
+    is_port(X);
+is_instance(X, _Mod, {type,_,pos_integer,[]}, _Stack) ->
+    is_integer(X) andalso X > 0;
+is_instance(_X, _Mod, {type,_,product,_Elements}, _Stack) ->
+    throw({'$typeserver',{internal,product_in_is_instance}});
+is_instance(X, _Mod, {type,_,range,[LowExpr,HighExpr]}, _Stack) ->
+    case {eval_int(LowExpr),eval_int(HighExpr)} of
+	{{ok,Low},{ok,High}} when Low =< High ->
+	    X >= Low andalso X =< High;
+	_ ->
+	    abs_expr_error(invalid_range, LowExpr, HighExpr)
+    end;
+is_instance(X, Mod, {type,_,record,[{atom,_,Name} = NameForm | RawSubsts]},
+	    Stack) ->
+    Substs = [{N,T} || {type,_,field_type,[{atom,_,N},T]} <- RawSubsts],
+    SubstsDict = dict:from_list(Substs),
+    case get_type_repr(Mod, {record,Name,0}, false) of
+	{ok,{abs_record,OrigFields}} ->
+	    Fields = [case dict:find(FieldName, SubstsDict) of
+			  {ok,NewFieldType} -> NewFieldType;
+			  error             -> OrigFieldType
+		      end
+		      || {FieldName,OrigFieldType} <- OrigFields],
+	    is_instance(X, Mod, {type,?anno(0),tuple,[NameForm|Fields]}, Stack);
+	{error,Reason} ->
+	    throw({'$typeserver',Reason})
+    end;
+is_instance(X, _Mod, {type,_,reference,[]}, _Stack) ->
+    is_reference(X);
+is_instance(X, _Mod, {type,_,tuple,any}, _Stack) ->
+    is_tuple(X);
+is_instance(X, Mod, {type,_,tuple,Fields}, _Stack) ->
+    is_tuple(X) andalso tuple_test(tuple_to_list(X), Mod, Fields);
+is_instance(X, Mod, {type,_,union,Choices}, Stack) ->
+    IsInstance = fun(Choice) -> is_instance(X,Mod,Choice,Stack) end,
+    lists:any(IsInstance, Choices);
+is_instance(X, Mod, {T,_,Name,[]}, Stack) when ?IS_TYPE_TAG(T) ->
+    case orddict:find(Name, ?EQUIV_TYPES) of
+	{ok,EquivType} ->
+	    is_instance(X, Mod, EquivType, Stack);
+	error ->
+	    is_maybe_hard_adt(X, Mod, Name, [], Stack)
+    end;
+is_instance(X, Mod, {T,_,Name,ArgForms}, Stack) when ?IS_TYPE_TAG(T) ->
+    is_maybe_hard_adt(X, Mod, Name, ArgForms, Stack);
+is_instance(_X, _Mod, _Type, _Stack) ->
+    false.
+
+-spec is_int_const(term(), abs_expr()) -> boolean().
+is_int_const(X, Expr) ->
+    case eval_int(Expr) of
+	{ok,Int} ->
+	    X =:= Int;
+	error ->
+	    abs_expr_error(invalid_int_const, Expr)
+    end.
+
+%% TODO: We implicitly add the '| []' at the termination of maybe_improper_list.
+%% TODO: We ignore a '[]' termination in improper_list.
+-spec list_test(term(), mod_name(), abs_type(), 'dummy' | abs_type(), boolean(),
+		boolean(), boolean()) -> boolean().
+list_test(X, Mod, Content, Termination, CanEmpty, CanProper, CanImproper) ->
+    is_list(X) andalso
+    list_rec(X, Mod, Content, Termination, CanEmpty, CanProper, CanImproper).
+
+-spec list_rec(term(), mod_name(), abs_type(), 'dummy' | abs_type(), boolean(),
+	       boolean(), boolean()) -> boolean().
+list_rec([], _Mod, _Content, _Termination, CanEmpty, CanProper, _CanImproper) ->
+    CanEmpty andalso CanProper;
+list_rec([X | Rest], Mod, Content, Termination, _CanEmpty, CanProper,
+	 CanImproper) ->
+    is_instance(X, Mod, Content, []) andalso
+    list_rec(Rest, Mod, Content, Termination, true, CanProper, CanImproper);
+list_rec(X, Mod, _Content, Termination, _CanEmpty, _CanProper, CanImproper) ->
+    CanImproper andalso is_instance(X, Mod, Termination, []).
+
+-spec tuple_test([term()], mod_name(), [abs_type()]) -> boolean().
+tuple_test([], _Mod, []) ->
+    true;
+tuple_test([X | XTail], Mod, [T | TTail]) ->
+    is_instance(X, Mod, T, []) andalso tuple_test(XTail, Mod, TTail);
+tuple_test(_, _Mod, _) ->
+    false.
+
+-spec is_maybe_hard_adt(term(), mod_name(), type_name(), [abs_type()],
+			imm_stack()) -> boolean().
+is_maybe_hard_adt(X, Mod, Name, ArgForms, Stack) ->
+    case orddict:find({Name,length(ArgForms)}, ?HARD_ADTS) of
+	{ok,ADTMod} ->
+	    is_custom_instance(X, Mod, ADTMod, Name, ArgForms, true, Stack);
+	error ->
+	    is_custom_instance(X, Mod, Mod, Name, ArgForms, false, Stack)
+    end.
+
+-spec is_custom_instance(term(), mod_name(), mod_name(), type_name(),
+			 [abs_type()], boolean(), imm_stack()) -> boolean().
+is_custom_instance(X, Mod, RemMod, Name, RawArgForms, IsRemote, Stack) ->
+    ArgForms = case Mod =/= RemMod of
+		   true  -> [{from_mod,Mod,A} || A <- RawArgForms];
+		   false -> RawArgForms
+	       end,
+    Arity = length(ArgForms),
+    FullTypeRef = {RemMod,Name,Arity},
+    case lists:member(FullTypeRef, Stack) of
+	true ->
+	    throw({'$typeserver',{self_reference,FullTypeRef}});
+	false ->
+	    TypeRef = {type,Name,Arity},
+	    AbsType = get_abs_type(RemMod, TypeRef, ArgForms, IsRemote),
+	    is_instance(X, RemMod, AbsType, [FullTypeRef|Stack])
+    end.
+
+-spec get_abs_type(mod_name(), type_ref(), [abs_type()], boolean()) ->
+	  abs_type().
+get_abs_type(RemMod, TypeRef, ArgForms, IsRemote) ->
+    case get_type_repr(RemMod, TypeRef, IsRemote) of
+	{ok,TypeRepr} ->
+	    {FinalAbsType,SymbInfo,VarNames} =
+		case TypeRepr of
+		    {cached,_FinType,FAT,SI} -> {FAT,SI,[]};
+		    {abs_type,FAT,VN,SI}     -> {FAT,SI,VN}
+		end,
+	    AbsType =
+		case SymbInfo of
+		    not_symb               -> FinalAbsType;
+		    {orig_abs,OrigAbsType} -> OrigAbsType
+		end,
+	    VarSubstsDict = dict:from_list(lists:zip(VarNames,ArgForms)),
+	    update_vars(AbsType, VarSubstsDict, false);
+	{error,Reason} ->
+	    throw({'$typeserver',Reason})
+    end.
+
+-spec abs_expr_error(atom(), abs_expr()) -> no_return().
+abs_expr_error(ImmReason, Expr) ->
+    {error,Reason} = expr_error(ImmReason, Expr),
+    throw({'$typeserver',Reason}).
+
+-spec abs_expr_error(atom(), abs_expr(), abs_expr()) -> no_return().
+abs_expr_error(ImmReason, Expr1, Expr2) ->
+    {error,Reason} = expr_error(ImmReason, Expr1, Expr2),
+    throw({'$typeserver',Reason}).
+
+
+%%------------------------------------------------------------------------------
+%% Type translation functions
+%%------------------------------------------------------------------------------
+
+-spec convert(mod_name(), abs_type(), state()) ->
+	  rich_result2(fin_type(),state()).
+convert(Mod, TypeForm, State) ->
+    case convert(Mod, TypeForm, State, [], dict:new()) of
+	{ok,{simple,Type},NewState} ->
+	    {ok, Type, NewState};
+	{ok,{rec,_RecFun,_RecArgs},_NewState} ->
+	    {error, {internal,rec_returned_to_toplevel}};
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert(mod_name(), abs_type(), state(), stack(), var_dict()) ->
+	  rich_result2(ret_type(),state()).
+convert(Mod, {paren_type,_,[Type]}, State, Stack, VarDict) ->
+    convert(Mod, Type, State, Stack, VarDict);
+convert(Mod, {ann_type,_,[_Var,Type]}, State, Stack, VarDict) ->
+    convert(Mod, Type, State, Stack, VarDict);
+convert(_Mod, {var,_,'_'}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:any()}, State};
+convert(_Mod, {var,_,VarName}, State, _Stack, VarDict) ->
+    case dict:find(VarName, VarDict) of
+	%% TODO: do we need to check if we are at toplevel of a recursive?
+	{ok,RetType} -> {ok, RetType, State};
+	error        -> {error, {unbound_var,VarName}}
+    end;
+convert(Mod, {remote_type,_,[{atom,_,RemMod},{atom,_,Name},ArgForms]}, State,
+	Stack, VarDict) ->
+    case prepare_for_remote(RemMod, Name, length(ArgForms), State) of
+	{ok,NewState} ->
+	    convert_custom(Mod,RemMod,Name,ArgForms,NewState,Stack,VarDict);
+	{error,_Reason} = Error ->
+	    Error
+    end;
+convert(_Mod, {atom,_,Atom}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:exactly(Atom)}, State};
+convert(_Mod, {integer,_,_Int} = IntExpr, State, _Stack, _VarDict) ->
+    convert_integer(IntExpr, State);
+convert(_Mod, {op,_,_Op,_Arg} = OpExpr, State, _Stack, _VarDict) ->
+    convert_integer(OpExpr, State);
+convert(_Mod, {op,_,_Op,_Arg1,_Arg2} = OpExpr, State, _Stack, _VarDict) ->
+    convert_integer(OpExpr, State);
+convert(_Mod, {type,_,binary,[BaseExpr,UnitExpr]}, State, _Stack, _VarDict) ->
+    %% <<_:X,_:_*Y>> means "bitstrings of X + k*Y bits, k >= 0"
+    case eval_int(BaseExpr) of
+	{ok,0} ->
+	    case eval_int(UnitExpr) of
+		{ok,0} -> {ok, {simple,proper_types:exactly(<<>>)}, State};
+		{ok,1} -> {ok, {simple,proper_types:bitstring()}, State};
+		{ok,8} -> {ok, {simple,proper_types:binary()}, State};
+		{ok,N} when N > 0 ->
+		    Gen = ?LET(L, proper_types:list(proper_types:bitstring(N)),
+			       concat_bitstrings(L)),
+		    {ok, {simple,Gen}, State};
+		_      -> expr_error(invalid_unit, UnitExpr)
+	    end;
+	{ok,Base} when Base > 0 ->
+	    Head = proper_types:bitstring(Base),
+	    case eval_int(UnitExpr) of
+		{ok,0} -> {ok, {simple,Head}, State};
+		{ok,1} ->
+		    Tail = proper_types:bitstring(),
+		    {ok, {simple,concat_binary_gens(Head, Tail)}, State};
+		{ok,8} ->
+		    Tail = proper_types:binary(),
+		    {ok, {simple,concat_binary_gens(Head, Tail)}, State};
+		{ok,N} when N > 0 ->
+		    Tail =
+			?LET(L, proper_types:list(proper_types:bitstring(N)),
+			     concat_bitstrings(L)),
+		    {ok, {simple,concat_binary_gens(Head, Tail)}, State};
+		_      -> expr_error(invalid_unit, UnitExpr)
+	    end;
+	_ ->
+	    expr_error(invalid_base, BaseExpr)
+    end;
+convert(_Mod, {type,_,range,[LowExpr,HighExpr]}, State, _Stack, _VarDict) ->
+    case {eval_int(LowExpr),eval_int(HighExpr)} of
+	{{ok,Low},{ok,High}} when Low =< High ->
+	    {ok, {simple,proper_types:integer(Low,High)}, State};
+	_ ->
+	    expr_error(invalid_range, LowExpr, HighExpr)
+    end;
+convert(_Mod, {type,_,nil,[]}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:exactly([])}, State};
+convert(Mod, {type,_,list,[ElemForm]}, State, Stack, VarDict) ->
+    convert_list(Mod, false, ElemForm, State, Stack, VarDict);
+convert(Mod, {type,_,nonempty_list,[ElemForm]}, State, Stack, VarDict) ->
+    convert_list(Mod, true, ElemForm, State, Stack, VarDict);
+convert(_Mod, {type,_,nonempty_list,[]}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:non_empty(proper_types:list())}, State};
+convert(_Mod, {type,_,nonempty_string,[]}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:non_empty(proper_types:string())}, State};
+convert(_Mod, {type,_,tuple,any}, State, _Stack, _VarDict) ->
+    {ok, {simple,proper_types:tuple()}, State};
+convert(Mod, {type,_,tuple,ElemForms}, State, Stack, VarDict) ->
+    convert_tuple(Mod, ElemForms, false, State, Stack, VarDict);
+convert(Mod, {type,_,'$fixed_list',ElemForms}, State, Stack, VarDict) ->
+    convert_tuple(Mod, ElemForms, true, State, Stack, VarDict);
+convert(Mod, {type,_,record,[{atom,_,Name}|FieldForms]}, State, Stack,
+	VarDict) ->
+    convert_record(Mod, Name, FieldForms, State, Stack, VarDict);
+convert(Mod, {type,_,union,ChoiceForms}, State, Stack, VarDict) ->
+    convert_union(Mod, ChoiceForms, State, Stack, VarDict);
+convert(Mod, {type,_,'fun',[{type,_,product,Domain},Range]}, State, Stack,
+	VarDict) ->
+    convert_fun(Mod, length(Domain), Range, State, Stack, VarDict);
+%% TODO: These types should be replaced with accurate types.
+%% TODO: Add support for nonempty_improper_list/2.
+convert(Mod, {type,Anno,maybe_improper_list,[]}, State, Stack, VarDict) ->
+    convert(Mod, {type,Anno,list,[]}, State, Stack, VarDict);
+convert(Mod, {type,A,maybe_improper_list,[Cont,_Ter]}, State, Stack, VarDict) ->
+    convert(Mod, {type,A,list,[Cont]}, State, Stack, VarDict);
+convert(Mod, {type,A,nonempty_maybe_improper_list,[]}, State, Stack, VarDict) ->
+    convert(Mod, {type,A,nonempty_list,[]}, State, Stack, VarDict);
+convert(Mod, {type,A,nonempty_maybe_improper_list,[Cont,_Term]}, State, Stack,
+	VarDict) ->
+    convert(Mod, {type,A,nonempty_list,[Cont]}, State, Stack, VarDict);
+convert(Mod, {type,A,iodata,[]}, State, Stack, VarDict) ->
+    RealType = {type,A,union,[{type,A,binary,[]},{type,A,iolist,[]}]},
+    convert(Mod, RealType, State, Stack, VarDict);
+convert(Mod, {T,_,Name,[]}, State, Stack, VarDict) when ?IS_TYPE_TAG(T) ->
+    case ordsets:is_element(Name, ?STD_TYPES_0) of
+	true ->
+	    {ok, {simple,proper_types:Name()}, State};
+	false ->
+	    convert_maybe_hard_adt(Mod, Name, [], State, Stack, VarDict)
+    end;
+convert(Mod, {T,_,Name,ArgForms}, State, Stack, VarDict) when ?IS_TYPE_TAG(T) ->
+    convert_maybe_hard_adt(Mod, Name, ArgForms, State, Stack, VarDict);
+convert(_Mod, TypeForm, _State, _Stack, _VarDict) ->
+    {error, {unsupported_type,TypeForm}}.
+
+-spec concat_bitstrings([bitstring()]) -> bitstring().
+concat_bitstrings(BitStrings) ->
+    concat_bitstrings_tr(BitStrings, <<>>).
+
+-spec concat_bitstrings_tr([bitstring()], bitstring()) -> bitstring().
+concat_bitstrings_tr([], Acc) ->
+    Acc;
+concat_bitstrings_tr([BitString | Rest], Acc) ->
+    concat_bitstrings_tr(Rest, <<Acc/bits,BitString/bits>>).
+
+-spec concat_binary_gens(fin_type(), fin_type()) -> fin_type().
+concat_binary_gens(HeadType, TailType) ->
+    ?LET({H,T}, {HeadType,TailType}, <<H/bits,T/bits>>).
+
+-spec convert_fun(mod_name(), arity(), abs_type(), state(), stack(),
+		  var_dict()) -> rich_result2(ret_type(),state()).
+convert_fun(Mod, Arity, Range, State, Stack, VarDict) ->
+    case convert(Mod, Range, State, ['fun' | Stack], VarDict) of
+	{ok,{simple,RangeType},NewState} ->
+	    {ok, {simple,proper_types:function(Arity,RangeType)}, NewState};
+	{ok,{rec,RecFun,RecArgs},NewState} ->
+	    case at_toplevel(RecArgs, Stack) of
+		true  -> base_case_error(Stack);
+		false -> convert_rec_fun(Arity, RecFun, RecArgs, NewState)
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_rec_fun(arity(), rec_fun(), rec_args(), state()) ->
+	  {'ok',ret_type(),state()}.
+convert_rec_fun(Arity, RecFun, RecArgs, State) ->
+    %% We bind the generated value by size.
+    NewRecFun =
+	fun(GenFuns,Size) ->
+	    proper_types:function(Arity, RecFun(GenFuns,Size))
+	end,
+    NewRecArgs = clean_rec_args(RecArgs),
+    {ok, {rec,NewRecFun,NewRecArgs}, State}.
+
+-spec convert_list(mod_name(), boolean(), abs_type(), state(), stack(),
+		   var_dict()) -> rich_result2(ret_type(),state()).
+convert_list(Mod, NonEmpty, ElemForm, State, Stack, VarDict) ->
+    case convert(Mod, ElemForm, State, [list | Stack], VarDict) of
+	{ok,{simple,ElemType},NewState} ->
+	    InnerType = proper_types:list(ElemType),
+	    FinType = case NonEmpty of
+			  true  -> proper_types:non_empty(InnerType);
+			  false -> InnerType
+		      end,
+	    {ok, {simple,FinType}, NewState};
+	{ok,{rec,RecFun,RecArgs},NewState} ->
+	    case {at_toplevel(RecArgs,Stack), NonEmpty} of
+		{true,true} ->
+		    base_case_error(Stack);
+		{true,false} ->
+		    NewRecFun =
+			fun(GenFuns,Size) ->
+			    ElemGen = fun(S) -> ?LAZY(RecFun(GenFuns,S)) end,
+			    proper_types:distlist(Size, ElemGen, false)
+			end,
+		    NewRecArgs = clean_rec_args(RecArgs),
+		    {ok, {rec,NewRecFun,NewRecArgs}, NewState};
+		{false,_} ->
+		    {NewRecFun,NewRecArgs} =
+			convert_rec_list(RecFun, RecArgs, NonEmpty),
+		    {ok, {rec,NewRecFun,NewRecArgs}, NewState}
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_rec_list(rec_fun(), rec_args(), boolean()) ->
+	  {rec_fun(),rec_args()}.
+convert_rec_list(RecFun, [{true,FullTypeRef}] = RecArgs, NonEmpty) ->
+    {NewRecFun,_NormalRecArgs} =
+	convert_normal_rec_list(RecFun, RecArgs, NonEmpty),
+    AltRecFun =
+	fun([InstListGen],Size) ->
+	    InstTypesList =
+		proper_types:get_prop(internal_types, InstListGen(Size)),
+	    proper_types:fixed_list([RecFun([fun(_Size) -> I end],0)
+				     || I <- InstTypesList])
+	end,
+    NewRecArgs = [{{list,NonEmpty,AltRecFun},FullTypeRef}],
+    {NewRecFun, NewRecArgs};
+convert_rec_list(RecFun, RecArgs, NonEmpty) ->
+    convert_normal_rec_list(RecFun, RecArgs, NonEmpty).
+
+-spec convert_normal_rec_list(rec_fun(), rec_args(), boolean()) ->
+	  {rec_fun(),rec_args()}.
+convert_normal_rec_list(RecFun, RecArgs, NonEmpty) ->
+    NewRecFun = fun(GenFuns,Size) ->
+		    ElemGen = fun(S) -> RecFun(GenFuns, S) end,
+		    proper_types:distlist(Size, ElemGen, NonEmpty)
+		end,
+    NewRecArgs = clean_rec_args(RecArgs),
+    {NewRecFun, NewRecArgs}.
+
+-spec convert_tuple(mod_name(), [abs_type()], boolean(), state(), stack(),
+		    var_dict()) -> rich_result2(ret_type(),state()).
+convert_tuple(Mod, ElemForms, ToList, State, Stack, VarDict) ->
+    case process_list(Mod, ElemForms, State, [tuple | Stack], VarDict) of
+	{ok,RetTypes,NewState} ->
+	    case combine_ret_types(RetTypes, {tuple,ToList}) of
+		{simple,_FinType} = RetType ->
+		    {ok, RetType, NewState};
+		{rec,_RecFun,RecArgs} = RetType ->
+		    case at_toplevel(RecArgs, Stack) of
+			true  -> base_case_error(Stack);
+			false -> {ok, RetType, NewState}
+		    end
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_union(mod_name(), [abs_type()], state(), stack(), var_dict()) ->
+	  rich_result2(ret_type(),state()).
+convert_union(Mod, ChoiceForms, State, Stack, VarDict) ->
+    case process_list(Mod, ChoiceForms, State, [union | Stack], VarDict) of
+	{ok,RawChoices,NewState} ->
+	    ProcessChoice = fun(T,A) -> process_choice(T,A,Stack) end,
+	    {RevSelfRecs,RevNonSelfRecs,RevNonRecs} =
+		lists:foldl(ProcessChoice, {[],[],[]}, RawChoices),
+	    case {lists:reverse(RevSelfRecs),lists:reverse(RevNonSelfRecs),
+		  lists:reverse(RevNonRecs)} of
+		{_SelfRecs,[],[]} ->
+		    base_case_error(Stack);
+		{[],NonSelfRecs,NonRecs} ->
+		    {ok, combine_ret_types(NonRecs ++ NonSelfRecs, union),
+		     NewState};
+		{SelfRecs,NonSelfRecs,NonRecs} ->
+		    {BCaseRecFun,BCaseRecArgs} =
+			case combine_ret_types(NonRecs ++ NonSelfRecs, union) of
+			    {simple,BCaseType} ->
+				{fun([],_Size) -> BCaseType end,[]};
+			    {rec,BCRecFun,BCRecArgs} ->
+				{BCRecFun,BCRecArgs}
+			end,
+		    NumBCaseGens = length(BCaseRecArgs),
+		    [ParentRef | _Upper] = Stack,
+		    FallbackRecFun = fun([SelfGen],_Size) -> SelfGen(0) end,
+		    FallbackRecArgs = [{false,ParentRef}],
+		    FallbackRetType = {rec,FallbackRecFun,FallbackRecArgs},
+		    {rec,RCaseRecFun,RCaseRecArgs} =
+			combine_ret_types([FallbackRetType] ++ SelfRecs
+					  ++ NonSelfRecs, wunion),
+		    NewRecFun =
+			fun(AllGens,Size) ->
+			    {BCaseGens,RCaseGens} =
+				lists:split(NumBCaseGens, AllGens),
+			    case Size of
+				0 -> BCaseRecFun(BCaseGens,0);
+				_ -> RCaseRecFun(RCaseGens,Size)
+			    end
+			end,
+		    NewRecArgs = BCaseRecArgs ++ RCaseRecArgs,
+		    {ok, {rec,NewRecFun,NewRecArgs}, NewState}
+	    end;
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec process_choice(ret_type(), {[ret_type()],[ret_type()],[ret_type()]},
+		     stack()) -> {[ret_type()],[ret_type()],[ret_type()]}.
+process_choice({simple,_} = RetType, {SelfRecs,NonSelfRecs,NonRecs}, _Stack) ->
+    {SelfRecs, NonSelfRecs, [RetType | NonRecs]};
+process_choice({rec,RecFun,RecArgs}, {SelfRecs,NonSelfRecs,NonRecs}, Stack) ->
+    case at_toplevel(RecArgs, Stack) of
+	true ->
+	    case partition_by_toplevel(RecArgs, Stack, true) of
+		{[],[],_,_} ->
+		    NewRecArgs = clean_rec_args(RecArgs),
+		    {[{rec,RecFun,NewRecArgs} | SelfRecs], NonSelfRecs,
+		     NonRecs};
+		{SelfRecArgs,SelfPos,OtherRecArgs,_OtherPos} ->
+		    NumInstances = length(SelfRecArgs),
+		    IsListInst = fun({true,_FTRef})                  -> false
+				  ; ({{list,_NE,_AltRecFun},_FTRef}) -> true
+				 end,
+		    NewRecFun =
+			case proper_arith:filter(IsListInst,SelfRecArgs) of
+			    {[],[]} ->
+				no_list_inst_rec_fun(RecFun,NumInstances,
+						     SelfPos);
+			    {[{{list,NonEmpty,AltRecFun},_}],[ListInstPos]} ->
+				list_inst_rec_fun(AltRecFun,NumInstances,
+						  SelfPos,NonEmpty,ListInstPos)
+			end,
+		    [{_B,SelfRef} | _] = SelfRecArgs,
+		    NewRecArgs =
+			[{false,SelfRef} | clean_rec_args(OtherRecArgs)],
+		    {[{rec,NewRecFun,NewRecArgs} | SelfRecs], NonSelfRecs,
+		     NonRecs}
+	    end;
+	false ->
+	    NewRecArgs = clean_rec_args(RecArgs),
+	    {SelfRecs, [{rec,RecFun,NewRecArgs} | NonSelfRecs], NonRecs}
+    end.
+
+-spec no_list_inst_rec_fun(rec_fun(), pos_integer(), [position()]) -> rec_fun().
+no_list_inst_rec_fun(RecFun, NumInstances, SelfPos) ->
+    fun([SelfGen|OtherGens], Size) ->
+	?LETSHRINK(
+	    Instances,
+	    %% Size distribution will be a little off if both normal and
+	    %% instance-accepting generators are present.
+	    lists:duplicate(NumInstances, SelfGen(Size div NumInstances)),
+	    begin
+		InstGens = [fun(_Size) -> proper_types:exactly(I) end
+			    || I <- Instances],
+		AllGens = proper_arith:insert(InstGens, SelfPos, OtherGens),
+		RecFun(AllGens, Size)
+	    end)
+    end.
+
+-spec list_inst_rec_fun(rec_fun(), pos_integer(), [position()], boolean(),
+			position()) -> rec_fun().
+list_inst_rec_fun(AltRecFun, NumInstances, SelfPos, NonEmpty, ListInstPos) ->
+    fun([SelfGen|OtherGens], Size) ->
+	?LETSHRINK(
+	    AllInsts,
+	    lists:duplicate(NumInstances - 1, SelfGen(Size div NumInstances))
+	    ++ proper_types:distlist(Size div NumInstances, SelfGen, NonEmpty),
+	    begin
+		{Instances,InstList} = lists:split(NumInstances - 1, AllInsts),
+		InstGens = [fun(_Size) -> proper_types:exactly(I) end
+			    || I <- Instances],
+		InstTypesList = [proper_types:exactly(I) || I <- InstList],
+		InstListGen =
+		    fun(_Size) -> proper_types:fixed_list(InstTypesList) end,
+		AllInstGens = proper_arith:list_insert(ListInstPos, InstListGen,
+						       InstGens),
+		AllGens = proper_arith:insert(AllInstGens, SelfPos, OtherGens),
+		AltRecFun(AllGens, Size)
+	    end)
+    end.
+
+-spec convert_maybe_hard_adt(mod_name(), type_name(), [abs_type()], state(),
+			     stack(), var_dict()) ->
+	  rich_result2(ret_type(),state()).
+convert_maybe_hard_adt(Mod, Name, ArgForms, State, Stack, VarDict) ->
+    Arity = length(ArgForms),
+    case orddict:find({Name,Arity}, ?HARD_ADTS) of
+	{ok,Mod} ->
+	    convert_custom(Mod, Mod, Name, ArgForms, State, Stack, VarDict);
+	{ok,ADTMod} ->
+	    A = ?anno(0),
+	    ADT = {remote_type,A,[{atom,A,ADTMod},{atom,A,Name},ArgForms]},
+	    convert(Mod, ADT, State, Stack, VarDict);
+	error ->
+	    convert_custom(Mod, Mod, Name, ArgForms, State, Stack, VarDict)
+    end.
+
+-spec convert_custom(mod_name(), mod_name(), type_name(), [abs_type()], state(),
+		     stack(), var_dict()) -> rich_result2(ret_type(),state()).
+convert_custom(Mod, RemMod, Name, ArgForms, State, Stack, VarDict) ->
+    case process_list(Mod, ArgForms, State, Stack, VarDict) of
+	{ok,Args,NewState} ->
+	    Arity = length(Args),
+	    TypeRef = {type,Name,Arity},
+	    FullTypeRef = {RemMod,type,Name,Args},
+	    convert_type(TypeRef, FullTypeRef, NewState, Stack);
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_record(mod_name(), type_name(), [abs_type()], state(), stack(),
+		     var_dict()) -> rich_result2(ret_type(),state()).
+convert_record(Mod, Name, RawSubsts, State, Stack, VarDict) ->
+    Substs = [{N,T} || {type,_,field_type,[{atom,_,N},T]} <- RawSubsts],
+    {SubstFields,SubstTypeForms} = lists:unzip(Substs),
+    case process_list(Mod, SubstTypeForms, State, Stack, VarDict) of
+	{ok,SubstTypes,NewState} ->
+	    SubstsDict = dict:from_list(lists:zip(SubstFields, SubstTypes)),
+	    TypeRef = {record,Name,0},
+	    FullTypeRef = {Mod,record,Name,SubstsDict},
+	    convert_type(TypeRef, FullTypeRef, NewState, Stack);
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_type(type_ref(), full_type_ref(), state(), stack()) ->
+	  rich_result2(ret_type(),state()).
+convert_type(TypeRef, {Mod,_Kind,_Name,_Spec} = FullTypeRef, State, Stack) ->
+    case stack_position(FullTypeRef, Stack) of
+	none ->
+	    case get_type_repr(Mod, TypeRef, false, State) of
+		{ok,TypeRepr,NewState} ->
+		    convert_new_type(TypeRef, FullTypeRef, TypeRepr, NewState,
+				     Stack);
+		{error,_Reason} = Error ->
+		    Error
+	    end;
+	1 ->
+	    base_case_error(Stack);
+	_Pos ->
+	    {ok, {rec,fun([Gen],Size) -> Gen(Size) end,[{true,FullTypeRef}]},
+	     State}
+    end.
+
+-spec convert_new_type(type_ref(), full_type_ref(), type_repr(), state(),
+		       stack()) -> rich_result2(ret_type(),state()).
+convert_new_type(_TypeRef, {_Mod,type,_Name,[]},
+		 {cached,FinType,_TypeForm,_SymbInfo}, State, _Stack) ->
+    {ok, {simple,FinType}, State};
+convert_new_type(TypeRef, {Mod,type,_Name,Args} = FullTypeRef,
+		 {abs_type,TypeForm,Vars,SymbInfo}, State, Stack) ->
+    VarDict = dict:from_list(lists:zip(Vars, Args)),
+    case convert(Mod, TypeForm, State, [FullTypeRef | Stack], VarDict) of
+	{ok, {simple,ImmFinType}, NewState} ->
+	    FinType = case SymbInfo of
+			  not_symb ->
+			      ImmFinType;
+			  {orig_abs,_OrigAbsType} ->
+			      proper_symb:internal_well_defined(ImmFinType)
+		      end,
+	    FinalState = case Vars of
+			     [] -> cache_type(Mod, TypeRef, FinType, TypeForm,
+					      SymbInfo, NewState);
+			     _  -> NewState
+			 end,
+	    {ok, {simple,FinType}, FinalState};
+	{ok, {rec,RecFun,RecArgs}, NewState} ->
+	    convert_maybe_rec(FullTypeRef, SymbInfo, RecFun, RecArgs, NewState,
+			      Stack);
+	{error,_Reason} = Error ->
+	    Error
+    end;
+convert_new_type(_TypeRef, {Mod,record,Name,SubstsDict} = FullTypeRef,
+		 {abs_record,OrigFields}, State, Stack) ->
+    Fields = [case dict:find(FieldName, SubstsDict) of
+		  {ok,NewFieldType} -> NewFieldType;
+		  error             -> OrigFieldType
+	      end
+	      || {FieldName,OrigFieldType} <- OrigFields],
+    case convert_tuple(Mod, [{atom,0,Name} | Fields], false, State,
+		       [FullTypeRef | Stack], dict:new()) of
+	{ok, {simple,_FinType}, _NewState} = Result ->
+	    Result;
+	{ok, {rec,RecFun,RecArgs}, NewState} ->
+	    convert_maybe_rec(FullTypeRef, not_symb, RecFun, RecArgs, NewState,
+			      Stack);
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec cache_type(mod_name(), type_ref(), fin_type(), abs_type(), symb_info(),
+		 state()) -> state().
+cache_type(Mod, TypeRef, FinType, TypeForm, SymbInfo,
+	   #state{types = Types} = State) ->
+    TypeRepr = {cached,FinType,TypeForm,SymbInfo},
+    ModTypes = dict:fetch(Mod, Types),
+    NewModTypes = dict:store(TypeRef, TypeRepr, ModTypes),
+    NewTypes = dict:store(Mod, NewModTypes, Types),
+    State#state{types = NewTypes}.
+
+-spec convert_maybe_rec(full_type_ref(), symb_info(), rec_fun(), rec_args(),
+			state(), stack()) -> rich_result2(ret_type(),state()).
+convert_maybe_rec(FullTypeRef, SymbInfo, RecFun, RecArgs, State, Stack) ->
+    case at_toplevel(RecArgs, Stack) of
+	true  -> base_case_error(Stack);
+	false -> safe_convert_maybe_rec(FullTypeRef, SymbInfo, RecFun, RecArgs,
+					State)
+    end.
+
+-spec safe_convert_maybe_rec(full_type_ref(),symb_info(),rec_fun(),rec_args(),
+			     state()) -> rich_result2(ret_type(),state()).
+safe_convert_maybe_rec(FullTypeRef, SymbInfo, RecFun, RecArgs, State) ->
+    case partition_rec_args(FullTypeRef, RecArgs, false) of
+	{[],[],_,_} ->
+	    {ok, {rec,RecFun,RecArgs}, State};
+	{MyRecArgs,MyPos,OtherRecArgs,_OtherPos} ->
+	    case lists:all(fun({B,_T}) -> B =:= false end, MyRecArgs) of
+		true  -> convert_rec_type(SymbInfo, RecFun, MyPos, OtherRecArgs,
+					  State);
+		false -> {error, {internal,true_rec_arg_reached_type}}
+	    end
+    end.
+
+-spec convert_rec_type(symb_info(), rec_fun(), [position()], rec_args(),
+		       state()) -> {ok, ret_type(), state()}.
+convert_rec_type(SymbInfo, RecFun, MyPos, [], State) ->
+    NumRecArgs = length(MyPos),
+    M = fun(GenFun) ->
+	    fun(Size) ->
+		GenFuns = lists:duplicate(NumRecArgs, GenFun),
+		RecFun(GenFuns, erlang:max(0,Size - 1))
+	    end
+	end,
+    SizedGen = y(M),
+    ImmFinType = ?SIZED(Size,SizedGen(Size + 1)),
+    FinType = case SymbInfo of
+		  not_symb ->
+		      ImmFinType;
+		  {orig_abs,_OrigAbsType} ->
+		      proper_symb:internal_well_defined(ImmFinType)
+	      end,
+    {ok, {simple,FinType}, State};
+convert_rec_type(_SymbInfo, RecFun, MyPos, OtherRecArgs, State) ->
+    NumRecArgs = length(MyPos),
+    NewRecFun =
+	fun(OtherGens,TopSize) ->
+	    M = fun(GenFun) ->
+		    fun(Size) ->
+			GenFuns = lists:duplicate(NumRecArgs, GenFun),
+			AllGens =
+			    proper_arith:insert(GenFuns, MyPos, OtherGens),
+			RecFun(AllGens, erlang:max(0,Size - 1))
+		    end
+		end,
+	    (y(M))(TopSize)
+	end,
+    NewRecArgs = clean_rec_args(OtherRecArgs),
+    {ok, {rec,NewRecFun,NewRecArgs}, State}.
+
+%% Y Combinator: Read more at http://bc.tech.coop/blog/070611.html.
+-spec y(fun((fun((T) -> S))  ->  fun((T) -> S))) -> fun((T) -> S).
+y(M) ->
+    G = fun(F) ->
+	    M(fun(A) -> (F(F))(A) end)
+	end,
+    G(G).
+
+-spec process_list(mod_name(), [abs_type() | ret_type()], state(), stack(),
+		   var_dict()) -> rich_result2([ret_type()],state()).
+process_list(Mod, RawTypes, State, Stack, VarDict) ->
+    Process = fun({simple,_FinType} = Type, {ok,Types,State1}) ->
+		     {ok, [Type|Types], State1};
+		 ({rec,_RecFun,_RecArgs} = Type, {ok,Types,State1}) ->
+		     {ok, [Type|Types], State1};
+		 (TypeForm, {ok,Types,State1}) ->
+		     case convert(Mod, TypeForm, State1, Stack, VarDict) of
+			 {ok,Type,State2} -> {ok,[Type|Types],State2};
+			 {error,_} = Err  -> Err
+		     end;
+		 (_RawType, {error,_} = Err) ->
+		     Err
+	      end,
+    case lists:foldl(Process, {ok,[],State}, RawTypes) of
+	{ok,RevTypes,NewState} ->
+	    {ok, lists:reverse(RevTypes), NewState};
+	{error,_Reason} = Error ->
+	    Error
+    end.
+
+-spec convert_integer(abs_expr(), state()) -> rich_result2(ret_type(),state()).
+convert_integer(Expr, State) ->
+    case eval_int(Expr) of
+	{ok,Int} -> {ok, {simple,proper_types:exactly(Int)}, State};
+	error    -> expr_error(invalid_int_const, Expr)
+    end.
+
+-spec eval_int(abs_expr()) -> tagged_result(integer()).
+eval_int(Expr) ->
+    NoBindings = erl_eval:new_bindings(),
+    try erl_eval:expr(Expr, NoBindings) of
+	{value,Value,_NewBindings} when is_integer(Value) ->
+	    {ok, Value};
+	_ ->
+	    error
+    catch
+	error:_ ->
+	    error
+    end.
+
+-spec expr_error(atom(), abs_expr()) -> {'error',term()}.
+expr_error(Reason, Expr) ->
+    {error, {Reason,lists:flatten(erl_pp:expr(Expr))}}.
+
+-spec expr_error(atom(), abs_expr(), abs_expr()) -> {'error',term()}.
+expr_error(Reason, Expr1, Expr2) ->
+    Str1 = lists:flatten(erl_pp:expr(Expr1)),
+    Str2 = lists:flatten(erl_pp:expr(Expr2)),
+    {error, {Reason,Str1,Str2}}.
+
+-spec base_case_error(stack()) -> {'error',term()}.
+%% TODO: This might confuse, since it doesn't record the arguments to parametric
+%%	 types or the type subsitutions of a record.
+base_case_error([{Mod,type,Name,Args} | _Upper]) ->
+    Arity = length(Args),
+    {error, {no_base_case,{Mod,type,Name,Arity}}};
+base_case_error([{Mod,record,Name,_SubstsDict} | _Upper]) ->
+    {error, {no_base_case,{Mod,record,Name}}}.
+
+
+%%------------------------------------------------------------------------------
+%% Helper datatypes handling functions
+%%------------------------------------------------------------------------------
+
+-spec stack_position(full_type_ref(), stack()) -> 'none' | pos_integer().
+stack_position(FullTypeRef, Stack) ->
+    SameType = fun(A) -> same_full_type_ref(A,FullTypeRef) end,
+    case proper_arith:find_first(SameType, Stack) of
+	{Pos,_} -> Pos;
+	none    -> none
+    end.
+
+-spec partition_by_toplevel(rec_args(), stack(), boolean()) ->
+	  {rec_args(),[position()],rec_args(),[position()]}.
+partition_by_toplevel(RecArgs, [], _OnlyInstanceAccepting) ->
+    {[],[],RecArgs,lists:seq(1,length(RecArgs))};
+partition_by_toplevel(RecArgs, [_Parent | _Upper], _OnlyInstanceAccepting)
+	when is_atom(_Parent) ->
+    {[],[],RecArgs,lists:seq(1,length(RecArgs))};
+partition_by_toplevel(RecArgs, [Parent | _Upper], OnlyInstanceAccepting) ->
+    partition_rec_args(Parent, RecArgs, OnlyInstanceAccepting).
+
+-spec at_toplevel(rec_args(), stack()) -> boolean().
+at_toplevel(RecArgs, Stack) ->
+    case partition_by_toplevel(RecArgs, Stack, false) of
+	{[],[],_,_} -> false;
+	_           -> true
+    end.
+
+-spec partition_rec_args(full_type_ref(), rec_args(), boolean()) ->
+	  {rec_args(),[position()],rec_args(),[position()]}.
+partition_rec_args(FullTypeRef, RecArgs, OnlyInstanceAccepting) ->
+    SameType =
+	case OnlyInstanceAccepting of
+	    true  -> fun({false,_T}) -> false
+		      ; ({_B,T})     -> same_full_type_ref(T,FullTypeRef) end;
+	    false -> fun({_B,T}) -> same_full_type_ref(T,FullTypeRef) end
+	end,
+    proper_arith:partition(SameType, RecArgs).
+
+%% Tuples can be of 0 arity, unions of 1 and wunions at least of 2.
+-spec combine_ret_types([ret_type()], {'tuple',boolean()} | 'union'
+				      | 'wunion') -> ret_type().
+combine_ret_types(RetTypes, EnclosingType) ->
+    case lists:all(fun is_simple_ret_type/1, RetTypes) of
+	true ->
+	    %% This should never happen for wunion.
+	    Combine = case EnclosingType of
+			  {tuple,false} -> fun proper_types:tuple/1;
+			  {tuple,true}  -> fun proper_types:fixed_list/1;
+			  union         -> fun proper_types:union/1
+		      end,
+	    FinTypes = [T || {simple,T} <- RetTypes],
+	    {simple, Combine(FinTypes)};
+	false ->
+	    NumTypes = length(RetTypes),
+	    {RevRecFuns,RevRecArgsList,NumRecs} =
+		lists:foldl(fun add_ret_type/2, {[],[],0}, RetTypes),
+	    RecFuns = lists:reverse(RevRecFuns),
+	    RecArgsList = lists:reverse(RevRecArgsList),
+	    RecArgLens = [length(RecArgs) || RecArgs <- RecArgsList],
+	    RecFunInfo = {NumTypes,NumRecs,RecArgLens,RecFuns},
+	    FlatRecArgs = lists:flatten(RecArgsList),
+	    {NewRecFun,NewRecArgs} =
+		case EnclosingType of
+		    {tuple,ToList} ->
+			{tuple_rec_fun(RecFunInfo,ToList),
+			 soft_clean_rec_args(FlatRecArgs,RecFunInfo,ToList)};
+		    union ->
+			{union_rec_fun(RecFunInfo),clean_rec_args(FlatRecArgs)};
+		    wunion ->
+			{wunion_rec_fun(RecFunInfo),
+			 clean_rec_args(FlatRecArgs)}
+		end,
+	    {rec, NewRecFun, NewRecArgs}
+    end.
+
+-spec tuple_rec_fun(rec_fun_info(), boolean()) -> rec_fun().
+tuple_rec_fun({_NumTypes,NumRecs,RecArgLens,RecFuns}, ToList) ->
+    Combine = case ToList of
+		  true  -> fun proper_types:fixed_list/1;
+		  false -> fun proper_types:tuple/1
+	      end,
+    fun(AllGFs,TopSize) ->
+	Size = TopSize div NumRecs,
+	GFsList = proper_arith:unflatten(AllGFs, RecArgLens),
+	ArgsList = [[GenFuns,Size] || GenFuns <- GFsList],
+	ZipFun = fun erlang:apply/2,
+	Combine(lists:zipwith(ZipFun, RecFuns, ArgsList))
+    end.
+
+-spec union_rec_fun(rec_fun_info()) -> rec_fun().
+union_rec_fun({_NumTypes,_NumRecs,RecArgLens,RecFuns}) ->
+    fun(AllGFs,Size) ->
+	GFsList = proper_arith:unflatten(AllGFs, RecArgLens),
+	ArgsList = [[GenFuns,Size] || GenFuns <- GFsList],
+	ZipFun = fun(F,A) -> ?LAZY(apply(F,A)) end,
+	proper_types:union(lists:zipwith(ZipFun, RecFuns, ArgsList))
+    end.
+
+-spec wunion_rec_fun(rec_fun_info()) -> rec_fun().
+wunion_rec_fun({NumTypes,_NumRecs,RecArgLens,RecFuns}) ->
+    fun(AllGFs,Size) ->
+	GFsList = proper_arith:unflatten(AllGFs, RecArgLens),
+	ArgsList = [[GenFuns,Size] || GenFuns <- GFsList],
+	ZipFun = fun(W,F,A) -> {W,?LAZY(apply(F,A))} end,
+	RecWeight = erlang:max(1, Size div (NumTypes - 1)),
+	Weights = [1 | lists:duplicate(NumTypes - 1, RecWeight)],
+	WeightedChoices = lists:zipwith3(ZipFun, Weights, RecFuns, ArgsList),
+	proper_types:wunion(WeightedChoices)
+    end.
+
+-spec add_ret_type(ret_type(), {[rec_fun()],[rec_args()],non_neg_integer()}) ->
+	  {[rec_fun()],[rec_args()],non_neg_integer()}.
+add_ret_type({simple,FinType}, {RecFuns,RecArgsList,NumRecs}) ->
+    {[fun([],_) -> FinType end | RecFuns], [[] | RecArgsList], NumRecs};
+add_ret_type({rec,RecFun,RecArgs}, {RecFuns,RecArgsList,NumRecs}) ->
+    {[RecFun | RecFuns], [RecArgs | RecArgsList], NumRecs + 1}.
+
+-spec is_simple_ret_type(ret_type()) -> boolean().
+is_simple_ret_type({simple,_FinType}) ->
+    true;
+is_simple_ret_type({rec,_RecFun,_RecArgs}) ->
+    false.
+
+-spec clean_rec_args(rec_args()) -> rec_args().
+clean_rec_args(RecArgs) ->
+    [{false,F} || {_B,F} <- RecArgs].
+
+-spec soft_clean_rec_args(rec_args(), rec_fun_info(), boolean()) -> rec_args().
+soft_clean_rec_args(RecArgs, RecFunInfo, ToList) ->
+    soft_clean_rec_args_tr(RecArgs, [], RecFunInfo, ToList, false, 1).
+
+-spec soft_clean_rec_args_tr(rec_args(), rec_args(), rec_fun_info(), boolean(),
+			     boolean(), position()) -> rec_args().
+soft_clean_rec_args_tr([], Acc, _RecFunInfo, _ToList, _FoundListInst, _Pos) ->
+    lists:reverse(Acc);
+soft_clean_rec_args_tr([{{list,_NonEmpty,_AltRecFun},FTRef} | Rest], Acc,
+		       RecFunInfo, ToList, true, Pos) ->
+    NewArg = {false,FTRef},
+    soft_clean_rec_args_tr(Rest, [NewArg|Acc], RecFunInfo, ToList, true, Pos+1);
+soft_clean_rec_args_tr([{{list,NonEmpty,AltRecFun},FTRef} | Rest], Acc,
+		       RecFunInfo, ToList, false, Pos) ->
+    {NumTypes,NumRecs,RecArgLens,RecFuns} = RecFunInfo,
+    AltRecFunPos = get_group(Pos, RecArgLens),
+    AltRecFuns = proper_arith:list_update(AltRecFunPos, AltRecFun, RecFuns),
+    AltRecFunInfo = {NumTypes,NumRecs,RecArgLens,AltRecFuns},
+    NewArg = {{list,NonEmpty,tuple_rec_fun(AltRecFunInfo,ToList)},FTRef},
+    soft_clean_rec_args_tr(Rest, [NewArg|Acc], RecFunInfo, ToList, true, Pos+1);
+soft_clean_rec_args_tr([Arg | Rest], Acc, RecFunInfo, ToList, FoundListInst,
+		       Pos) ->
+    soft_clean_rec_args_tr(Rest, [Arg | Acc], RecFunInfo, ToList, FoundListInst,
+			   Pos+1).
+
+-spec get_group(pos_integer(), [non_neg_integer()]) -> pos_integer().
+get_group(Pos, AllMembers) ->
+    get_group_tr(Pos, AllMembers, 1).
+
+-spec get_group_tr(pos_integer(), [non_neg_integer()], pos_integer()) ->
+	  pos_integer().
+get_group_tr(Pos, [Members | Rest], GroupNum) ->
+    case Pos =< Members of
+	true  -> GroupNum;
+	false -> get_group_tr(Pos - Members, Rest, GroupNum + 1)
+    end.
+
+-spec same_full_type_ref(full_type_ref(), term()) -> boolean().
+same_full_type_ref({SameMod,type,SameName,Args1},
+		   {SameMod,type,SameName,Args2}) ->
+    length(Args1) =:= length(Args2)
+    andalso lists:all(fun({A,B}) -> same_ret_type(A,B) end,
+		      lists:zip(Args1, Args2));
+same_full_type_ref({SameMod,record,SameName,SubstsDict1},
+		   {SameMod,record,SameName,SubstsDict2}) ->
+    same_substs_dict(SubstsDict1, SubstsDict2);
+same_full_type_ref(_, _) ->
+    false.
+
+-spec same_ret_type(ret_type(), ret_type()) -> boolean().
+same_ret_type({simple,FinType1}, {simple,FinType2}) ->
+    same_fin_type(FinType1, FinType2);
+same_ret_type({rec,RecFun1,RecArgs1}, {rec,RecFun2,RecArgs2}) ->
+    NumRecArgs = length(RecArgs1),
+    length(RecArgs2) =:= NumRecArgs
+    andalso lists:all(fun({A1,A2}) -> same_rec_arg(A1,A2,NumRecArgs) end,
+		      lists:zip(RecArgs1,RecArgs2))
+    andalso same_rec_fun(RecFun1, RecFun2, NumRecArgs);
+same_ret_type(_, _) ->
+    false.
+
+%% TODO: Is this too strict?
+-spec same_rec_arg(rec_arg(), rec_arg(), arity()) -> boolean().
+same_rec_arg({{list,SameBool,AltRecFun1},FTRef1},
+	     {{list,SameBool,AltRecFun2},FTRef2}, NumRecArgs) ->
+    same_rec_fun(AltRecFun1, AltRecFun2, NumRecArgs)
+    andalso same_full_type_ref(FTRef1, FTRef2);
+same_rec_arg({true,FTRef1}, {true,FTRef2}, _NumRecArgs) ->
+    same_full_type_ref(FTRef1, FTRef2);
+same_rec_arg({false,FTRef1}, {false,FTRef2}, _NumRecArgs) ->
+    same_full_type_ref(FTRef1, FTRef2);
+same_rec_arg(_, _, _NumRecArgs) ->
+    false.
+
+-spec same_substs_dict(substs_dict(), substs_dict()) -> boolean().
+same_substs_dict(SubstsDict1, SubstsDict2) ->
+    SameKVPair = fun({{_K,V1},{_K,V2}}) -> same_ret_type(V1,V2);
+		    (_)                 -> false
+		 end,
+    SubstsKVList1 = lists:sort(dict:to_list(SubstsDict1)),
+    SubstsKVList2 = lists:sort(dict:to_list(SubstsDict2)),
+    length(SubstsKVList1) =:= length(SubstsKVList2)
+    andalso lists:all(SameKVPair, lists:zip(SubstsKVList1,SubstsKVList2)).
+
+-spec same_fin_type(fin_type(), fin_type()) -> boolean().
+same_fin_type(Type1, Type2) ->
+    proper_types:equal_types(Type1, Type2).
+
+-spec same_rec_fun(rec_fun(), rec_fun(), arity()) -> boolean().
+same_rec_fun(RecFun1, RecFun2, NumRecArgs) ->
+    %% It's ok that we return a type, even if there's a 'true' for use of
+    %% an instance.
+    GenFun = fun(_Size) -> proper_types:exactly('$dummy') end,
+    GenFuns = lists:duplicate(NumRecArgs,GenFun),
+    same_fin_type(RecFun1(GenFuns,0), RecFun2(GenFuns,0)).