Merge branch 'hb/dialyzer/fix_loop/OTP-12826'

* hb/dialyzer/fix_loop/OTP-12826:
  dialyzer: Simplify some code
  dialyzer: Fix a bug in the expansion of forms

7 files changed, 1038 insertions, 94 deletions

diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index 4a1ba9c539..914a4c6d8f 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -409,7 +409,7 @@ contract_from_form([{type, _, 'fun', [_, _]} = Form | Left], Module, RecDict,
     fun(ExpTypes, AllRecords) ->
 	NewType =
 	  try
-            erl_types:t_from_form(Form, ExpTypes, Module, AllRecords)
+            from_form_with_check(Form, ExpTypes, Module, AllRecords)
 	  catch
 	    throw:{error, Msg} ->
 	      {File, Line} = FileLine,
@@ -430,8 +430,8 @@ contract_from_form([{type, _L1, bounded_fun,
     fun(ExpTypes, AllRecords) ->
 	{Constr1, VarDict} =
 	  process_constraints(Constr, Module, RecDict, ExpTypes, AllRecords),
-        NewType = erl_types:t_from_form(Form, ExpTypes, Module, AllRecords,
-                                        VarDict),
+        NewType = from_form_with_check(Form, ExpTypes, Module, AllRecords,
+                                       VarDict),
         NewTypeNoVars = erl_types:subst_all_vars_to_any(NewType),
 	{NewTypeNoVars, Constr1}
     end,
@@ -454,7 +454,7 @@ initialize_constraints([], _Module, _RecDict, _ExpTypes, _AllRecords, Acc) ->
 initialize_constraints([Constr|Rest], Module, RecDict, ExpTypes, AllRecords, Acc) ->
   case Constr of
     {type, _, constraint, [{atom, _, is_subtype}, [Type1, Type2]]} ->
-      T1 = final_form(Type1, Module, ExpTypes, AllRecords, dict:new()),
+      T1 = final_form(Type1, ExpTypes, Module, AllRecords, dict:new()),
       Entry = {T1, Type2},
       initialize_constraints(Rest, Module, RecDict, ExpTypes, AllRecords, [Entry|Acc]);
     {type, _, constraint, [{atom,_,Name}, List]} ->
@@ -483,7 +483,16 @@ constraints_fixpoint(OldVarDict, Module, Constrs, RecDict, ExpTypes, AllRecords)
       constraints_fixpoint(NewVarDict, Module, Constrs, RecDict, ExpTypes, AllRecords)
   end.
 
-final_form(Form, Module, ExpTypes, AllRecords, VarDict) ->
+final_form(Form, ExpTypes, Module, AllRecords, VarDict) ->
+  from_form_with_check(Form, ExpTypes, Module, AllRecords, VarDict).
+
+from_form_with_check(Form, ExpTypes, Module, AllRecords) ->
+  erl_types:t_check_record_fields(Form, ExpTypes, Module, AllRecords),
+  erl_types:t_from_form(Form, ExpTypes, Module, AllRecords).
+
+from_form_with_check(Form, ExpTypes, Module, AllRecords, VarDict) ->
+  erl_types:t_check_record_fields(Form, ExpTypes, Module, AllRecords,
+                                  VarDict),
   erl_types:t_from_form(Form, ExpTypes, Module, AllRecords, VarDict).
 
 constraints_to_dict(Constrs, Module, RecDict, ExpTypes, AllRecords, VarDict) ->
@@ -495,7 +504,7 @@ constraints_to_subs([], _Module, _RecDict, _ExpTypes, _AllRecords, _VarDict, Acc
   Acc;
 constraints_to_subs([C|Rest], Module, RecDict, ExpTypes, AllRecords, VarDict, Acc) ->
   {T1, Form2} = C,
-  T2 = final_form(Form2, Module, ExpTypes, AllRecords, VarDict),
+  T2 = final_form(Form2, ExpTypes, Module, AllRecords, VarDict),
   NewAcc = [{subtype, T1, T2}|Acc],
   constraints_to_subs(Rest, Module, RecDict, ExpTypes, AllRecords, VarDict, NewAcc).
 
diff --git a/lib/dialyzer/src/dialyzer_utils.erl b/lib/dialyzer/src/dialyzer_utils.erl
index e29fc3ba8b..dbfd20014c 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -64,15 +64,15 @@ print_types(RecDict) ->
 print_types1([], _) ->
   ok;
 print_types1([{type, _Name, _NArgs} = Key|T], RecDict) ->
-  {ok, {{_Mod, _Form, _Args}, Type}} = dict:find(Key, RecDict),
+  {ok, {{_Mod, _FileLine, _Form, _Args}, Type}} = dict:find(Key, RecDict),
   io:format("\n~w: ~w\n", [Key, Type]),
   print_types1(T, RecDict);
 print_types1([{opaque, _Name, _NArgs} = Key|T], RecDict) ->
-  {ok, {{_Mod, _Form, _Args}, Type}} = dict:find(Key, RecDict),
+  {ok, {{_Mod, _FileLine, _Form, _Args}, Type}} = dict:find(Key, RecDict),
   io:format("\n~w: ~w\n", [Key, Type]),
   print_types1(T, RecDict);
 print_types1([{record, _Name} = Key|T], RecDict) ->
-  {ok, [{_Arity, _Fields} = AF]} = dict:find(Key, RecDict),
+  {ok, {_FileLine, [{_Arity, _Fields} = AF]}} = dict:find(Key, RecDict),
   io:format("~w: ~w\n\n", [Key, AF]),
   print_types1(T, RecDict).
 -define(debug(D_), print_types(D_)).
@@ -203,52 +203,53 @@ get_record_and_type_info(AbstractCode) ->
 	{'ok', dict:dict()} | {'error', string()}.
 
 get_record_and_type_info(AbstractCode, Module, RecDict) ->
-  get_record_and_type_info(AbstractCode, Module, [], RecDict).
+  get_record_and_type_info(AbstractCode, Module, RecDict, "nofile").
 
-get_record_and_type_info([{attribute, _, record, {Name, Fields0}}|Left],
-			 Module, Records, RecDict) ->
+get_record_and_type_info([{attribute, A, record, {Name, Fields0}}|Left],
+			 Module, RecDict, File) ->
   {ok, Fields} = get_record_fields(Fields0, RecDict),
   Arity = length(Fields),
-  NewRecDict = dict:store({record, Name}, [{Arity, Fields}], RecDict),
-  get_record_and_type_info(Left, Module, [{record, Name}|Records], NewRecDict);
-get_record_and_type_info([{attribute, _, type, {{record, Name}, Fields0, []}}
-			  |Left], Module, Records, RecDict) ->
+  FN = {File, erl_anno:line(A)},
+  NewRecDict = dict:store({record, Name}, {FN, [{Arity,Fields}]}, RecDict),
+  get_record_and_type_info(Left, Module, NewRecDict, File);
+get_record_and_type_info([{attribute, A, type, {{record, Name}, Fields0, []}}
+			  |Left], Module, RecDict, File) ->
   %% This overrides the original record declaration.
   {ok, Fields} = get_record_fields(Fields0, RecDict),
   Arity = length(Fields),
-  NewRecDict = dict:store({record, Name}, [{Arity, Fields}], RecDict),
-  get_record_and_type_info(Left, Module, Records, NewRecDict);
-get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm}}|Left],
-			 Module, Records, RecDict) when Attr =:= 'type';
-                                                        Attr =:= 'opaque' ->
-  try add_new_type(Attr, Name, TypeForm, [], Module, RecDict) of
+  FN = {File, erl_anno:line(A)},
+  NewRecDict = dict:store({record, Name}, {FN, [{Arity, Fields}]}, RecDict),
+  get_record_and_type_info(Left, Module, NewRecDict, File);
+get_record_and_type_info([{attribute, A, Attr, {Name, TypeForm}}|Left],
+			 Module, RecDict, File)
+               when Attr =:= 'type'; Attr =:= 'opaque' ->
+  FN = {File, erl_anno:line(A)},
+  try add_new_type(Attr, Name, TypeForm, [], Module, FN, RecDict) of
     NewRecDict ->
-      get_record_and_type_info(Left, Module, Records, NewRecDict)
+      get_record_and_type_info(Left, Module, NewRecDict, File)
   catch
     throw:{error, _} = Error -> Error
   end;
-get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm, Args}}|Left],
-			 Module, Records, RecDict) when Attr =:= 'type';
-                                                        Attr =:= 'opaque' ->
-  try add_new_type(Attr, Name, TypeForm, Args, Module, RecDict) of
+get_record_and_type_info([{attribute, A, Attr, {Name, TypeForm, Args}}|Left],
+			 Module, RecDict, File)
+               when Attr =:= 'type'; Attr =:= 'opaque' ->
+  FN = {File, erl_anno:line(A)},
+  try add_new_type(Attr, Name, TypeForm, Args, Module, FN, RecDict) of
     NewRecDict ->
