dialyzer: Fix a bug in the expansion of forms

The check that a modified type of a field is a subtype of the declared
type has been moved outside of the expansion of forms to avoid loops.

4 files changed, 849 insertions, 1 deletions

diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl
new file mode 100644
index 0000000000..07243f8d23
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_macros.hrl
@@ -0,0 +1,215 @@
+%% -*- erlang-indent-level: 2 -*-
+%%------------------------------------------------------------------------------
+
+%%====================================================================
+%% Types
+%%====================================================================
+
+%% Code and Monitor servers' info.
+-record(svs, {
+  code    :: pid(),
+  monitor :: pid()
+}).
+
+%% Tags of an AST's node.
+-record(tags, {
+  this = undefined :: cuter_cerl:tag() | undefined,
+  next = undefined :: cuter_cerl:tag() | undefined
+}).
+
+-type loaded_ret_atoms() :: cover_compiled | preloaded | non_existing.
+-type servers() :: #svs{}.
+-type ast_tags() :: #tags{}.
+
+%%====================================================================
+%% Directories
+%%====================================================================
+
+-define(RELATIVE_TMP_DIR, "temp").
+-define(PYTHON_CALL, ?PYTHON_PATH ++ " -u " ++ ?PRIV ++ "/cuter_interface.py").
+
+%%====================================================================
+%% Prefixes
+%%====================================================================
+
+-define(DEPTH_PREFIX, '__conc_depth').
+-define(EXECUTION_PREFIX, '__conc_prefix').
+-define(SYMBOLIC_PREFIX, '__s').
+-define(CONCOLIC_PREFIX_MSG, '__concm').
+-define(ZIPPED_VALUE_PREFIX, '__czip').
+-define(CONCOLIC_PREFIX_PDICT, '__concp').
+-define(FUNCTION_PREFIX, '__cfunc').
+-define(UNBOUND_VAR_PREFIX, '__uboundvar').
+-define(BRANCH_TAG_PREFIX, '__branch_tag').
+-define(VISITED_TAGS_PREFIX, '__visited_tags').
+-define(EXECUTION_COUNTER_PREFIX, '__exec_counter').
+
+%%====================================================================
+%% Flags & Default Values
+%%====================================================================
+
+-define(LOGGING_FLAG, ok).
+-define(DELETE_TRACE, ok).
+-define(LOG_UNSUPPORTED_MFAS, ok).
+%%-define(VERBOSE_SCHEDULER, ok).
+%%-define(VERBOSE_FILE_DELETION, ok).
+%%-define(VERBOSE_SOLVING, ok).
+%%-define(VERBOSE_MERGING, ok).
+%%-define(VERBOSE_REPORTING, ok).
+-define(USE_SPECS, ok).
+
+%%====================================================================
+%% Solver Responses
+%%====================================================================
+
+-define(RSP_MODEL_DELIMITER_START, <<"model_start">>).
+-define(RSP_MODEL_DELIMITER_END, <<"model_end">>).
+
+%%====================================================================
+%% OpCodes for types in JSON objects
+%%====================================================================
+
+-define(JSON_TYPE_ANY, 0).
+-define(JSON_TYPE_INT, 1).
+-define(JSON_TYPE_FLOAT, 2).
+-define(JSON_TYPE_ATOM, 3).
+-define(JSON_TYPE_LIST, 4).
+-define(JSON_TYPE_TUPLE, 5).
+-define(JSON_TYPE_PID, 6).
+-define(JSON_TYPE_REF, 7).
+
+%%====================================================================
+%% OpCodes for the commands to the solver
+%%====================================================================
+
+-define(JSON_CMD_LOAD_TRACE_FILE, 1).
+-define(JSON_CMD_SOLVE, 2).
+-define(JSON_CMD_GET_MODEL, 3).
+-define(JSON_CMD_ADD_AXIOMS, 4).
+-define(JSON_CMD_FIX_VARIABLE, 5).
+-define(JSON_CMD_RESET_SOLVER, 6).
+-define(JSON_CMD_STOP, 42).
+
+%%====================================================================
+%% OpCodes for constraint types
+%%====================================================================
+
+-define(CONSTRAINT_TRUE, 1).
+-define(CONSTRAINT_FALSE, 2).
+-define(NOT_CONSTRAINT, 3).
+
+-define(CONSTRAINT_TRUE_REPR, 84).   %% $T
+-define(CONSTRAINT_FALSE_REPR, 70).  %% $F
+
+%%====================================================================
+%% OpCodes of constraints & built-in operations
+%%====================================================================
+
+%% Empty tag ID
+-define(EMPTY_TAG_ID, 0).
+
+%% MFA's Parameters & Spec definitions.
+-define(OP_PARAMS, 1).
+-define(OP_SPEC, 2).
+%% Constraints.
+-define(OP_GUARD_TRUE, 3).
+-define(OP_GUARD_FALSE, 4).
+-define(OP_MATCH_EQUAL_TRUE, 5).
+-define(OP_MATCH_EQUAL_FALSE, 6).
+-define(OP_TUPLE_SZ, 7).
+-define(OP_TUPLE_NOT_SZ, 8).
+-define(OP_TUPLE_NOT_TPL, 9).
+-define(OP_LIST_NON_EMPTY, 10).
+-define(OP_LIST_EMPTY, 11).
+-define(OP_LIST_NOT_LST, 12).
+%% Information used for syncing & merging the traces of many processes.
+-define(OP_SPAWN, 13).
+-define(OP_SPAWNED, 14).
+-define(OP_MSG_SEND, 15).
+-define(OP_MSG_RECEIVE, 16).
+-define(OP_MSG_CONSUME, 17).
+%% Necessary operations for the evaluation of Core Erlang.
+-define(OP_UNFOLD_TUPLE, 18).
+-define(OP_UNFOLD_LIST, 19).
+%% Bogus operation (operations interpreted as the identity function).
+-define(OP_BOGUS, 48).
+%% Type conversions.
+-define(OP_FLOAT, 47).
+-define(OP_LIST_TO_TUPLE, 52).
+-define(OP_TUPLE_TO_LIST, 53).
+%% Query types.
+-define(OP_IS_INTEGER, 27).
+-define(OP_IS_ATOM, 28).
+-define(OP_IS_FLOAT, 29).
+-define(OP_IS_LIST, 30).
+-define(OP_IS_TUPLE, 31).
+-define(OP_IS_BOOLEAN, 32).
+-define(OP_IS_NUMBER, 33).
+%% Arithmetic operations.
+-define(OP_PLUS, 34).
+-define(OP_MINUS, 35).
+-define(OP_TIMES, 36).
+-define(OP_RDIV, 37).
+-define(OP_IDIV_NAT, 38).
+-define(OP_REM_NAT, 39).
+-define(OP_UNARY, 40).
+%% Operations on atoms.
+-define(OP_ATOM_NIL, 49).
+-define(OP_ATOM_HEAD, 50).
+-define(OP_ATOM_TAIL, 51).
+%% Operations on lists.
+-define(OP_HD, 25).
+-define(OP_TL, 26).
+-define(OP_CONS, 56).
+%% Operations on tuples.
+-define(OP_TCONS, 57).
+%% Comparisons.
+-define(OP_EQUAL, 41).
+-define(OP_UNEQUAL, 42).
+-define(OP_LT_INT, 54).
+-define(OP_LT_FLOAT, 55).
+
+%% Maps MFAs to their JSON Opcodes
+-define(OPCODE_MAPPING,
+  dict:from_list([ %% Simulated built-in operations
+                   { {cuter_erlang, atom_to_list_bogus, 1}, ?OP_BOGUS         }
+                 , { {cuter_erlang, is_atom_nil,        1}, ?OP_ATOM_NIL      }
+                 , { {cuter_erlang, safe_atom_head,     1}, ?OP_ATOM_HEAD     }
+                 , { {cuter_erlang, safe_atom_tail,     1}, ?OP_ATOM_TAIL     }
+                 , { {cuter_erlang, safe_pos_div,       2}, ?OP_IDIV_NAT      }
+                 , { {cuter_erlang, safe_pos_rem,       2}, ?OP_REM_NAT       }
+                 , { {cuter_erlang, lt_int,             2}, ?OP_LT_INT        }
+                 , { {cuter_erlang, lt_float,           2}, ?OP_LT_FLOAT      }
+                 , { {cuter_erlang, safe_plus,          2}, ?OP_PLUS          }
+                 , { {cuter_erlang, safe_minus,         2}, ?OP_MINUS         }
+                 , { {cuter_erlang, safe_times,         2}, ?OP_TIMES         }
+                 , { {cuter_erlang, safe_rdiv,          2}, ?OP_RDIV          }
+                 , { {cuter_erlang, safe_float,         1}, ?OP_FLOAT         }
+                 , { {cuter_erlang, safe_list_to_tuple, 1}, ?OP_LIST_TO_TUPLE }
+                 , { {cuter_erlang, safe_tuple_to_list, 1}, ?OP_TUPLE_TO_LIST }
+                 , { {bogus_erlang, cons,               2}, ?OP_CONS          }
+                   %% Actual erlang BIFs
+                 , { {erlang, hd,            1}, ?OP_HD            }
+                 , { {erlang, tl,            1}, ?OP_TL            }
+                 , { {erlang, is_integer,    1}, ?OP_IS_INTEGER    }
+                 , { {erlang, is_atom,       1}, ?OP_IS_ATOM       }
+                 , { {erlang, is_boolean,    1}, ?OP_IS_BOOLEAN    }
+                 , { {erlang, is_float,      1}, ?OP_IS_FLOAT      }
+                 , { {erlang, is_list,       1}, ?OP_IS_LIST       }
+                 , { {erlang, is_tuple,      1}, ?OP_IS_TUPLE      }
+                 , { {erlang, is_number,     1}, ?OP_IS_NUMBER     }
+                 , { {erlang, '-',           1}, ?OP_UNARY         }
+                 , { {erlang, '=:=',         2}, ?OP_EQUAL         }
+                 , { {erlang, '=/=',         2}, ?OP_UNEQUAL       }
+                 ])).
+
+%% All the MFAs that are supported for symbolic evaluation.
+-define(SUPPORTED_MFAS, gb_sets:from_list(dict:fetch_keys(?OPCODE_MAPPING))).
+
+-define(UNSUPPORTED_MFAS,
+  gb_sets:from_list([ {cuter_erlang, unsupported_lt, 2} ])).
+
+%% The set of all the built-in operations that the solver can try to reverse.
+-define (REVERSIBLE_OPERATIONS,
+  gb_sets:from_list([ ?OP_HD, ?OP_TL
+                    ])).
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.erl b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.erl
new file mode 100644
index 0000000000..e9561374cc
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.erl
@@ -0,0 +1,607 @@
+%% -*- erlang-indent-level: 2 -*-
+%%------------------------------------------------------------------------------
+-module(cuter_types).
+
+-export([parse_spec/3, retrieve_types/1, retrieve_specs/1, find_spec/2, get_kind/1]).
+
+-export([params_of_t_function_det/1, ret_of_t_function_det/1, atom_of_t_atom_lit/1, integer_of_t_integer_lit/1,
+         elements_type_of_t_list/1, elements_type_of_t_nonempty_list/1, elements_types_of_t_tuple/1,
+         elements_types_of_t_union/1, bounds_of_t_range/1, segment_size_of_bitstring/1]).
+
+-export_type([erl_type/0, erl_spec_clause/0, erl_spec/0, stored_specs/0, stored_types/0, stored_spec_value/0, t_range_limit/0]).
+
+-include("cuter_macros.hrl").
+-include("cuter_types.hrl").
+
+
+%% Define tags
+-define(type_variable, vart).
+-define(type_var, tvar).
+-define(max_char, 16#10ffff).
+
+%% Pre-processed types.
+
+-type type_name() :: atom().
+-type type_arity() :: byte().
+-type type_var() :: {?type_var, atom()}.
+-type remote_type() :: {module(), type_name(), type_arity()}.
+-type record_name() :: atom().
+-type record_field_name() :: atom().
+-type record_field_type() :: {record_field_name(), raw_type()}.
+-type dep() :: remote_type().
+-type deps() :: ordsets:ordset(remote_type()).
+-record(t, {
+  kind,
+  rep,
+  deps = ordsets:new() :: deps()
+}).
+-type erl_type() :: t_any()               % any()
+                  | t_nil()               % []
+                  | t_atom()              % atom()
+                  | t_atom_lit()          % Erlang_Atom
+                  | t_integer()           % integer(), +infinity, -inifinity
+                  | t_integer_lit()       % Erlang_Integer
+                  | t_float()             % float()
+                  | t_tuple()             % tuple(), {TList}
+                  | t_list()              % list(Type)
+                  | t_nonempty_list()     % nonempty_list(Type)
+                  | t_union()             % Type1 | ... | TypeN
+                  | t_range()             % Erlang_Integer..Erlang_Integer
+                  | t_bitstring()         % <<_:M>>
+                  | t_function()          % function() | Fun | BoundedFun
+                  .
+-type raw_type() :: erl_type()
+                  | t_local()             % Local Type Usage
+                  | t_remote()            % Remote Type Usage
+                  | t_record()            % Record Usage
+                  | t_type_var()          % Type Variable
+                  .
+
+-type t_any() :: #t{kind :: ?any_tag}.
+-type t_nil() :: #t{kind :: ?nil_tag}.
+-type t_atom() :: #t{kind :: ?atom_tag}.
+-type t_atom_lit() :: #t{kind :: ?atom_lit_tag, rep :: atom()}.
+-type t_integer() :: #t{kind :: ?integer_tag}.
+-type t_integer_lit() :: #t{kind :: ?integer_lit_tag, rep :: integer()}.
+-type t_float() :: #t{kind :: ?float_tag}.
+-type t_tuple() :: #t{kind :: ?tuple_tag, rep :: [raw_type()]}.
+-type t_list() :: #t{kind :: ?list_tag, rep :: raw_type()}.
+-type t_nonempty_list() :: #t{kind :: ?nonempty_list_tag, rep :: raw_type()}.
+-type t_union() :: #t{kind :: ?union_tag, rep :: [raw_type()]}.
+-type t_range() :: #t{kind :: ?range_tag, rep :: {t_range_limit(), t_range_limit()}}.
+-type t_range_limit() :: t_integer_lit() | t_integer_inf().
+-type t_integer_inf() :: t_integer_pos_inf() | t_integer_neg_inf().
+-type t_integer_pos_inf() :: #t{kind :: ?pos_inf}.
+-type t_integer_neg_inf() :: #t{kind :: ?neg_inf}.
+-type t_bitstring() :: #t{kind :: ?bitstring_tag, rep :: 1|8}.
+-type t_function() :: #t{kind :: ?function_tag} | t_function_det().
+-type t_function_det() :: #t{kind :: ?function_tag, rep :: {[raw_type()], raw_type(), [t_constraint()]}, deps :: deps()}.
+-type t_constraint() :: {t_type_var(), raw_type()}.
+-type t_local() :: #t{kind :: ?local_tag, rep :: {type_name(), [raw_type()]}}.
+-type t_remote() :: #t{kind :: ?remote_tag, rep :: {module(), type_name(), [raw_type()]}}.
+-type t_record() :: #t{kind :: ?record_tag, rep :: {record_name(), [record_field_type()]}}.
+-type t_type_var() :: #t{kind :: ?type_variable, rep :: type_var()}.
+
+%% How pre-processed types are stored.
+-type stored_type_key() :: {record, record_name()} | {type, type_name(), type_arity()}.
+-type stored_type_value() :: [record_field_type()] | {any(), [type_var()]}. % raw_type()
+-type stored_types() :: dict:dict(stored_type_key(), stored_type_value()).
+
+-type stored_spec_key() :: {type_name(), type_arity()}.
+-type stored_spec_value() :: [t_function_det()].
+-type stored_specs() :: dict:dict(stored_spec_key(), stored_spec_value()).
+
+-type type_var_env() :: dict:dict(type_var(), raw_type()).
+-type erl_spec_clause() :: t_function_det().
+-type erl_spec() :: [erl_spec_clause()].
+
+%% Pre-process the type & record declarations of a module.
+-spec retrieve_types([cuter_cerl:cerl_attr_type()]) -> stored_types().
+retrieve_types(TypeAttrs) ->
+  lists:foldl(fun process_type_attr/2, dict:new(), TypeAttrs).
+
+-spec process_type_attr(cuter_cerl:cerl_recdef() | cuter_cerl:cerl_typedef(), stored_types()) -> stored_types().
+%% Declaration of a record.
+process_type_attr({{record, Name}, Fields, []}, Processed) ->
+  Fs = [t_field_from_form(Field) || Field <- Fields],
+  Record = t_record(Name, Fs),
+  dict:store({record, Name}, Record, Processed);
+%% Declaration of a type.
+process_type_attr({Name, Repr, Vars}, Processed) ->
+  Type = safe_t_from_form(Repr),
+  Vs = [{?type_var, Var} || {var, _, Var} <- Vars],
+  dict:store({type, Name, length(Vs)}, {Type, Vs}, Processed).
+
+%% The fields of a declared record.
+-spec t_field_from_form(cuter_cerl:cerl_record_field()) -> record_field_type().
+t_field_from_form({record_field, _, {atom, _, Name}}) ->
+  {Name, t_any()};
+t_field_from_form({record_field, _, {atom, _, Name}, _Default}) ->
+  {Name, t_any()};
+t_field_from_form({typed_record_field, {record_field, _, {atom, _, Name}}, Type}) ->
+  {Name, safe_t_from_form(Type)};
+t_field_from_form({typed_record_field, {record_field, _, {atom, _, Name}, _Default}, Type}) ->
+  {Name, safe_t_from_form(Type)}.
+
+%% Provision for unsupported types.
+safe_t_from_form(Form) ->
+  try t_from_form(Form)
+  catch throw:{unsupported, Info} ->
+    cuter_pp:form_has_unsupported_type(Info),
+    t_any()
+  end.
+
+%% Parse a type.
+
+-spec t_from_form(cuter_cerl:cerl_type()) -> raw_type().
+%% Erlang_Atom
+t_from_form({atom, _, Atom}) ->
+  t_atom_lit(Atom);
+%% Erlang_Integer
+t_from_form({integer, _, Integer}) ->
+  t_integer_lit(Integer);
+%% integer()
+t_from_form({type, _, integer, []}) ->
+  t_integer();
+%% nil
+t_from_form({type, _, nil, []}) ->
+  t_nil();
+%% any()
+t_from_form({type, _, any, []}) ->
+  t_any();
+%% term()
+t_from_form({type, _, term, []}) ->
+  t_any();
+%% atom()
+t_from_form({type, _, atom, []}) ->
+  t_atom();
+%% module()
+t_from_form({type, _, module, []}) ->
+  t_module();
+%% float()
+t_from_form({type, _, float, []}) ->
+  t_float();
+%% tuple()
+t_from_form({type, _, tuple, any}) ->
+  t_tuple();
+%% {TList}
+t_from_form({type, _, tuple, Types}) ->
+  Ts = [t_from_form(T) || T <- Types],
+  t_tuple(Ts);
+%% list()
+t_from_form({type, _, list, []}) ->
+  t_list();
+%% list(Type)
+t_from_form({type, _, list, [Type]}) ->
+  T = t_from_form(Type),
+  t_list(T);
+%% Type1 | ... | TypeN
+t_from_form({type, _, union, Types}) ->
+  Ts = [t_from_form(T) || T <- Types],
+  t_union(Ts);
+%% boolean()
+t_from_form({type, _, boolean, []}) ->
+  t_union([t_atom_lit(true), t_atom_lit(false)]);
+%% number()
+t_from_form({type, _, number, []}) ->
+  t_union([t_integer(), t_float()]);
+%% Erlang_Integer..Erlang_Integer
+t_from_form({type, _, range, [{integer, _, I1}, {integer, _, I2}]}) ->
+  t_range(t_integer_lit(I1), t_integer_lit(I2));
+%% non_neg_integer()
+t_from_form({type, _, non_neg_integer, []}) ->
+  t_range(t_integer_lit(0), t_pos_inf());
+%% pos_integer()
+t_from_form({type, _, pos_integer, []}) ->
+  t_range(t_integer_lit(1), t_pos_inf());
+%% neg_integer()
+t_from_form({type, _, neg_integer, []}) ->
+  t_range(t_neg_inf(), t_integer_lit(-1));
+%% char()
+t_from_form({type, _, char, []}) ->
+  t_char();
+%% byte()
+t_from_form({type, _, byte, []}) ->
+  t_byte();
+%% mfa()
+t_from_form({type, _, mfa, []}) ->
+  t_tuple([t_module(), t_atom(), t_byte()]);
+%% string()
+t_from_form({type, _, string, []}) ->
+  t_list(t_char());
+%% nonempty_list()
+t_from_form({type, _, nonempty_list, []}) ->
+  t_nonempty_list();
+%% nonempty_list(Type)
+t_from_form({type, _, nonempty_list, [Type]}) ->
+  T = t_from_form(Type),
+  t_nonempty_list(T);
+%% binary()
+t_from_form({type, _, binary, []}) ->
+  t_bitstring(8);
+%% bitstring()
+t_from_form({type, _, bitstring, []}) ->
+  t_bitstring(1);
+%% function()
+t_from_form({type, _, function, []}) ->
+  t_function();
+%% fun((TList) -> Type)
+t_from_form({type, _, 'fun', [_Product, _RetType]}=Fun) ->
+  t_function_from_form(Fun);
+%% fun((TList) -> Type) (bounded_fun)
+t_from_form({type, _, 'bounded_fun', [_Fun, _Cs]}=BoundedFun) ->
+  t_bounded_function_from_form(BoundedFun);
+%% ann_type
+t_from_form({ann_type, _, [_Var, Type]}) ->
+  t_from_form(Type);
+%% paren_type
+t_from_form({paren_type, _, [Type]}) ->
+  t_from_form(Type);
+%% remote_type
+t_from_form({remote_type, _, [{atom, _, M}, {atom, _, Name}, Types]}) ->
+  Ts = [t_from_form(T) || T <- Types],
+  t_remote(M, Name, Ts);
+%% Record
+t_from_form({type, _, record, [{atom, _, Name} | FieldTypes]}) ->
+  Fields = [t_bound_field_from_form(F) || F <- FieldTypes],
+  t_record(Name, Fields);
+%% Map
+t_from_form({type, _, map, _}=X) ->
+  throw({unsupported, X});
+%% local type
+t_from_form({type, _, Name, Types}) ->
+  Ts = [t_from_form(T) || T <- Types],
+  t_local(Name, Ts);
+%% Type Variable
+t_from_form({var, _, Var}) ->
+  t_var(Var);
+%% Unsupported forms
+t_from_form(Type) ->
+  throw({unsupported, Type}).
+
+-spec t_bound_field_from_form(cuter_cerl:cerl_type_record_field()) -> record_field_type().
+%% Record Field.
+t_bound_field_from_form({type, _, field_type, [{atom, _, Name}, Type]}) ->
+  {Name, t_from_form(Type)}.
+
+-spec t_function_from_form(cuter_cerl:cerl_func()) -> t_function_det().
+t_function_from_form({type, _, 'fun', [{type, _, 'product', Types}, RetType]}) ->
+  Ret = t_from_form(RetType),
+  Ts = [t_from_form(T) || T <- Types],
+  t_function(Ts, Ret).
+
+-spec t_bounded_function_from_form(cuter_cerl:cerl_bounded_func()) -> t_function_det().
+t_bounded_function_from_form({type, _, 'bounded_fun', [Fun, Constraints]}) ->
+  {type, _, 'fun', [{type, _, 'product', Types}, RetType]} = Fun,
+  Ret = t_from_form(RetType),
+  Ts = [t_from_form(T) || T <- Types],
+  Cs = [t_constraint_from_form(C) || C <- Constraints],
+  t_function(Ts, Ret, Cs).
+
+-spec t_constraint_from_form(cuter_cerl:cerl_constraint()) -> t_constraint().
+t_constraint_from_form({type, _, constraint, [{atom, _, is_subtype}, [{var, _, Var}, Type]]}) ->
+  {t_var(Var), t_from_form(Type)}.
+
+
+%% Type constructors.
+
+-spec t_any() -> t_any().
+t_any() ->
+  #t{kind = ?any_tag}.
+
+-spec t_atom_lit(atom()) -> t_atom_lit().
+t_atom_lit(Atom) ->
+  #t{kind = ?atom_lit_tag, rep = Atom}.
+
+-spec t_atom() -> t_atom().
+t_atom() ->
+  #t{kind = ?atom_tag}.
+
+-spec t_module() -> t_atom().
+t_module() -> t_atom().
+
+-spec t_integer_lit(integer()) -> t_integer_lit().
+t_integer_lit(Integer) ->
+  #t{kind = ?integer_lit_tag, rep = Integer}.
+
+-spec t_integer() -> t_integer().
+t_integer() ->
+  #t{kind = ?integer_tag}.
+
+-spec t_range(t_range_limit(), t_range_limit()) -> t_range().
+t_range(Int1, Int2) ->
+  #t{kind = ?range_tag, rep = {Int1, Int2}}.
+
+-spec t_pos_inf() -> t_integer_pos_inf().
+t_pos_inf() ->
+  #t{kind = ?pos_inf}.
+
+-spec t_neg_inf() -> t_integer_neg_inf().
+t_neg_inf() ->
+  #t{kind = ?neg_inf}.
+
+-spec t_char() -> t_range().
+t_char() ->
+  t_range(t_integer_lit(0), t_integer_lit(?max_char)).
+
+-spec t_nil() -> t_nil().
+t_nil() ->
+  #t{kind = ?nil_tag}.
+
+-spec t_float() -> t_float().
+t_float() ->
+  #t{kind = ?float_tag}.
+
+-spec t_list() -> t_list().
+t_list() ->
+  #t{kind = ?list_tag, rep = t_any()}.
+
+-spec t_list(raw_type()) -> t_list().
+t_list(Type) ->
+  #t{kind = ?list_tag, rep = Type, deps = get_deps(Type)}.
+
+-spec t_nonempty_list() -> t_nonempty_list().
+t_nonempty_list() ->
+  #t{kind = ?nonempty_list_tag, rep = t_any()}.
+
+-spec t_nonempty_list(raw_type()) -> t_nonempty_list().
+t_nonempty_list(Type) ->
+  #t{kind = ?nonempty_list_tag, rep = Type, deps = get_deps(Type)}.
+
+-spec t_tuple() -> t_tuple().
+t_tuple() ->
+  #t{kind = ?tuple_tag, rep = []}.
+
+-spec t_tuple([raw_type()]) -> t_tuple().
+t_tuple(Types) ->
+  #t{kind = ?tuple_tag, rep = Types, deps = unify_deps(Types)}.
+
+-spec t_union([raw_type()]) -> t_union().
+t_union(Types) ->
+  #t{kind = ?union_tag, rep = Types, deps = unify_deps(Types)}.
+
+-spec t_byte() -> t_range().
+t_byte() ->
+  t_range(t_integer_lit(0), t_integer_lit(255)).
+
+-spec t_local(type_name(), [raw_type()]) -> t_local().
+t_local(Name, Types) ->
+  Rep = {Name, Types},
+  #t{kind = ?local_tag, rep = Rep, deps = unify_deps(Types)}.
+
+-spec t_remote(module(), type_name(), [raw_type()]) -> t_remote().
+t_remote(Mod, Name, Types) ->
+  Rep = {Mod, Name, Types},
+  Dep = {Mod, Name, length(Types)},
+  #t{kind = ?remote_tag, rep = Rep, deps = add_dep(Dep, unify_deps(Types))}.
+
+-spec t_var(atom()) -> t_type_var().
+t_var(Var) ->
+  #t{kind = ?type_variable, rep = {?type_var, Var}}.
+
+-spec t_record(record_name(), [record_field_type()]) -> t_record().
+t_record(Name, Fields) ->
+  Rep = {Name, Fields},
+  Ts = [T || {_, T} <- Fields],
+  #t{kind = ?record_tag, rep = Rep, deps = unify_deps(Ts)}.
+
+-spec fields_of_t_record(t_record()) -> [record_field_type()].
+fields_of_t_record(Record) ->
+  Rep = Record#t.rep,
+  element(2, Rep).
+
+-spec t_bitstring(1 | 8) -> t_bitstring().
+t_bitstring(N) ->
+  #t{kind = ?bitstring_tag, rep = N}.
+
+-spec t_function() -> t_function().
+t_function() ->
+  #t{kind = ?function_tag}.
+
+-spec t_function([raw_type()], raw_type()) -> t_function_det().
+t_function(Types, Ret) ->
+  Rep = {Types, Ret, []},
+  #t{kind = ?function_tag, rep = Rep, deps = unify_deps([Ret|Types])}.
+
+-spec t_function([raw_type()], raw_type(), [t_constraint()]) -> t_function_det().
+t_function(Types, Ret, Constraints) ->
+  Rep = {Types, Ret, Constraints},
+  Ts = [T || {_V, T} <- Constraints],
+  #t{kind = ?function_tag, rep = Rep, deps = unify_deps([Ret|Types] ++ Ts)}.
+
+%% Accessors of representations.
+
+-spec params_of_t_function_det(t_function_det()) -> [raw_type()].
+params_of_t_function_det(#t{kind = ?function_tag, rep = {Params, _Ret, _Constraints}}) ->
+  Params.
+
+-spec ret_of_t_function_det(t_function_det()) -> raw_type().
+ret_of_t_function_det(#t{kind = ?function_tag, rep = {_Params, Ret, _Constraints}}) ->
+  Ret.
+
+-spec atom_of_t_atom_lit(t_atom_lit()) -> atom().
+atom_of_t_atom_lit(#t{kind = ?atom_lit_tag, rep = Atom}) ->
+  Atom.
+
+-spec integer_of_t_integer_lit(t_integer_lit()) -> integer().
+integer_of_t_integer_lit(#t{kind = ?integer_lit_tag, rep = Integer}) ->
+  Integer.
+
+-spec elements_type_of_t_list(t_list()) -> raw_type().
+elements_type_of_t_list(#t{kind = ?list_tag, rep = Type}) ->
+  Type.
+
+-spec elements_type_of_t_nonempty_list(t_nonempty_list()) -> raw_type().
+elements_type_of_t_nonempty_list(#t{kind = ?nonempty_list_tag, rep = Type}) ->
+  Type.
+
+-spec elements_types_of_t_tuple(t_tuple()) -> [raw_type()].
+elements_types_of_t_tuple(#t{kind = ?tuple_tag, rep = Types}) ->
+  Types.
+
+-spec elements_types_of_t_union(t_union()) -> [raw_type()].
+elements_types_of_t_union(#t{kind = ?union_tag, rep = Types}) ->
+  Types.
+
+-spec bounds_of_t_range(t_range()) -> {t_range_limit(), t_range_limit()}.
+bounds_of_t_range(#t{kind = ?range_tag, rep = Limits}) ->
+  Limits.
+
+-spec segment_size_of_bitstring(t_bitstring()) -> integer().
+segment_size_of_bitstring(#t{kind = ?bitstring_tag, rep = Sz}) ->
+  Sz.
+
+-spec is_tvar_wild_card(t_type_var()) -> boolean().
+is_tvar_wild_card(#t{kind = ?type_variable, rep = {?type_var, Var}}) ->
+  Var =:= '_'.
+
+%% Helper functions for kinds.
+
+-spec get_kind(raw_type()) -> atom().
+get_kind(Type) ->
+  Type#t.kind.
+
+%% Helper functions for dependencies.
+
+-spec get_deps(raw_type()) -> deps().
+get_deps(Type) ->
+  Type#t.deps.
+
+-spec has_deps(raw_type()) -> boolean().
+has_deps(Type) ->
+  get_deps(Type) =/= ordsets:new().
+
+-spec add_dep(dep(), deps()) -> deps().
+add_dep(Dep, Deps) ->
+  ordsets:add_element(Dep, Deps).
+
+-spec unify_deps([raw_type()]) -> deps().
+unify_deps(Types) ->
+  ordsets:union([T#t.deps || T <- Types]).
+
+%% Deal with specs.
+
+-spec retrieve_specs([cuter_cerl:cerl_attr_spec()]) -> stored_specs().
+retrieve_specs(SpecAttrs) ->
+  lists:foldl(fun process_spec_attr/2, dict:new(), SpecAttrs).
+
+-spec process_spec_attr(cuter_cerl:cerl_attr_spec(), stored_specs()) -> stored_specs().
+process_spec_attr({FA, Specs}, Processed) ->
+  Xs = [t_spec_from_form(Spec) || Spec <- Specs],
+  dict:store(FA, Xs, Processed).
+
+-spec t_spec_from_form(cuter_cerl:cerl_spec_func()) -> t_function_det().
+t_spec_from_form({type, _, 'fun', _}=Fun) ->
+  t_function_from_form(Fun);
+t_spec_from_form({type, _, 'bounded_fun', _}=Fun) ->
+  t_bounded_function_from_form(Fun).
+
+-spec find_spec(stored_spec_key(), stored_specs()) -> {'ok', stored_spec_value()} | 'error'.
+find_spec(FA, Specs) ->
+  dict:find(FA, Specs).
+
+%% Parse the spec of an MFA.
+
+-type spec_parse_reply() :: {error, has_remote_types | recursive_type}
+                          | {error, unsupported_type, type_name()}
+                          | {ok, erl_spec()}.
+
+-spec parse_spec(stored_spec_key(), stored_spec_value(), stored_types()) -> spec_parse_reply().
+parse_spec(FA, Spec, Types) ->
+  try parse_spec_clauses(FA, Spec, Types, []) of
+    {error, has_remote_types}=E -> E;
+    Parsed -> {ok, Parsed}
+  catch
+    throw:remote_type -> {error, has_remote_types};
+    throw:recursive_type -> {error, recursive_type};
+    throw:{unsupported, Name} -> {error, unsupported_type, Name}
+  end.
+
+
+parse_spec_clauses(_FA, [], _Types, Acc) ->
+  lists:reverse(Acc);
+parse_spec_clauses(FA, [Clause|Clauses], Types, Acc) ->
+  case has_deps(Clause) of
+    true  -> {error, has_remote_types};
+    false ->
+      Visited = ordsets:add_element(FA, ordsets:new()),
+      Simplified = simplify(Clause, Types, dict:new(), Visited),
+      parse_spec_clauses(FA, Clauses, Types, [Simplified|Acc])
+  end.
+
+add_constraints_to_env([], Env) ->
+  Env;
+add_constraints_to_env([{Var, Type}|Cs], Env) ->
+  F = fun(StoredTypes, E, Visited) -> simplify(Type, StoredTypes, E, Visited) end,
+  Env1 = dict:store(Var#t.rep, F, Env),
+  add_constraints_to_env(Cs, Env1).
+
+bind_parameters([], [], Env) ->
+  Env;
+bind_parameters([P|Ps], [A|As], Env) ->
+  F = fun(StoredTypes, E, Visited) -> simplify(A, StoredTypes, E, Visited) end,
+  Env1 = dict:store(P, F, Env),
+  bind_parameters(Ps, As, Env1).
+
+-spec simplify(raw_type(), stored_types(), type_var_env(), ordsets:ordset(stored_spec_key())) -> raw_type().
+%% fun
+simplify(#t{kind = ?function_tag, rep = {Params, Ret, Constraints}}=Raw, StoredTypes, Env, Visited) ->
+  Env1 = add_constraints_to_env(Constraints, Env),
+  ParamsSimplified = [simplify(P, StoredTypes, Env1, Visited) || P <- Params],
+  RetSimplified = simplify(Ret, StoredTypes, Env1, Visited),
+  Rep = {ParamsSimplified, RetSimplified, []},
+  Raw#t{rep = Rep};
+%% tuple
+simplify(#t{kind = ?tuple_tag, rep = Types}=Raw, StoredTypes, Env, Visited) ->
+  Rep = [simplify(T, StoredTypes, Env, Visited) || T <- Types],
+  Raw#t{rep = Rep};
+%% list / nonempty_list
+simplify(#t{kind = Tag, rep = Type}=Raw, StoredTypes, Env, Visited) when Tag =:= ?list_tag; Tag =:= ?nonempty_list_tag ->
+  Rep = simplify(Type, StoredTypes, Env, Visited),
+  Raw#t{rep = Rep};
+%% union
+simplify(#t{kind = ?union_tag, rep = Types}=Raw, StoredTypes, Env, Visited) ->
+  Rep = [simplify(T, StoredTypes, Env, Visited) || T <- Types],
+  Raw#t{rep = Rep};
+%% local type
+simplify(#t{kind = ?local_tag, rep = {Name, Args}}, StoredTypes, Env, Visited) ->
+  Arity = length(Args),
+  TA = {Name, Arity},
+  case ordsets:is_element(TA, Visited) of
+    true -> throw(recursive_type);
+    false ->
+      case dict:find({type, Name, Arity}, StoredTypes) of
+        error -> throw({unsupported, Name});
+        {ok, {Type, Params}} ->
+          Env1 = bind_parameters(Params, Args, Env),
+          simplify(Type, StoredTypes, Env1, [TA|Visited])
+      end
+  end;
+%% type variable
+simplify(#t{kind = ?type_variable, rep = TVar}=T, StoredTypes, Env, Visited) ->
+  case is_tvar_wild_card(T) of
+    true -> t_any();
+    false ->
+      V = dict:fetch(TVar, Env),
+      V(StoredTypes, Env, Visited)
+  end;
+simplify(#t{kind = ?remote_tag}, _StoredTypes, _Env, _Visited) ->
+  throw(remote_type);
+%% record
+simplify(#t{kind = ?record_tag, rep = {Name, OverridenFields}}, StoredTypes, Env, Visited) ->
+  RecordDecl = dict:fetch({record, Name}, StoredTypes),
+  Fields = fields_of_t_record(RecordDecl),
+  ActualFields = replace_record_fields(Fields, OverridenFields),
+  FinalFields = [{N, simplify(T, StoredTypes, Env, Visited)} || {N, T} <- ActualFields],
+  Simplified = [T || {_, T} <- FinalFields],
+  t_tuple([t_atom_lit(Name)|Simplified]);
+%% all others
+simplify(Raw, _StoredTypes, _Env, _Visited) ->
+  Raw.
+
+-spec replace_record_fields([record_field_type()], [record_field_type()]) -> [record_field_type()].
+replace_record_fields(Fields, []) ->
+  Fields;
+replace_record_fields(Fields, [{Name, Type}|Rest]) ->
+  Replaced = lists:keyreplace(Name, 1, Fields, {Name, Type}),
+  replace_record_fields(Replaced, Rest).
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.hrl b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.hrl
new file mode 100644
index 0000000000..4172184709
--- /dev/null
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/cuter/cuter_types.hrl
@@ -0,0 +1,26 @@
+%% -*- erlang-indent-level: 2 -*-
+%%------------------------------------------------------------------------------
+
+%%====================================================================
+%% Tags for the kind of encoded types.
+%%====================================================================
+
+-define(atom_lit_tag, atom_lit).
+-define(integer_lit_tag, integer_lit).
+-define(integer_tag, integer).
+-define(nil_tag, nil).
+-define(any_tag, any).
+-define(atom_tag, atom).
+-define(float_tag, float).
+-define(tuple_tag, tuple).
+-define(list_tag, list).
+-define(nonempty_list_tag, nonempty_list).
+-define(union_tag, union).
+-define(range_tag, range).
+-define(bitstring_tag, bitstring).
+-define(neg_inf, neg_inf).
+-define(pos_inf, pos_inf).
+-define(remote_tag, remote).
+-define(local_tag, local).
+-define(record_tag, record).
+-define(function_tag, function).
diff --git a/lib/dialyzer/test/small_SUITE_data/src/remote_field.erl b/lib/dialyzer/test/small_SUITE_data/src/remote_field.erl
index c34fa1b9dd..d83f2e3234 100644
--- a/lib/dialyzer/test/small_SUITE_data/src/remote_field.erl
+++ b/lib/dialyzer/test/small_SUITE_data/src/remote_field.erl
@@ -3,7 +3,7 @@
 -type f(T) :: {ssl:sslsocket(), T}.
 
 -record(r1, { f1 :: f(_) }).
--type r1(T) :: #r1{ f1 :: fun((ssl:sslsocket(), T) -> any()) }.
+-type r1(T) :: #r1{ f1 :: {ssl:sslsocket(), T} }.
 
 -record(state, {
           r :: r1(T),