-      get_record_and_type_info(Left, Module, Records, NewRecDict)
+      get_record_and_type_info(Left, Module, NewRecDict, File)
   catch
     throw:{error, _} = Error -> Error
   end;
-get_record_and_type_info([_Other|Left], Module, Records, RecDict) ->
-  get_record_and_type_info(Left, Module, Records, RecDict);
-get_record_and_type_info([], _Module, Records, RecDict) ->
-  case
-    check_type_of_record_fields(lists:reverse(Records), RecDict)
-  of
-    ok ->
-      {ok, RecDict};
-    {error, Name, Error} ->
-      {error, flat_format("  Error while parsing #~w{}: ~s\n", [Name, Error])}
-  end.
-
-add_new_type(TypeOrOpaque, Name, TypeForm, ArgForms, Module, RecDict) ->
+get_record_and_type_info([{attribute, _, file, {IncludeFile, _}}|Left],
+                         Module, RecDict, _File) ->
+  get_record_and_type_info(Left, Module, RecDict, IncludeFile);
+get_record_and_type_info([_Other|Left], Module, RecDict, File) ->
+  get_record_and_type_info(Left, Module, RecDict, File);
+get_record_and_type_info([], _Module, RecDict, _File) ->
+  {ok, RecDict}.
+
+add_new_type(TypeOrOpaque, Name, TypeForm, ArgForms, Module, FN,
+             RecDict) ->
   Arity = length(ArgForms),
   case erl_types:type_is_defined(TypeOrOpaque, Name, Arity, RecDict) of
     true ->
@@ -258,7 +259,7 @@ add_new_type(TypeOrOpaque, Name, TypeForm, ArgForms, Module, RecDict) ->
       try erl_types:t_var_names(ArgForms) of
         ArgNames ->
 	  dict:store({TypeOrOpaque, Name, Arity},
-                     {{Module, TypeForm, ArgNames},
+                     {{Module, FN, TypeForm, ArgNames},
                       erl_types:t_any()}, RecDict)
       catch
         _:_ ->
@@ -280,32 +281,16 @@ get_record_fields([{typed_record_field, OrdRecField, TypeForm}|Left],
     end,
   get_record_fields(Left, RecDict, [{Name, TypeForm}|Acc]);
 get_record_fields([{record_field, _Line, Name}|Left], RecDict, Acc) ->
-  NewAcc = [{erl_parse:normalise(Name), {var, -1, '_'}}|Acc],
+  A = erl_anno:set_generated(true, erl_anno:new(1)),
+  NewAcc = [{erl_parse:normalise(Name), {var, A, '_'}}|Acc],
   get_record_fields(Left, RecDict, NewAcc);
 get_record_fields([{record_field, _Line, Name, _Init}|Left], RecDict, Acc) ->
-  NewAcc = [{erl_parse:normalise(Name), {var, -1, '_'}}|Acc],
+  A = erl_anno:set_generated(true, erl_anno:new(1)),
+  NewAcc = [{erl_parse:normalise(Name), {var, A, '_'}}|Acc],
   get_record_fields(Left, RecDict, NewAcc);
 get_record_fields([], _RecDict, Acc) ->
   lists:reverse(Acc).
 
-%% Just check the local types. process_record_remote_types will add
-%% the types later.
-check_type_of_record_fields([], _RecDict) ->
-  ok;
-check_type_of_record_fields([RecKey|Recs], RecDict) ->
-  {ok, [{_Arity, Fields}]} = dict:find(RecKey, RecDict),
-  try
-    [erl_types:t_from_form_without_remote(FieldTypeForm, RecDict)
-     || {_FieldName, FieldTypeForm, _} <- Fields]
-  of
-    L when is_list(L) ->
-      check_type_of_record_fields(Recs, RecDict)
-  catch
-    throw:{error, Error} ->
-      {record, Name} = RecKey,
-      {error, Name, Error}
-  end.
-
 -spec process_record_remote_types(codeserver()) -> codeserver().
 
 %% The field types are cached. Used during analysis when handling records.
@@ -327,9 +312,10 @@ process_record_remote_types(CServer) ->
                                                 TempRecords)}
                          || {Name, Field, _} <- Fields]
                     end,
-                  orddict:map(FieldFun, Value);
+                  {FileLine, Fields} = Value,
+                  {FileLine, orddict:map(FieldFun, Fields)};
                 {opaque, _, _} ->
-                  {{_Module, Form, _ArgNames}=F, _Type} = Value,
+                  {{_Module, _FileLine, Form, _ArgNames}=F, _Type} = Value,
                   Type = erl_types:t_from_form(Form, TempExpTypes, Module,
                                                TempRecords),
                   {F, Type};
@@ -340,13 +326,53 @@ process_record_remote_types(CServer) ->
     end,
   try dict:map(ModuleFun, TempRecords) of
     NewRecords ->
+      ok = check_record_fields(NewRecords, TempExpTypes),
       CServer1 = dialyzer_codeserver:finalize_records(NewRecords, CServer),
       dialyzer_codeserver:finalize_exported_types(TempExpTypes, CServer1)
   catch
-    throw:{error, _RecName, _Error} = Error->
+    throw:{error, _RecName, _Error} = Error ->
       Error
   end.
 
+check_record_fields(Records, TempExpTypes) ->
+  CheckFun =
+    fun({Module, Element}) ->
+        CheckForm = fun(F) ->
+                      erl_types:t_check_record_fields(F, TempExpTypes,
+                                                      Module, Records)
+                  end,
+        ElemFun =
+          fun({Key, Value}) ->
+              case Key of
+                {record, _Name} ->
+                  FieldFun =
+                    fun({_Arity, Fields}) ->
+                        _ = [ok = CheckForm(Field) || {_, Field, _} <- Fields],
+                        ok
+                    end,
+                  {FileLine, Fields} = Value,
+                  Fun = fun() -> lists:foreach(FieldFun, Fields) end,
+                  msg_with_position(Fun, FileLine);
+                {_OpaqueOrType, _Name, _} ->
+                  {{_Module, FileLine, Form, _ArgNames}, _Type} = Value,
+                  Fun = fun() -> ok = CheckForm(Form) end,
+                  msg_with_position(Fun, FileLine)
+              end
+          end,
+        lists:foreach(ElemFun, dict:to_list(Element))
+    end,
+  lists:foreach(CheckFun, dict:to_list(Records)).
+
+msg_with_position(Fun, FileLine) ->
+  try Fun()
+  catch
+    throw:{error, Msg} ->
+      {File, Line} = FileLine,
+      BaseName = filename:basename(File),
+      NewMsg = io_lib:format("~s:~p: ~s", [BaseName, Line, Msg]),
+      throw({error, NewMsg})
+  end.
+
 -spec merge_records(dict:dict(), dict:dict()) -> dict:dict().
 
 merge_records(NewRecords, OldRecords) ->
@@ -385,11 +411,11 @@ get_optional_callbacks(Abs) ->
 %%  - Constraint is of the form {subtype, T1, T2} where T1 and T2
 %%    are erl_types:erl_type()
 
-get_spec_info([{attribute, Attr, Contract, {Id, TypeSpec}}|Left],
+get_spec_info([{attribute, Anno, Contract, {Id, TypeSpec}}|Left],
 	      SpecDict, CallbackDict, RecordsDict, ModName, OptCb, File)
   when ((Contract =:= 'spec') or (Contract =:= 'callback')),
        is_list(TypeSpec) ->
-  Ln = erl_anno:line(Attr),
+  Ln = erl_anno:line(Anno),
   MFA = case Id of
 	  {_, _, _} = T -> T;
 	  {F, A} -> {ModName, F, A}
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),
diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl
index 14335cf635..e7823a596a 100644
--- a/lib/hipe/cerl/erl_types.erl
+++ b/lib/hipe/cerl/erl_types.erl
@@ -82,6 +82,8 @@
          t_from_form/4,
          t_from_form/5,
          t_from_form_without_remote/2,
+         t_check_record_fields/4,
+         t_check_record_fields/5,
 	 t_from_range/2,
 	 t_from_range_unsafe/2,
 	 t_from_term/1,
@@ -747,7 +749,8 @@ t_opaque_from_records(RecDict) ->
 		    end
 		end, RecDict),
   OpaqueTypeDict =
-    dict:map(fun({opaque, Name, _Arity}, {{Module, _Form, ArgNames}, _Type}) ->
+    dict:map(fun({opaque, Name, _Arity},
+                 {{Module, _FileLine, _Form, ArgNames}, _Type}) ->
                  %% Args = args_to_types(ArgNames),
                  %% List = lists:zip(ArgNames, Args),
                  %% TmpVarDict = dict:from_list(List),
@@ -4189,7 +4192,7 @@ builtin_type(Name, Type, TypeNames, ET, M, MR, V, D, L) ->
   case dict:find(M, MR) of
     {ok, R} ->
       case lookup_type(Name, 0, R) of
-        {_, {{_M, _F, _A}, _T}} ->
+        {_, {{_M, _FL, _F, _A}, _T}} ->
           type_from_form(Name, [], TypeNames, ET, M, MR, V, D, L);
         error ->
           {Type, L}
@@ -4203,7 +4206,7 @@ type_from_form(Name, Args, TypeNames, ET, M, MR, V, D, L) ->
   {ArgTypes, L1} = list_from_form(Args, TypeNames, ET, M, MR, V, D, L),
   {ok, R} = dict:find(M, MR),
   case lookup_type(Name, ArgsLen, R) of
-    {type, {{Module, Form, ArgNames}, _Type}} ->
+    {type, {{Module, _FileName, Form, ArgNames}, _Type}} ->
       TypeName = {type, Module, Name, ArgsLen},
       case can_unfold_more(TypeName, TypeNames) of
         true ->
@@ -4213,7 +4216,7 @@ type_from_form(Name, Args, TypeNames, ET, M, MR, V, D, L) ->
         false ->
           {t_any(), L1}
       end;
-    {opaque, {{Module, Form, ArgNames}, Type}} ->
+    {opaque, {{Module, _FileName, Form, ArgNames}, Type}} ->
       TypeName = {opaque, Module, Name, ArgsLen},
       {Rep, L2} =
         case can_unfold_more(TypeName, TypeNames) of
@@ -4251,7 +4254,7 @@ remote_from_form(RemMod, Name, Args, TypeNames, ET, M, MR, V, D, L) ->
           case sets:is_element(MFA, ET) of
             true ->
               case lookup_type(Name, ArgsLen, RemDict) of
-                {type, {{_Mod, Form, ArgNames}, _Type}} ->
+                {type, {{_Mod, _FileLine, Form, ArgNames}, _Type}} ->
                   RemType = {type, RemMod, Name, ArgsLen},
                   case can_unfold_more(RemType, TypeNames) of
                     true ->
@@ -4263,7 +4266,7 @@ remote_from_form(RemMod, Name, Args, TypeNames, ET, M, MR, V, D, L) ->
                     false ->
                       {t_any(), L1}
                   end;
-                {opaque, {{Mod, Form, ArgNames}, Type}} ->
+                {opaque, {{Mod, _FileLine, Form, ArgNames}, Type}} ->
                   RemType = {opaque, RemMod, Name, ArgsLen},
                   List = lists:zip(ArgNames, ArgTypes),
                   TmpVarDict = dict:from_list(List),
@@ -4358,34 +4361,24 @@ build_field_dict(FieldTypes, TypeNames, ET, M, MR, V, D, L) ->
 build_field_dict([{type, _, field_type, [{atom, _, Name}, Type]}|Left],
 		 TypeNames, ET, M, MR, V, D, L, Acc) ->
   {T, L1} = t_from_form(Type, TypeNames, ET, M, MR, V, D, L - 1),
-  %% The cached record field type (DeclType) in
-  %% get_mod_record_types()), was created with a similar call as TT.
-  %% Using T for the subtype test does not work since any() is not
-  %% always a subset of the field type.
-  TT = t_from_form(Type, ET, M, MR, V),
-  NewAcc = [{Name, Type, T, TT}|Acc],
+  NewAcc = [{Name, Type, T}|Acc],
   {Dict, L2} =
     build_field_dict(Left, TypeNames, ET, M, MR, V, D, L1, NewAcc),
   {Dict, L2};
 build_field_dict([], _TypeNames, _ET, _M, _MR, _V, _D, L, Acc) ->
   {lists:keysort(1, Acc), L}.
 
-get_mod_record_types([{FieldName, _Abstr, DeclType}|Left1],
-                     [{FieldName, TypeForm, ModType, ModTypeTest}|Left2],
+get_mod_record_types([{FieldName, _Abstr, _DeclType}|Left1],
+                     [{FieldName, TypeForm, ModType}|Left2],
                      Acc) ->
-  ModTypeNoVars = subst_all_vars_to_any(ModTypeTest),
-  case t_is_subtype(ModTypeNoVars, DeclType) of
-    false -> {error, FieldName};
-    true -> get_mod_record_types(Left1, Left2,
-                              [{FieldName, TypeForm, ModType}|Acc])
-  end;
+  get_mod_record_types(Left1, Left2, [{FieldName, TypeForm, ModType}|Acc]);
 get_mod_record_types([{FieldName1, _Abstr, _DeclType} = DT|Left1],
-                     [{FieldName2, _FormType, _ModType, _TT}|_] = List2,
+                     [{FieldName2, _FormType, _ModType}|_] = List2,
                      Acc) when FieldName1 < FieldName2 ->
   get_mod_record_types(Left1, List2, [DT|Acc]);
 get_mod_record_types(Left1, [], Acc) ->
   {ok, lists:keysort(1, Left1++Acc)};
-get_mod_record_types(_, [{FieldName2, _FormType, _ModType, _TT}|_], _Acc) ->
+get_mod_record_types(_, [{FieldName2, _FormType, _ModType}|_], _Acc) ->
   {error, FieldName2}.
 
 %% It is important to create a limited version of the record type
@@ -4406,6 +4399,74 @@ list_from_form([H|Tail], TypeNames, ET, M, MR, V, D, L) ->
   {T1, L2} = list_from_form(Tail, TypeNames, ET, M, MR, V, D, L1),
   {[H1|T1], L2}.
 
+-spec t_check_record_fields(parse_form(), sets:set(mfa()), module(),
+                            mod_records()) -> ok.
+
+t_check_record_fields(Form, ExpTypes, Module, RecDict) ->
+  t_check_record_fields(Form, ExpTypes, Module, RecDict, dict:new()).
+
+-spec t_check_record_fields(parse_form(), sets:set(mfa()), module(),
+                            mod_records(), var_table()) -> ok.
+
+%% If there is something wrong with parse_form()
+%% throw({error, io_lib:chars()} is called.
+
+t_check_record_fields({var, _L, _}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({ann_type, _L, [_Var, Type]}, ET, M, MR, V) ->
+  t_check_record_fields(Type, ET, M, MR, V);
+t_check_record_fields({paren_type, _L, [Type]}, ET, M, MR, V) ->
+  t_check_record_fields(Type, ET, M, MR, V);
+t_check_record_fields({remote_type, _L, [{atom, _, _}, {atom, _, _}, Args]},
+                    ET, M, MR, V) ->
+  list_check_record_fields(Args, ET, M, MR, V);
+t_check_record_fields({atom, _L, _}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({integer, _L, _}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({op, _L, _Op, _Arg}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({op, _L, _Op, _Arg1, _Arg2}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({type, _L, tuple, any}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({type, _L, map, any}, _ET, _M, _MR, _V) -> ok;
+t_check_record_fields({type, _L, binary, [_Base, _Unit]}, _ET, _M, _MR, _V) ->
+  ok;
+t_check_record_fields({type, _L, 'fun', [{type, _, any}, Range]},
+                      ET, M, MR, V) ->
+  t_check_record_fields(Range, ET, M, MR, V);
+t_check_record_fields({type, _L, range, [_From, _To]}, _ET, _M, _MR, _V) ->
+  ok;
+t_check_record_fields({type, _L, record, [Name|Fields]}, ET, M, MR, V) ->
+  check_record(Name, Fields, ET, M, MR, V);
+t_check_record_fields({type, _L, _, Args}, ET, M, MR, V) ->
+  list_check_record_fields(Args, ET, M, MR, V);
+t_check_record_fields({user_type, _L, _Name, Args}, ET, M, MR, V) ->
+  list_check_record_fields(Args, ET, M, MR, V).
+
+check_record({atom, _, Name}, ModFields, ET, M, MR, V) ->
+  {ok, R} = dict:find(M, MR),
+  {ok, DeclFields} = lookup_record(Name, R),
+  case check_fields(ModFields, DeclFields, ET, M, MR, V) of
+    {error, FieldName} ->
+       throw({error, io_lib:format("Illegal declaration of #~w{~w}\n",
+                                   [Name, FieldName])});
+    ok -> ok
+  end.
+
+check_fields([{type, _, field_type, [{atom, _, Name}, Abstr]}|Left],
+             DeclFields, ET, M, MR, V) ->
+  Type = t_from_form(Abstr, ET, M, MR, V),
+  {Name, _, DeclType} = lists:keyfind(Name, 1, DeclFields),
+  TypeNoVars = subst_all_vars_to_any(Type),
+  case t_is_subtype(TypeNoVars, DeclType) of
+    false -> {error, Name};
+    true -> check_fields(Left, DeclFields, ET, M, MR, V)
+  end;
+check_fields([], _Decl, _ET, _M, _MR, _V) ->
+  ok.
+
+list_check_record_fields([], _ET, _M, _MR, _V) ->
+  ok;
+list_check_record_fields([H|Tail], ET, M, MR, V) ->
+  ok = t_check_record_fields(H, ET, M, MR, V),
+  list_check_record_fields(Tail, ET, M, MR, V).
+
 -spec t_var_names([erl_type()]) -> [atom()].
 
 t_var_names([{var, _, Name}|L]) when L =/= '_' ->
@@ -4556,9 +4617,9 @@ is_erl_type(_) -> false.
 
 lookup_record(Tag, RecDict) when is_atom(Tag) ->
   case dict:find({record, Tag}, RecDict) of
-    {ok, [{_Arity, Fields}]} ->
+    {ok, {_FileLine, [{_Arity, Fields}]}} ->
       {ok, Fields};
-    {ok, List} when is_list(List) ->
+    {ok, {_FileLine, List}} when is_list(List) ->
       %% This will have to do, since we do not know which record we
       %% are looking for.
       error;
@@ -4571,8 +4632,8 @@ lookup_record(Tag, RecDict) when is_atom(Tag) ->
 
 lookup_record(Tag, Arity, RecDict) when is_atom(Tag) ->
   case dict:find({record, Tag}, RecDict) of
-    {ok, [{Arity, Fields}]} -> {ok, Fields};
-    {ok, OrdDict} -> orddict:find(Arity, OrdDict);
+    {ok, {_FileLine, [{Arity, Fields}]}} -> {ok, Fields};
+    {ok, {_FileLine, OrdDict}} -> orddict:find(Arity, OrdDict);
     error -> error
   end.