[dialyzer] Fix handling of literal records

This ticket is about records in Erlang code, and when to check the
fields against the (optional) types given when defining records.

Dialyzer operates on the Erlang Core format, where there are no trace
of records. The fix implemented is a Real Hack:

Given the new option 'dialyzer' erl_expand_records marks the line
number of records in a way that is undone by v3_core, which in turn
inserts annotations that can be recognized by Dialyzer.

22 files changed, 377 insertions, 222 deletions

diff --git a/lib/compiler/src/v3_core.erl b/lib/compiler/src/v3_core.erl
index 8c18f6a9f7..3d60992e95 100644
--- a/lib/compiler/src/v3_core.erl
+++ b/lib/compiler/src/v3_core.erl
@@ -1,7 +1,7 @@
 %%
 %% %CopyrightBegin%
 %%
-%% Copyright Ericsson AB 1999-2013. All Rights Reserved.
+%% Copyright Ericsson AB 1999-2014. All Rights Reserved.
 %%
 %% The contents of this file are subject to the Erlang Public License,
 %% Version 1.1, (the "License"); you may not use this file except in
@@ -82,6 +82,8 @@
 
 -include("core_parse.hrl").
 
+-define(REC_OFFSET, 100000000). % Also in erl_expand_records.
+
 %% Internal core expressions and help functions.
 %% N.B. annotations fields in place as normal Core expressions.
 
@@ -501,7 +503,7 @@ expr({cons,L,H0,T0}, St0) ->
     {H1,Hps,St1} = safe(H0, St0),
     {T1,Tps,St2} = safe(T0, St1),
     A = lineno_anno(L, St2),
-    {ann_c_cons(A, H1, T1),Hps ++ Tps,St2};
+    {annotate_cons(A, H1, T1, St2),Hps ++ Tps,St2};
 expr({lc,L,E,Qs0}, St0) ->
     {Qs1,St1} = preprocess_quals(L, Qs0, St0),
     lc_tq(L, E, Qs1, #c_literal{anno=lineno_anno(L, St1),val=[]}, St1);
@@ -509,8 +511,8 @@ expr({bc,L,E,Qs}, St) ->
     bc_tq(L, E, Qs, {nil,L}, St);
 expr({tuple,L,Es0}, St0) ->
     {Es1,Eps,St1} = safe_list(Es0, St0),
-    A = lineno_anno(L, St1),
-    {ann_c_tuple(A, Es1),Eps,St1};
+    A = record_anno(L, St1),
+    {annotate_tuple(A, Es1, St1),Eps,St1};
 expr({map,L,Es0}, St0) ->
     % erl_lint should make sure only #{ K => V } are allowed
     % in map construction.
@@ -1557,9 +1559,9 @@ pattern({atom,L,A}, St) -> #c_literal{anno=lineno_anno(L, St),val=A};
 pattern({string,L,S}, St) -> #c_literal{anno=lineno_anno(L, St),val=S};
 pattern({nil,L}, St) -> #c_literal{anno=lineno_anno(L, St),val=[]};
 pattern({cons,L,H,T}, St) ->
-    ann_c_cons(lineno_anno(L, St), pattern(H, St), pattern(T, St));
+    annotate_cons(lineno_anno(L, St), pattern(H, St), pattern(T, St), St);
 pattern({tuple,L,Ps}, St) ->
-    ann_c_tuple(lineno_anno(L, St), pattern_list(Ps, St));
+    annotate_tuple(record_anno(L, St), pattern_list(Ps, St), St);
 pattern({map,L,Ps}, St) ->
     #c_map{anno=lineno_anno(L, St), es=pattern_map_pairs(Ps, St)};
 pattern({bin,L,Ps}, St) ->
@@ -1721,6 +1723,26 @@ fail_clause(Pats, Anno, Arg) ->
 	     body=[#iprimop{anno=#a{anno=Anno},name=#c_literal{val=match_fail},
 			    args=[Arg]}]}.
 
+annotate_tuple(A, Es, St) ->
+    case member(annotate_records, St#core.opts) of
+        true ->
+            %% Do not coalesce constant tuple elements. A Hack.
+            Node = cerl:ann_c_tuple(A, [cerl:c_var(any)]),
+            cerl:update_c_tuple_skel(Node, Es);
+        false ->
+            ann_c_tuple(A, Es)
+    end.
+
+annotate_cons(A, H, T, St) ->
+    case member(annotate_records, St#core.opts) of
+        true ->
+            %% Do not coalesce constant conses. A Hack.
+            Node= cerl:ann_c_cons(A, cerl:c_var(any), cerl:c_var(any)),
+            cerl:update_c_cons_skel(Node, H, T);
+        false ->
+            ann_c_cons(A, H, T)
+    end.
+
 ubody(B, St) -> uexpr(B, [], St).
 
 %% uclauses([Lclause], [KnownVar], State) -> {[Lclause],State}.
@@ -2238,6 +2260,23 @@ bitstr_vars(Segs, Vs) ->
  		  lit_vars(V, lit_vars(S, Vs0))
 	  end, Vs, Segs).
 
+record_anno(L, St) when L >= ?REC_OFFSET ->
+    case member(annotate_records, St#core.opts) of
+        true ->
+            [record | lineno_anno(L - ?REC_OFFSET, St)];
+        false ->
+            lineno_anno(L, St)
+    end;
+record_anno(L, St) when L < -?REC_OFFSET ->
+    case member(annotate_records, St#core.opts) of
+        true ->
+            [record | lineno_anno(L + ?REC_OFFSET, St)];
+        false ->
+            lineno_anno(L, St)
+    end;
+record_anno(L, St) ->
+    lineno_anno(L, St).
+
 lineno_anno(L, St) ->
     {line, Line} = erl_parse:get_attribute(L, line),
     if
diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index e0873b17f8..92aab68ad6 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -53,7 +53,7 @@
 	 t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_bitstr_match/2,
 	 t_cons/0, t_cons/2, t_cons_hd/2, t_cons_tl/2,
          t_contains_opaque/2,
-	 t_find_opaque_mismatch/2, t_float/0, t_from_range/2, t_from_term/1,
+	 t_find_opaque_mismatch/3, t_float/0, t_from_range/2, t_from_term/1,
 	 t_fun/0, t_fun/2, t_fun_args/1, t_fun_args/2, t_fun_range/1,
 	 t_fun_range/2, t_integer/0, t_integers/1,
 	 t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_any_atom/3,
@@ -136,11 +136,10 @@
 
 get_warnings(Tree, Plt, Callgraph, Records, NoWarnUnused) ->
   State1 = analyze_module(Tree, Plt, Callgraph, Records, true),
-  State2 = find_mismatched_record_patterns(Tree, State1),
-  State3 =
-    state__renew_warnings(state__get_warnings(State2, NoWarnUnused), State2),
-  State4 = state__get_race_warnings(State3),
-  {State4#state.warnings, state__all_fun_types(State4)}.
+  State2 =
+    state__renew_warnings(state__get_warnings(State1, NoWarnUnused), State1),
+  State3 = state__get_race_warnings(State2),
+  {State3#state.warnings, state__all_fun_types(State3)}.
 
 -spec get_fun_types(cerl:c_module(), dialyzer_plt:plt(),
                     dialyzer_callgraph:callgraph(),
@@ -277,13 +276,8 @@ traverse(Tree, Map, State) ->
       {State1, Map1} = lists:foldl(FoldFun, {State, Map}, Defs),
       traverse(Body, Map1, State1);
     literal ->
-      %% This is needed for finding records
-      case cerl:unfold_literal(Tree) of
-	Tree ->
-	  Type = literal_type(Tree),
-	  {State, Map, Type};
-	NewTree -> traverse(NewTree, Map, State)
-      end;
+      Type = literal_type(Tree),
+      {State, Map, Type};
     module ->
       handle_module(Tree, Map, State);
     primop ->
@@ -1110,7 +1104,7 @@ handle_tuple(Tree, Map, State) ->
       %% Let's find out if this is a record
       case Elements of
 	[Tag|Left] ->
-	  case cerl:is_c_atom(Tag) of
+	  case cerl:is_c_atom(Tag) andalso is_literal_record(Tree) of
 	    true ->
 	      TagVal = cerl:atom_val(Tag),
               case state__lookup_record(TagVal, length(Left), State1) of
@@ -1240,15 +1234,10 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map, State) ->
         false ->
           {State1, Map, t_none(), ArgType0};
 	true ->
-	  PatString =
-	    case ErrorType of
-	      bind   -> format_patterns(Pats);
-	      record -> format_patterns(Pats);
-	      opaque -> format_patterns(NewPats)
-	    end,
 	  {Msg, Force} =
 	    case t_is_none(ArgType0) of
 	      true ->
+                PatString = format_patterns(Pats),
 		PatTypes = [PatString, format_type(OrigArgType, State1)],
 		%% See if this is covered by an earlier clause or if it
 		%% simply cannot match
@@ -1298,6 +1287,12 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map, State) ->
 		    false ->
 		      true
 		  end,
+                PatString =
+                  case ErrorType of
+                    bind   -> format_patterns(Pats);
+                    record -> format_patterns(NewPats);
+                    opaque -> format_patterns(NewPats)
+                  end,
 		PatTypes = case ErrorType of
 			     bind -> [PatString, format_type(ArgType0, State1)];
 			     record -> [PatString, format_type(Type, State1)];
@@ -1444,7 +1439,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	    BinType = t_inf(t_bitstr(), Type, Opaques),
 	    case t_is_none(BinType) of
 	      true ->
-                case t_find_opaque_mismatch(t_bitstr(), Type) of
+                case t_find_opaque_mismatch(t_bitstr(), Type, Opaques) of
                   {ok, T1, T2}  ->
                     bind_error([Pat], T1, T2, opaque);
                   error ->
@@ -1460,7 +1455,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	Cons = t_inf(Type, t_cons(), Opaques),
 	case t_is_none(Cons) of
 	  true ->
-	    bind_opaque_pats(t_cons(), Type, Pat, Map, State, Rev);
+	    bind_opaque_pats(t_cons(), Type, Pat, State);
 	  false ->
 	    {Map1, [HdType, TlType]} =
 	      bind_pat_vars([cerl:cons_hd(Pat), cerl:cons_tl(Pat)],
@@ -1473,7 +1468,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	Literal = literal_type(Pat),
 	case t_is_none(t_inf(Literal, Type, Opaques)) of
 	  true ->
-	    bind_opaque_pats(Literal, Type, Pat, Map, State, Rev);
+	    bind_opaque_pats(Literal, Type, Pat, State);
 	  false -> {Map, Literal}
 	end;
       map ->
@@ -1484,7 +1479,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	  case Es of
 	    [] -> {false, t_tuple([])};
 	    [Tag|Left] ->
-	      case cerl:is_c_atom(Tag) of
+	      case cerl:is_c_atom(Tag) andalso is_literal_record(Pat) of
 		true ->
 		  TagAtom = cerl:atom_val(Tag),
 		  case state__lookup_record(TagAtom, length(Left), State) of
@@ -1500,7 +1495,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	Tuple = t_inf(Prototype, Type, Opaques),
 	case t_is_none(Tuple) of
 	  true ->
-	    bind_opaque_pats(Prototype, Type, Pat, Map, State, Rev);
+	    bind_opaque_pats(Prototype, Type, Pat, State);
 	  false ->
 	    SubTuples = t_tuple_subtypes(Tuple, Opaques),
 	    %% Need to call the top function to get the try-catch wrapper
@@ -1549,7 +1544,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	VarType2 = t_inf(VarType1, Type, Opaques),
 	case t_is_none(VarType2) of
 	  true ->
-	    case t_find_opaque_mismatch(VarType1, Type) of
+	    case t_find_opaque_mismatch(VarType1, Type, Opaques) of
 	      {ok, T1, T2}  ->
 		bind_error([Pat], T1, T2, opaque);
 	      error ->
@@ -1631,21 +1626,26 @@ bind_bin_segs([Seg|Segs], BinType, Acc, Map, State) ->
 bind_bin_segs([], _BinType, Acc, Map, _State) ->
   {Map, lists:reverse(Acc)}.
 
-bind_error(Pats, Type, OpaqueType, Error) ->
+bind_error(Pats, Type, OpaqueType, Error0) ->
+  Error = case {Error0, Pats} of
+            {bind, [Pat]} ->
+              case is_literal_record(Pat) of
+                true -> record;
+                false -> Error0
+              end;
+            _ -> Error0
+          end,
   throw({error, Error, Pats, Type, OpaqueType}).
 
-bind_opaque_pats(GenType, Type, Pat, Map, State, Rev) ->
-  case t_find_opaque_mismatch(GenType, Type) of
+-spec bind_opaque_pats(type(), type(), cerl:c_literal(), state()) ->
+                          no_return().
+
+bind_opaque_pats(GenType, Type, Pat, State) ->
+  case t_find_opaque_mismatch(GenType, Type, State#state.opaques) of
     {ok, T1, T2}  ->
-      case erl_types:is_opaque_type(T2, State#state.opaques) of
-	true ->
-	  NewType = erl_types:t_struct_from_opaque(Type, [T2]),
-	  {Map1, _} =
-	    bind_pat_vars([Pat], [NewType], [], Map, State, Rev),
-	  {Map1, T2};
-	false -> bind_error([Pat], T1, T2, opaque)
-      end;
-    error -> bind_error([Pat], Type, t_none(), bind)
+	bind_error([Pat], T1, T2, opaque);
+    error ->
+      bind_error([Pat], Type, t_none(), bind)
   end.
 
 %%----------------------------------------
@@ -1843,9 +1843,9 @@ handle_guard_comp(Guard, Comp, Map, Env, Eval, State) ->
   [Type1, Type2] = ArgTypes,
   IsInt1 = t_is_integer(Type1, Opaques),
   IsInt2 = t_is_integer(Type2, Opaques),
-  case {cerl:type(Arg1), cerl:type(Arg2)} of
-    {literal, literal} ->
-      case erlang:Comp(cerl:concrete(Arg1), cerl:concrete(Arg2)) of
+  case {type(Arg1), type(Arg2)} of
+    {{literal, Lit1}, {literal, Lit2}} ->
+      case erlang:Comp(cerl:concrete(Lit1), cerl:concrete(Lit2)) of
 	true  when Eval =:= pos ->       {Map, t_atom(true)};
 	true  when Eval =:= dont_know -> {Map, t_atom(true)};
 	true  when Eval =:= neg ->       {Map, t_atom(true)};
@@ -1854,13 +1854,13 @@ handle_guard_comp(Guard, Comp, Map, Env, Eval, State) ->
 	false when Eval =:= dont_know -> {Map, t_atom(false)};
 	false when Eval =:= neg ->       {Map, t_atom(false)}
       end;
-    {literal, var} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
-      case bind_comp_literal_var(Arg1, Arg2, Type2, Comp, Map1, Opaques) of
+    {{literal, Lit1}, var} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
+      case bind_comp_literal_var(Lit1, Arg2, Type2, Comp, Map1, Opaques) of
 	error -> signal_guard_fail(Eval, Guard, ArgTypes, State);
 	{ok, NewMap} -> {NewMap, t_atom(true)}
       end;
-    {var, literal} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
-      case bind_comp_literal_var(Arg2, Arg1, Type1, invert_comp(Comp),
+    {var, {literal, Lit2}} when IsInt1 andalso IsInt2 andalso (Eval =:= pos) ->
+      case bind_comp_literal_var(Lit2, Arg1, Type1, invert_comp(Comp),
                                  Map1, Opaques) of
 	error -> signal_guard_fail(Eval, Guard, ArgTypes, State);
 	{ok, NewMap} -> {NewMap, t_atom(true)}
@@ -1980,15 +1980,15 @@ handle_guard_is_record(Guard, Map, Env, Eval, State) ->
 
 handle_guard_eq(Guard, Map, Env, Eval, State) ->
   [Arg1, Arg2] = cerl:call_args(Guard),
-  case {cerl:type(Arg1), cerl:type(Arg2)} of
-    {literal, literal} ->
-      case cerl:concrete(Arg1) =:= cerl:concrete(Arg2) of
+  case {type(Arg1), type(Arg2)} of
+    {{literal, Lit1}, {literal, Lit2}} ->
+      case cerl:concrete(Lit1) =:= cerl:concrete(Lit2) of
 	true ->
 	  if
 	    Eval =:= pos -> {Map, t_atom(true)};
 	    Eval =:= neg ->
-	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
-			  t_from_term(cerl:concrete(Arg2))],
+	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
+			  t_from_term(cerl:concrete(Lit2))],
 	      signal_guard_fail(Eval, Guard, ArgTypes, State);
 	    Eval =:= dont_know -> {Map, t_atom(true)}
 	  end;
@@ -1997,28 +1997,28 @@ handle_guard_eq(Guard, Map, Env, Eval, State) ->
 	    Eval =:= neg -> {Map, t_atom(false)};
 	    Eval =:= dont_know -> {Map, t_atom(false)};
 	    Eval =:= pos ->
-	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
-			  t_from_term(cerl:concrete(Arg2))],
+	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
+			  t_from_term(cerl:concrete(Lit2))],
 	      signal_guard_fail(Eval, Guard, ArgTypes, State)
 	  end
       end;
-    {literal, _} when Eval =:= pos ->
-      case cerl:concrete(Arg1) of
+    {{literal, Lit1}, _} when Eval =:= pos ->
+      case cerl:concrete(Lit1) of
 	Atom when is_atom(Atom) ->
-	  bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State);
+	  bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
 	[] ->
-	  bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State);
+	  bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
 	_ ->
-	  bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
+	  bind_eq_guard(Guard, Lit1, Arg2, Map, Env, Eval, State)
       end;
-    {_, literal} when Eval =:= pos ->
-      case cerl:concrete(Arg2) of
+    {_, {literal, Lit2}} when Eval =:= pos ->
+      case cerl:concrete(Lit2) of
 	Atom when is_atom(Atom) ->
-	  bind_eqeq_guard_lit_other(Guard, Arg2, Arg1, Map, Env, State);
+	  bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
 	[] ->
-	  bind_eqeq_guard_lit_other(Guard, Arg2, Arg1, Map, Env, State);
+	  bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
 	_ ->
-	  bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
+	  bind_eq_guard(Guard, Arg1, Lit2, Map, Env, Eval, State)
       end;
     {_, _} ->
       bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
@@ -2050,13 +2050,14 @@ bind_eq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) ->
 
 handle_guard_eqeq(Guard, Map, Env, Eval, State) ->
   [Arg1, Arg2] = cerl:call_args(Guard),
-  case {cerl:type(Arg1), cerl:type(Arg2)} of
-    {literal, literal} ->
-      case cerl:concrete(Arg1) =:= cerl:concrete(Arg2) of
+  case {type(Arg1), type(Arg2)} of
+    {{literal, Lit1}, {literal, Lit2}} ->
+
+      case cerl:concrete(Lit1) =:= cerl:concrete(Lit2) of
 	true ->
 	  if Eval =:= neg ->
-	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
-			  t_from_term(cerl:concrete(Arg2))],
+	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
+			  t_from_term(cerl:concrete(Lit2))],
 	      signal_guard_fail(Eval, Guard, ArgTypes, State);
 	     Eval =:= pos -> {Map, t_atom(true)};
 	     Eval =:= dont_know -> {Map, t_atom(true)}
@@ -2065,15 +2066,15 @@ handle_guard_eqeq(Guard, Map, Env, Eval, State) ->
 	  if Eval =:= neg -> {Map, t_atom(false)};
 	     Eval =:= dont_know -> {Map, t_atom(false)};
 	     Eval =:= pos ->
-	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
-			  t_from_term(cerl:concrete(Arg2))],
+	      ArgTypes = [t_from_term(cerl:concrete(Lit1)),
+			  t_from_term(cerl:concrete(Lit2))],
 	      signal_guard_fail(Eval, Guard, ArgTypes, State)
 	  end
       end;
-    {literal, _} when Eval =:= pos ->
-      bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State);
-    {_, literal} when Eval =:= pos ->
-      bind_eqeq_guard_lit_other(Guard, Arg2, Arg1, Map, Env, State);
+    {{literal, Lit1}, _} when Eval =:= pos ->
+      bind_eqeq_guard_lit_other(Guard, Lit1, Arg2, Map, Env, State);
+    {_, {literal, Lit2}} when Eval =:= pos ->
+      bind_eqeq_guard_lit_other(Guard, Lit2, Arg1, Map, Env, State);
     {_, _} ->
       bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State)
   end.
@@ -3282,12 +3283,17 @@ get_file([_|Tail]) -> get_file(Tail).
 is_compiler_generated(Ann) ->
   lists:member(compiler_generated, Ann) orelse (get_line(Ann) < 1).
 
+is_literal_record(Tree) ->
+  Ann = cerl:get_ann(Tree),
+  lists:member(record, Ann).
+
 -spec format_args([cerl:cerl()], [type()], state()) ->
   nonempty_string().
 
 format_args([], [], _State) ->
   "()";
-format_args(ArgList, TypeList, State) ->
+format_args(ArgList0, TypeList, State) ->
+  ArgList = fold_literals(ArgList0),
   "(" ++ format_args_1(ArgList, TypeList, State) ++ ")".
 
 format_args_1([Arg], [Type], State) ->
@@ -3346,7 +3352,8 @@ format_cerl(Tree) ->
 			{ribbon, 100000} %% newlines.
 		       ]).
 
-format_patterns(Pats) ->
+format_patterns(Pats0) ->
+  Pats = fold_literals(Pats0),
   NewPats = map_pats(cerl:c_values(Pats)),
   String = format_cerl(NewPats),
   case Pats of
@@ -3378,6 +3385,23 @@ map_pats(Pats) ->
 	end,
   cerl_trees:map(Fun, Pats).
 
+fold_literals(TreeList) ->
+  [cerl:fold_literal(Tree) || Tree <- TreeList].
+
+type(Tree) ->
+  Folded = cerl:fold_literal(Tree),
+  case cerl:type(Folded) of
+    literal -> {literal, Folded};
+    Type -> Type
+  end.
+
+is_literal(Tree) ->
+  Folded = cerl:fold_literal(Tree),
+  case cerl:is_literal(Folded) of
+    true -> {yes, Folded};
+    false -> no
+  end.
+
 parent_allows_this(FunLbl, #state{callgraph = Callgraph, plt = Plt} =State) ->
   case state__is_escaping(FunLbl, State) of
     false -> false; % if it isn't escaping it can't be a return value
@@ -3422,18 +3446,18 @@ find_terminals(Tree) ->
       M0 = cerl:call_module(Tree),
       F0 = cerl:call_name(Tree),
       A = length(cerl:call_args(Tree)),
-      case cerl:is_literal(M0) andalso cerl:is_literal(F0) of
-	false ->
-	  %% We cannot make assumptions. Say that both are true.
-	  {true, true};
-	true ->
-	  M = cerl:concrete(M0),
-	  F = cerl:concrete(F0),
+      case {is_literal(M0), is_literal(F0)} of
+        {{yes, LitM}, {yes, LitF}} ->
+	  M = cerl:concrete(LitM),
+	  F = cerl:concrete(LitF),
 	  case (erl_bif_types:is_known(M, F, A)
 		andalso t_is_none(erl_bif_types:type(M, F, A))) of
 	    true -> {true, false};
 	    false -> {false, true}
-	  end
+	  end;
+        _ ->
+	  %% We cannot make assumptions. Say that both are true.
+	  {true, true}
       end;
     'case' -> find_terminals_list(cerl:case_clauses(Tree));
     'catch' -> find_terminals(cerl:catch_body(Tree));
@@ -3478,66 +3502,6 @@ find_terminals_list([], Explicit, Normal) ->
 
 %%----------------------------------------------------------------------------
 
-%% If you write a record pattern in a matching that violates the
-%% definition it will never match. However, the warning is lost in the
-%% regular analysis. This after-pass catches it.
-
-find_mismatched_record_patterns(Tree, State) ->
-  cerl_trees:fold(
-    fun(SubTree, AccState) ->
-	case cerl:is_c_clause(SubTree) of
-	  true -> lists:foldl(fun(P, AccState1) ->
-				  find_rec_warnings(P, AccState1)
-			      end, AccState, cerl:clause_pats(SubTree));
-	  false -> AccState
-	end
-    end, State, Tree).
-
-find_rec_warnings(Tree, State) ->
-  cerl_trees:fold(
-    fun(SubTree, AccState) ->
-	case cerl:is_c_tuple(SubTree) of
-	  true -> find_rec_warnings_tuple(SubTree, AccState);
-	  false -> AccState
-	end
-    end, State, Tree).
-
-find_rec_warnings_tuple(Tree, State) ->
-  Elements = cerl:tuple_es(Tree),
-  {_, _, EsType} = traverse_list(Elements, map__new(), State),
-  TupleType = t_tuple(EsType),
-  case t_is_none(TupleType) of
-    true -> State;
-    false ->
-      %% Let's find out if this is a record construction.
-      case Elements of
-	[Tag|Left] ->
-	  case cerl:is_c_atom(Tag) of
-	    true ->
-	      TagVal = cerl:atom_val(Tag),
-	      case state__lookup_record(TagVal, length(Left), State) of
-		error -> State;
-		{ok, Prototype} ->
-		  InfTupleType = t_inf(Prototype, TupleType),
-		  case t_is_none(InfTupleType) of
-		    true ->
-		      Msg = {record_matching,
-			     [format_patterns([Tree]), TagVal]},
-		      state__add_warning(State, ?WARN_MATCHING, Tree, Msg);
-		    false ->
-		      State
-		  end
-	      end;
-	    false ->
-	      State
-	  end;
-	_ ->
-	  State
-      end
-  end.
-
-%%----------------------------------------------------------------------------
-
 -ifdef(DEBUG_PP).
 debug_pp(Tree, true) ->
   io:put_chars(cerl_prettypr:format(Tree, [{hook, cerl_typean:pp_hook()}])),
diff --git a/lib/dialyzer/src/dialyzer_races.erl b/lib/dialyzer/src/dialyzer_races.erl
index 28c2ad2c0b..2a8aba5d8f 100644
--- a/lib/dialyzer/src/dialyzer_races.erl
+++ b/lib/dialyzer/src/dialyzer_races.erl
@@ -1848,7 +1848,8 @@ ets_tuple_argtypes1(Str, Tuple, TupleList, NestingLevel) ->
   end.
 
 format_arg(?bypassed) -> ?no_label;
-format_arg(Arg) ->
+format_arg(Arg0) ->
+  Arg = cerl:fold_literal(Arg0),
   case cerl:type(Arg) of
     var -> cerl_trees:get_label(Arg);
     tuple -> list_to_tuple([format_arg(A) || A <- cerl:tuple_es(Arg)]);
@@ -1878,7 +1879,7 @@ format_args_1([Arg|Args], [Type|Types], CleanState) ->
     case Arg =:= ?bypassed of
       true -> [?no_label, format_type(Type, CleanState)];
       false ->
-        case cerl:is_literal(Arg) of
+        case cerl:is_literal(cerl:fold_literal(Arg)) of
           true -> [?no_label, format_cerl(Arg)];
           false -> [format_arg(Arg), format_type(Type, CleanState)]
         end
@@ -2148,7 +2149,8 @@ race_var_map_guard_helper1(Arg, Pats, RaceVarMap, Op) ->
       end
   end.
 
-race_var_map_guard_helper2(Arg, Pat, Bool, RaceVarMap, Op) ->
+race_var_map_guard_helper2(Arg, Pat0, Bool, RaceVarMap, Op) ->
+  Pat = cerl:fold_literal(Pat0),
   case cerl:type(Pat) of
     literal ->
       [Arg1, Arg2] = cerl:call_args(Arg),
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 31ceaf5ac5..3d03ed3ab3 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -389,13 +389,8 @@ traverse(Tree, DefinedVars, State) ->
       {State2, _} = traverse_list(Funs, DefinedVars1, State1),
       traverse(Body, DefinedVars1, State2);
     literal ->
-      %% This is needed for finding records
-      case cerl:unfold_literal(Tree) of
-	Tree ->
-	  Type = t_from_term(cerl:concrete(Tree)),
-	  {State, Type};
-	NewTree -> traverse(NewTree, DefinedVars, State)
-      end;
+      Type = t_from_term(cerl:concrete(Tree)),
+      {State, Type};
     module ->
       Defs = cerl:module_defs(Tree),
       Funs = [Fun || {_Var, Fun} <- Defs],
@@ -462,7 +457,7 @@ traverse(Tree, DefinedVars, State) ->
 	end,
       case Elements of
 	[Tag|Fields] ->
-	  case cerl:is_c_atom(Tag) of
+	  case cerl:is_c_atom(Tag) andalso is_literal_record(Tree) of
 	    true ->
               %% Check if a record is constructed.
               Arity = length(Fields),
@@ -874,7 +869,8 @@ get_underapprox_from_guard(Tree, Map) ->
 	MFA ->
 	  case get_type_test(MFA) of
 	    {ok, Type} ->
-	      [Arg] = cerl:call_args(Tree),
+	      [Arg0] = cerl:call_args(Tree),
+              Arg = cerl:fold_literal(Arg0),
 	      {ArgType, Map1} = get_underapprox_from_guard(Arg, Map),
 	      Inf = t_inf(Type, ArgType),
 	      case t_is_none(Inf) of
@@ -891,7 +887,9 @@ get_underapprox_from_guard(Tree, Map) ->
 		{erlang, '=:=', 2} -> throw(dont_know);
 		{erlang, '==', 2} -> throw(dont_know);
 		{erlang, 'and', 2} ->
-		  [Arg1, Arg2] = cerl:call_args(Tree),
+		  [Arg1_0, Arg2_0] = cerl:call_args(Tree),
+                  Arg1 = cerl:fold_literal(Arg1_0),
+                  Arg2 = cerl:fold_literal(Arg2_0),
 		  case ((cerl:is_c_var(Arg1) orelse cerl:is_literal(Arg1))
 			andalso
 			(cerl:is_c_var(Arg2) orelse cerl:is_literal(Arg2))) of
@@ -3272,6 +3270,10 @@ lookup_record(Records, Tag, Arity) ->
       error
   end.
 
+is_literal_record(Tree) ->
+  Ann = cerl:get_ann(Tree),
+  lists:member(record, Ann).
+
 family(L) ->
     sofs:to_external(sofs:rel2fam(sofs:relation(L))).
 
diff --git a/lib/dialyzer/src/dialyzer_utils.erl b/lib/dialyzer/src/dialyzer_utils.erl
index 21183e3459..2eba68322b 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -402,7 +402,9 @@ sets_filter([Mod|Mods], ExpTypes) ->
 src_compiler_opts() ->
   [no_copt, to_core, binary, return_errors,
    no_inline, strict_record_tests, strict_record_updates,
-   no_is_record_optimization].
+   %% The following could be coalesced into one Dialyzer specific option.
+   no_is_record_optimization,
+   annotate_records].
 
 -spec get_module(abstract_code()) -> module().
 
diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/simple b/lib/dialyzer/test/opaque_SUITE_data/results/simple
index 072ac9be8f..29864d6065 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/simple
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/simple
@@ -14,12 +14,17 @@ is_rec.erl:53: The call erlang:is_record(A::simple1_adt:d1(),A::simple1_adt:d1()
 is_rec.erl:57: Guard test is_record(A::simple1_adt:d1(),'r',2) breaks the opaqueness of its argument
 is_rec.erl:61: The record #r{f1::simple1_adt:d1()} violates the declared type for #r{}
 is_rec.erl:65: The call erlang:is_record({simple1_adt:d1(),1},'r',2) contains an opaque term as 1st argument when terms of different types are expected in these positions
-rec_api.erl:22: Record construction #r1{f1::10} violates the declared type of field f1::'undefined' | rec_api:a()
-rec_api.erl:23: The pattern {'r1', 10} violates the declared type for #r1{}
-rec_api.erl:27: The attempt to match a term of type rec_adt:r1() against the pattern {'r1', 'a'} breaks the opaqueness of the term
-rec_api.erl:29: Invalid type specification for function rec_api:adt_t1/1. The success typing is (#r1{f1::'a'}) -> #r1{f1::'a'}
-rec_api.erl:34: Invalid type specification for function rec_api:adt_r1/0. The success typing is () -> #r1{f1::'a'}
-rec_api.erl:77: The attempt to match a term of type rec_api:f() against the variable _ breaks the opaqueness of the term
+rec_api.erl:104: Matching of pattern {'r2', 10} tagged with a record name violates the declared type of #r2{f1::10}
+rec_api.erl:113: The attempt to match a term of type #r3{f1::queue:queue(_)} against the pattern {'r3', 'a'} breaks the opaqueness of queue:queue(_)
+rec_api.erl:118: Record construction #r3{f1::10} violates the declared type of field f1::queue:queue(_)
+rec_api.erl:123: The attempt to match a term of type #r3{f1::10} against the pattern {'r3', 10} breaks the opaqueness of queue:queue(_)
+rec_api.erl:24: Record construction #r1{f1::10} violates the declared type of field f1::'undefined' | rec_api:a()
+rec_api.erl:29: Matching of pattern {'r1', 10} tagged with a record name violates the declared type of #r1{f1::10}
+rec_api.erl:33: The attempt to match a term of type rec_adt:r1() against the pattern {'r1', 'a'} breaks the opaqueness of the term
+rec_api.erl:35: Invalid type specification for function rec_api:adt_t1/1. The success typing is (#r1{f1::'a'}) -> #r1{f1::'a'}
+rec_api.erl:40: Invalid type specification for function rec_api:adt_r1/0. The success typing is () -> #r1{f1::'a'}
+rec_api.erl:85: The attempt to match a term of type rec_api:f() against the variable _ breaks the opaqueness of rec_adt:f()
+rec_api.erl:99: Record construction #r2{f1::10} violates the declared type of field f1::rec_api:a()
 simple1_api.erl:113: The test simple1_api:d1() =:= simple1_api:d2() can never evaluate to 'true'
 simple1_api.erl:118: Guard test simple1_api:d2() =:= A::simple1_api:d1() can never succeed
 simple1_api.erl:142: Attempt to test for equality between a term of type simple1_adt:o2() and a term of opaque type simple1_adt:o1()
@@ -58,7 +63,7 @@ simple1_api.erl:381: Invalid type specification for function simple1_api:bool_ad
 simple1_api.erl:407: The size simple1_adt:i1() breaks the opaqueness of A
 simple1_api.erl:418: The attempt to match a term of type non_neg_integer() against the variable A breaks the opaqueness of simple1_adt:i1()
 simple1_api.erl:425: The attempt to match a term of type non_neg_integer() against the variable B breaks the opaqueness of simple1_adt:i1()
-simple1_api.erl:432: The attempt to match a term of type non_neg_integer() against the variable B breaks the opaqueness of simple1_api:o1()
+simple1_api.erl:432: The pattern <<_:B/integer-unit:1>> can never match the type any()
 simple1_api.erl:448: The attempt to match a term of type non_neg_integer() against the variable Sz breaks the opaqueness of simple1_adt:i1()
 simple1_api.erl:460: The attempt to match a term of type simple1_adt:bit1() against the pattern <<_/binary-unit:8>> breaks the opaqueness of the term
 simple1_api.erl:478: The call 'foo':A(A::simple1_adt:a()) breaks the opaqueness of the term A :: simple1_adt:a()
diff --git a/lib/dialyzer/test/opaque_SUITE_data/results/timer b/lib/dialyzer/test/opaque_SUITE_data/results/timer
index e917b76b08..b1cfcd4e9f 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/results/timer
+++ b/lib/dialyzer/test/opaque_SUITE_data/results/timer
@@ -1,4 +1,4 @@
 
 timer_use.erl:16: The pattern 'gazonk' can never match the type {'error',_} | {'ok',timer:tref()}
-timer_use.erl:17: The attempt to match a term of type {'ok',timer:tref()} against the pattern {'ok', 42} breaks the opaqueness of timer:tref()
+timer_use.erl:17: The attempt to match a term of type {'error',_} | {'ok',timer:tref()} against the pattern {'ok', 42} breaks the opaqueness of timer:tref()
 timer_use.erl:18: The attempt to match a term of type {'error',_} | {'ok',timer:tref()} against the pattern {Tag, 'gazonk'} breaks the opaqueness of timer:tref()
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl
index d9b1d59f0c..fb6d59d263 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/rec_api.erl
@@ -1,9 +1,9 @@
 -module(rec_api).
 
--export([t1/0, t2/0, adt_t1/0, adt_t1/1, adt_r1/0,
-         t/1, t_adt/0, r/0, r_adt/0]).
+-export([t1/0, t2/0, t3/0, adt_t1/0, adt_t1/1, adt_r1/0,
+         t/1, t_adt/0, r/0, r_adt/0, u1/0, u2/0, u3/0, v1/0, v2/0, v3/0]).
 
--export_type([{a,0},{r1,0}]).
+-export_type([{a,0},{r1,0}, r2/0, r3/0]).
 
 -export_type([f/0, op_t/0, r/0, tup/0]).
 
@@ -19,8 +19,14 @@ t1() ->
     {r1, a} = A.
 
 t2() ->
-    A = {r1, 10}, % violates the type of #r1{}
-    {r1, 10} = A. % violates the type of #r1{}
+    A = {r1, 10},
+    {r1, 10} = A,
+    A = #r1{f1 = 10}, % violates the type of field f1
+    #r1{f1 = 10} = A.
+
+t3() ->
+    A = {r1, 10},
+    #r1{f1 = 10} = A. % violates the type of #r1{}
 
 adt_t1() ->
     R = rec_adt:r1(),
@@ -66,7 +72,8 @@ t_adt() ->
 -spec r() -> _.
 
 r() ->
-    {r, f(), 2}. % OK, f() is a local opaque type
+    {{r, f(), 2},
+     #r{f = f(), o = 2}}. % OK, f() is a local opaque type
 
 -spec f() -> f().
 
@@ -74,4 +81,43 @@ f() ->
     fun(_) -> 3 end.
 
 r_adt() ->
-    {r, rec_adt:f(), 2}. % breaks the opaqueness
+    {{r, rec_adt:f(), 2},
+     #r{f = rec_adt:f(), o = 2}}. % breaks the opaqueness
+
+-record(r2, % like #r1{}, but with initial value
+        {f1 = a :: a()}).
+
+-opaque r2() :: #r2{}.
+
+u1() ->
+    A = #r2{f1 = a},
+    {r2, a} = A.
+
+u2() ->
+    A = {r2, 10},
+    {r2, 10} = A,
+    A = #r2{f1 = 10}, % violates the type of field f1
+    #r2{f1 = 10} = A.
+
+u3() ->
+    A = {r2, 10},
+    #r2{f1 = 10} = A. % violates the type of #r2{}
+
+-record(r3, % like #r1{}, but an opaque type
+        {f1 = queue:new():: queue:queue()}).
+
+-opaque r3() :: #r3{}.
+
+v1() ->
+    A = #r3{f1 = queue:new()},
+    {r3, a} = A. % breaks the opaqueness
+
+v2() ->
+    A = {r3, 10},
+    {r3, 10} = A,
+    A = #r3{f1 = 10}, % violates the type of field f1
+    #r3{f1 = 10} = A.
+
+v3() ->
+    A = {r3, 10},
+    #r3{f1 = 10} = A. % breaks the opaqueness
diff --git a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
index 5135eb8e59..eef2074e0c 100644
--- a/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
+++ b/lib/dialyzer/test/opaque_SUITE_data/src/simple/simple1_api.erl
@@ -428,8 +428,8 @@ bit_adt_t3(A) ->
 
 bit_t5(A) ->
     B = o1(),
-    case none:none() of
-        <<A:B>> -> 1 % breaks the opaqueness
+    case none:none() of % the type is any(); should fix that XXX
+        <<A:B>> -> 1 % can never match (local opaque type is OK)
     end.
 
 -spec bit_t4(<<_:1>>) -> integer().
diff --git a/lib/dialyzer/test/options1_SUITE_data/results/compiler b/lib/dialyzer/test/options1_SUITE_data/results/compiler
index 6399e3e36b..30b6f4814a 100644
--- a/lib/dialyzer/test/options1_SUITE_data/results/compiler
+++ b/lib/dialyzer/test/options1_SUITE_data/results/compiler
@@ -4,7 +4,7 @@ beam_bool.erl:193: The pattern {[], _} can never match the type {[{_,_,_,_},...]
 beam_bool.erl:510: The pattern [{'set', [Dst], _, _}, {'%live', _}] can never match the type [{_,_,_,_}]
 beam_disasm.erl:537: The variable X can never match since previous clauses completely covered the type 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7
 beam_type.erl:284: The pattern <'pi', 0> can never match the type <_,1 | 2>
-beam_validator.erl:396: The pattern <{'jump', {'f', _}}, Vst = {'vst', 'none', _}> can never match the type <_,#vst{current::#st{ct::[]}}>
+beam_validator.erl:396: Matching of pattern {'vst', 'none', _} tagged with a record name violates the declared type of #vst{current::#st{ct::[]}}
 beam_validator.erl:690: The pattern <'term', OldT> can never match the type <{'tuple',[any(),...]},_>
 beam_validator.erl:693: Guard test 'or'('false','false') can never succeed
 beam_validator.erl:700: Guard test 'or'('false','false') can never succeed
@@ -33,4 +33,4 @@ core_lint.erl:473: The pattern <{'c_atom', _, 'all'}, 'binary', _Def, St> can ne
 core_lint.erl:505: The pattern <_Req, 'unknown', St> can never match the type <non_neg_integer(),non_neg_integer(),_>
 v3_codegen.erl:1569: The call v3_codegen:load_reg_1(V::any(),I::0,Rs::any(),pos_integer()) will never return since it differs in the 4th argument from the success typing arguments: (any(),0,maybe_improper_list(),0)
 v3_codegen.erl:1571: The call v3_codegen:load_reg_1(V::any(),I::0,[],pos_integer()) will never return since it differs in the 4th argument from the success typing arguments: (any(),0,maybe_improper_list(),0)
-v3_core.erl:646: The pattern <Prim = {'iprimop', _, _, _}, St> can never match the type <#c_nil{anno::[any(),...]} | {'c_atom' | 'c_char' | 'c_float' | 'c_int' | 'c_string' | 'c_tuple' | 'c_var' | 'ibinary' | 'icatch' | 'ireceive1',[any(),...] | {_,_,_,_},_} | #c_cons{anno::[any(),...]} | #c_fname{anno::[any(),...]} | #iletrec{anno::{_,_,_,_},defs::[any(),...],body::[any(),...]} | #icase{anno::{_,_,_,_},args::[any()],clauses::[any()],fc::{_,_,_,_,_,_}} | #ireceive2{anno::{_,_,_,_},clauses::[any()],action::[any()]} | #ifun{anno::{_,_,_,_},id::[any(),...],vars::[any()],clauses::[any(),...],fc::{_,_,_,_,_,_}} | #imatch{anno::{_,_,_,_},guard::[],fc::{_,_,_,_,_,_}} | #itry{anno::{_,_,_,_},args::[any()],vars::[any(),...],body::[any(),...],evars::[any(),...],handler::[any(),...]},_>
+v3_core.erl:646: Matching of pattern {'iprimop', _, _, _} tagged with a record name violates the declared type of #c_nil{anno::[any(),...]} | {'c_atom' | 'c_char' | 'c_float' | 'c_int' | 'c_string' | 'c_tuple' | 'c_var' | 'ibinary' | 'icatch' | 'ireceive1',[any(),...] | {_,_,_,_},_} | #c_cons{anno::[any(),...]} | #c_fname{anno::[any(),...]} | #iletrec{anno::{_,_,_,_},defs::[any(),...],body::[any(),...]} | #icase{anno::{_,_,_,_},args::[any()],clauses::[any()],fc::{_,_,_,_,_,_}} | #ireceive2{anno::{_,_,_,_},clauses::[any()],action::[any()]} | #ifun{anno::{_,_,_,_},id::[any(),...],vars::[any()],clauses::[any(),...],fc::{_,_,_,_,_,_}} | #imatch{anno::{_,_,_,_},guard::[],fc::{_,_,_,_,_,_}} | #itry{anno::{_,_,_,_},args::[any()],vars::[any(),...],body::[any(),...],evars::[any(),...],handler::[any(),...]}
diff --git a/lib/dialyzer/test/r9c_SUITE_data/results/asn1 b/lib/dialyzer/test/r9c_SUITE_data/results/asn1
index c11105b76d..1cf03346ee 100644
--- a/lib/dialyzer/test/r9c_SUITE_data/results/asn1
+++ b/lib/dialyzer/test/r9c_SUITE_data/results/asn1
@@ -5,7 +5,7 @@ asn1ct.erl:1673: The pattern 'all' can never match the type 'asn1_module' | 'exc
 asn1ct.erl:672: The pattern <{'false', Result}, _, _> can never match the type <{'true','true'},atom() | binary() | [atom() | [any()] | char()],[any()]>
 asn1ct.erl:909: Guard test is_atom(Ext::[49 | 97 | 98 | 100 | 110 | 115]) can never succeed
 asn1ct_check.erl:1698: The pattern {'error', _} can never match the type [any()]
-asn1ct_check.erl:2733: The pattern {'type', Tag, _, _, _, _} can never match the type 'ASN1_OPEN_TYPE' | {_,_} | {'fixedtypevaluefield',_,_}
+asn1ct_check.erl:2733: Matching of pattern {'type', Tag, _, _, _, _} tagged with a record name violates the declared type of 'ASN1_OPEN_TYPE' | {_,_} | {'fixedtypevaluefield',_,_}
 asn1ct_check.erl:2738: The pattern <_S, _> can never match since previous clauses completely covered the type <#state{},#'ObjectClassFieldType'{class::#objectclass{fields::maybe_improper_list() | {_,_,_,_}},fieldname::{_,maybe_improper_list()},type::'ASN1_OPEN_TYPE' | {_,_} | {'fixedtypevaluefield',_,_}}>
 asn1ct_check.erl:2887: The variable Other can never match since previous clauses completely covered the type any()
 asn1ct_check.erl:3188: The pattern <_S, [], B> can never match the type <#state{},{'SingleValue',_},{'ValueRange',_}>
diff --git a/lib/dialyzer/test/small_SUITE_data/results/confusing_record_warning b/lib/dialyzer/test/small_SUITE_data/results/confusing_record_warning
deleted file mode 100644
index ac3d89b02b..0000000000
--- a/lib/dialyzer/test/small_SUITE_data/results/confusing_record_warning
+++ /dev/null
@@ -1,3 +0,0 @@
-
-confusing_record_warning.erl:18: Function test/1 has no local return
-confusing_record_warning.erl:18: Matching of pattern {'r', [_]} tagged with a record name violates the declared type of #r{field::'binary' | 'undefined'}
diff --git a/lib/dialyzer/test/small_SUITE_data/results/literals b/lib/dialyzer/test/small_SUITE_data/results/literals
new file mode 100644
index 0000000000..03e161ca71
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/results/literals
@@ -0,0 +1,14 @@
+
+literals.erl:11: Function t1/0 has no local return
+literals.erl:12: Record construction #r{id::'a'} violates the declared type of field id::'integer' | 'undefined'
+literals.erl:14: Function t2/0 has no local return
+literals.erl:15: Record construction #r{id::'a'} violates the declared type of field id::'integer' | 'undefined'
+literals.erl:17: Function t3/0 has no local return
+literals.erl:18: Record construction #r{id::'a'} violates the declared type of field id::'integer' | 'undefined'
+literals.erl:21: Record construction #r{id::'a'} violates the declared type of field id::'integer' | 'undefined'
+literals.erl:23: Function m1/1 has no local return
+literals.erl:23: Matching of pattern {'r', 'a'} tagged with a record name violates the declared type of #r{id::'integer' | 'undefined'}
+literals.erl:26: Function m2/1 has no local return
+literals.erl:26: Matching of pattern {'r', 'a'} tagged with a record name violates the declared type of #r{id::'integer' | 'undefined'}
+literals.erl:29: Function m3/1 has no local return
+literals.erl:29: The pattern {{'r', 'a'}} can never match the type any()
diff --git a/lib/dialyzer/test/small_SUITE_data/results/my_sofs b/lib/dialyzer/test/small_SUITE_data/results/my_sofs
index bc97c08d62..0b933e6cd7 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/my_sofs
+++ b/lib/dialyzer/test/small_SUITE_data/results/my_sofs
@@ -1,3 +1,3 @@
 
-my_sofs.erl:34: The pattern {'Set', _, _} can never match the type #'OrdSet'{}
-my_sofs.erl:54: The pattern {'Set', _, _} can never match the type #'OrdSet'{}
+my_sofs.erl:34: Matching of pattern {'Set', _, _} tagged with a record name violates the declared type of #'OrdSet'{}
+my_sofs.erl:54: Matching of pattern {'Set', _, _} tagged with a record name violates the declared type of #'OrdSet'{}
diff --git a/lib/dialyzer/test/small_SUITE_data/results/record_pat b/lib/dialyzer/test/small_SUITE_data/results/record_pat
index 9a3f925e42..a46be6c451 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/record_pat
+++ b/lib/dialyzer/test/small_SUITE_data/results/record_pat
@@ -1,2 +1,2 @@
 
-record_pat.erl:14: The pattern {'foo', 'baz'} violates the declared type for #foo{}
+record_pat.erl:14: Matching of pattern {'foo', 'baz'} tagged with a record name violates the declared type of #foo{bar::'undefined' | integer()}
diff --git a/lib/dialyzer/test/small_SUITE_data/results/record_test b/lib/dialyzer/test/small_SUITE_data/results/record_test
index 9715f0dcfb..7060bfa200 100644
--- a/lib/dialyzer/test/small_SUITE_data/results/record_test
+++ b/lib/dialyzer/test/small_SUITE_data/results/record_test
@@ -1,3 +1,3 @@
 
-record_test.erl:19: The pattern {'foo', _} can never match the type 'foo'
+record_test.erl:19: Matching of pattern {'foo', _} tagged with a record name violates the declared type of 'foo'
 record_test.erl:21: The variable _ can never match since previous clauses completely covered the type 'foo'
diff --git a/lib/dialyzer/test/small_SUITE_data/results/relevant_record_warning b/lib/dialyzer/test/small_SUITE_data/results/relevant_record_warning
new file mode 100644
index 0000000000..2e417e1b2a
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/results/relevant_record_warning
@@ -0,0 +1,3 @@
+
+relevant_record_warning.erl:22: Function test/1 has no local return
+relevant_record_warning.erl:23: Record construction #r{field::<<_:8>>} violates the declared type of field field::'binary' | 'undefined'
diff --git a/lib/dialyzer/test/small_SUITE_data/src/fun2ms.erl b/lib/dialyzer/test/small_SUITE_data/src/fun2ms.erl
new file mode 100644
index 0000000000..9e7df85e4c
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/src/fun2ms.erl
@@ -0,0 +1,21 @@
+-module(fun2ms).
+-export([return/0]).
+-include_lib("stdlib/include/ms_transform.hrl").
+
+-record(snapshot, {id :: integer(), arg1 :: atom(), arg2 :: tuple()}).
+
+return() ->
+    TableId = ets:new(table, [public, {keypos, #snapshot.id}]),
+
+    ets:insert(TableId, [#snapshot{id = 1, arg1 = hard, arg2 = {1,2}},
+                         #snapshot{id = 2, arg1 = rock, arg2 = {1,2}},
+                         #snapshot{id = 3, arg1 = hallelujah, arg2 =
+                                       {1,2}}]),
+
+
+    Example = ets:fun2ms(
+                fun(#snapshot{id = Arg1, arg1 = Arg2}) ->
+                        {Arg1, Arg2}
+                end),
+
+    ets:select(TableId, Example).
diff --git a/lib/dialyzer/test/small_SUITE_data/src/literals.erl b/lib/dialyzer/test/small_SUITE_data/src/literals.erl
new file mode 100644
index 0000000000..abd7033712
--- /dev/null
+++ b/lib/dialyzer/test/small_SUITE_data/src/literals.erl
@@ -0,0 +1,33 @@
+-module(literals).
+
+%% Bad records inside structures used to be ignored. The reason:
+%% v3_core:unfold() does not annotate the parts of a literal.
+%% This example does not work perfectly yet, in particular Maps.
+
+-export([t1/0, t2/0, t3/0, t4/0, m1/1, m2/1, m3/1, m4/1]).
+
+-record(r, {id :: integer}).
+
+t1() ->
+    #r{id = a}. % violation
+
+t2() ->
+    [#r{id = a}]. % violation
+
+t3() ->
+    {#r{id = a}}. % violation
+
+t4() ->
+    #{a => #r{id = a}}. % violation found, but t4() returns... (bug)
+
+m1(#r{id = a}) -> % violation
+    ok.
+
+m2([#r{id = a}]) -> % violation
+    ok.
+
+m3({#r{id = a}}) -> % can never match; not so good
+    ok.
+
+m4(#{a := #r{id = a}}) -> % violation not found
+    ok.
diff --git a/lib/dialyzer/test/small_SUITE_data/src/confusing_record_warning.erl b/lib/dialyzer/test/small_SUITE_data/src/relevant_record_warning.erl
index 8af74e0914..3ff65458df 100644
--- a/lib/dialyzer/test/small_SUITE_data/src/confusing_record_warning.erl
+++ b/lib/dialyzer/test/small_SUITE_data/src/relevant_record_warning.erl
@@ -1,3 +1,7 @@
+%% Formerly confusing_record_warning.erl.
+%% The warning output is relevant as of Erlang/OTP 17.1.
+%% The original comment kept below.
+
 %%---------------------------------------------------------------------
 %% A user complained that dialyzer produces a weird warning for the
 %% following program.  I explained to him that there is an implicit
@@ -9,7 +13,7 @@
 %%    The pattern {'r', [_]} can never match the type any()
 %% We should clearly give some less confusing warning in this case.
 %%---------------------------------------------------------------------
--module(confusing_record_warning).
+-module(relevant_record_warning).
 
 -export([test/1]).
 
diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl
index 67661130a5..0927c17b6b 100644
--- a/lib/hipe/cerl/erl_types.erl
+++ b/lib/hipe/cerl/erl_types.erl
@@ -72,7 +72,7 @@
          t_contains_opaque/1, t_contains_opaque/2,
          t_decorate_with_opaque/3,
 	 t_elements/1,
-	 t_find_opaque_mismatch/2,
+	 t_find_opaque_mismatch/3,
          t_find_unknown_opaque/3,
 	 t_fixnum/0,
 	 t_map/2,
@@ -530,39 +530,51 @@ list_contains_opaque(List, Opaques) ->
 %% The first argument of the function is the pattern and its second
 %% argument the type we are matching against the pattern.
 
--spec t_find_opaque_mismatch(erl_type(), erl_type()) -> 'error' | {'ok', erl_type(), erl_type()}.
+-spec t_find_opaque_mismatch(erl_type(), erl_type(), [erl_type()]) ->
+                                'error' | {'ok', erl_type(), erl_type()}.
 
-t_find_opaque_mismatch(T1, T2) ->
-  t_find_opaque_mismatch(T1, T2, T2).
+t_find_opaque_mismatch(T1, T2, Opaques) ->
+  t_find_opaque_mismatch(T1, T2, T2, Opaques).
 
-t_find_opaque_mismatch(?any, _Type, _TopType) -> error;
-t_find_opaque_mismatch(?none, _Type, _TopType) -> error;
-t_find_opaque_mismatch(?list(T1, Tl1, _), ?list(T2, Tl2, _), TopType) ->
-  t_find_opaque_mismatch_ordlists([T1, Tl1], [T2, Tl2], TopType);
-t_find_opaque_mismatch(_T1, ?opaque(_) = T2, TopType) -> {ok, TopType, T2};
-t_find_opaque_mismatch(?opaque(_) = T1, _T2, TopType) ->
+t_find_opaque_mismatch(?any, _Type, _TopType, _Opaques) -> error;
+t_find_opaque_mismatch(?none, _Type, _TopType, _Opaques) -> error;
+t_find_opaque_mismatch(?list(T1, Tl1, _), ?list(T2, Tl2, _), TopType, Opaques) ->
+  t_find_opaque_mismatch_ordlists([T1, Tl1], [T2, Tl2], TopType, Opaques);
+t_find_opaque_mismatch(T1, ?opaque(_) = T2, TopType, Opaques) ->
+  case is_opaque_type(T2, Opaques) of
+    false -> {ok, TopType, T2};
+    true ->
+      t_find_opaque_mismatch(T1, t_opaque_structure(T2), TopType, Opaques)
+  end;
+t_find_opaque_mismatch(?opaque(_) = T1, T2, TopType, Opaques) ->
   %% The generated message is somewhat misleading:
-  {ok, TopType, T1};
-t_find_opaque_mismatch(?product(T1), ?product(T2), TopType) ->
-  t_find_opaque_mismatch_ordlists(T1, T2, TopType);
-t_find_opaque_mismatch(?tuple(T1, Arity, _), ?tuple(T2, Arity, _), TopType) ->
-  t_find_opaque_mismatch_ordlists(T1, T2, TopType);
-t_find_opaque_mismatch(?tuple(_, _, _) = T1, ?tuple_set(_) = T2, TopType) ->
+  case is_opaque_type(T1, Opaques) of
+    false -> {ok, TopType, T1};
+    true ->
+      t_find_opaque_mismatch(t_opaque_structure(T1), T2, TopType, Opaques)
+  end;
+t_find_opaque_mismatch(?product(T1), ?product(T2), TopType, Opaques) ->
+  t_find_opaque_mismatch_ordlists(T1, T2, TopType, Opaques);
+t_find_opaque_mismatch(?tuple(T1, Arity, _), ?tuple(T2, Arity, _),
+                       TopType, Opaques) ->
+  t_find_opaque_mismatch_ordlists(T1, T2, TopType, Opaques);
+t_find_opaque_mismatch(?tuple(_, _, _) = T1, ?tuple_set(_) = T2,
+                       TopType, Opaques) ->
   Tuples1 = t_tuple_subtypes(T1),
   Tuples2 = t_tuple_subtypes(T2),
-  t_find_opaque_mismatch_lists(Tuples1, Tuples2, TopType);
-t_find_opaque_mismatch(T1, ?union(U2), TopType) ->
-  t_find_opaque_mismatch_lists([T1], U2, TopType);
-t_find_opaque_mismatch(_T1, _T2, _TopType) -> error.
+  t_find_opaque_mismatch_lists(Tuples1, Tuples2, TopType, Opaques);
+t_find_opaque_mismatch(T1, ?union(U2), TopType, Opaques) ->
+  t_find_opaque_mismatch_lists([T1], U2, TopType, Opaques);
+t_find_opaque_mismatch(_T1, _T2, _TopType, _Opaques) -> error.
 
-t_find_opaque_mismatch_ordlists(L1, L2, TopType) ->
+t_find_opaque_mismatch_ordlists(L1, L2, TopType, Opaques) ->
   List = lists:zipwith(fun(T1, T2) ->
-			   t_find_opaque_mismatch(T1, T2, TopType)
+			   t_find_opaque_mismatch(T1, T2, TopType, Opaques)
 		       end, L1, L2),
   t_find_opaque_mismatch_list(List).
 
-t_find_opaque_mismatch_lists(L1, L2, _TopType) ->
-  List = [t_find_opaque_mismatch(T1, T2, T2) || T1 <- L1, T2 <- L2],
+t_find_opaque_mismatch_lists(L1, L2, _TopType, Opaques) ->
+  List = [t_find_opaque_mismatch(T1, T2, T2, Opaques) || T1 <- L1, T2 <- L2],
   t_find_opaque_mismatch_list(List).
 
 t_find_opaque_mismatch_list([]) -> error;
@@ -1423,7 +1435,6 @@ t_number_vals(Type) ->
 t_number_vals(Type, Opaques) ->
   do_opaque(Type, Opaques, fun number_vals/1).
 
-number_vals(?int_set(?any)) -> unknown;
 number_vals(?int_set(Set)) -> set_to_list(Set);
 number_vals(?number(_, _)) -> unknown;
 number_vals(?opaque(_)) -> unknown;
diff --git a/lib/stdlib/src/erl_expand_records.erl b/lib/stdlib/src/erl_expand_records.erl
index 57e768ba9d..42b02ade8f 100644
--- a/lib/stdlib/src/erl_expand_records.erl
+++ b/lib/stdlib/src/erl_expand_records.erl
@@ -1,7 +1,7 @@
 %%
 %% %CopyrightBegin%
 %%
-%% Copyright Ericsson AB 2005-2012. All Rights Reserved.
+%% Copyright Ericsson AB 2005-2014. All Rights Reserved.
 %%
 %% The contents of this file are subject to the Erlang Public License,
 %% Version 1.1, (the "License"); you may not use this file except in
@@ -38,6 +38,8 @@
                  checked_ra=[]        % successfully accessed records
                 }).
 
+-define(REC_OFFSET, 100000000). % A hundred millions. Also in v3_core.
+
 -spec(module(AbsForms, CompileOptions) -> AbsForms when
       AbsForms :: [erl_parse:abstract_form()],
       CompileOptions :: [compile:option()]).
@@ -144,10 +146,11 @@ pattern({map_field_exact,Line,K0,V0}, St0) ->
 %%    {{struct,Line,Tag,TPs},TPsvs,St1};
 pattern({record_index,Line,Name,Field}, St) ->
     {index_expr(Line, Field, Name, record_fields(Name, St)),St};
-pattern({record,Line,Name,Pfs}, St0) ->
+pattern({record,Line0,Name,Pfs}, St0) ->
     Fs = record_fields(Name, St0),
     {TMs,St1} = pattern_list(pattern_fields(Fs, Pfs), St0),
-    {{tuple,Line,[{atom,Line,Name} | TMs]},St1};
+    Line = record_offset(Line0, St1),
+    {{tuple,Line,[{atom,Line0,Name} | TMs]},St1};
 pattern({bin,Line,Es0}, St0) ->
     {Es1,St1} = pattern_bin(Es0, St0),
     {{bin,Line,Es1},St1};
@@ -329,8 +332,9 @@ expr({map_field_exact,Line,K0,V0}, St0) ->
 expr({record_index,Line,Name,F}, St) ->
     I = index_expr(Line, F, Name, record_fields(Name, St)),
     expr(I, St);
-expr({record,Line,Name,Is}, St) ->
-    expr({tuple,Line,[{atom,Line,Name} | 
+expr({record,Line0,Name,Is}, St) ->
+    Line = record_offset(Line0, St),
+    expr({tuple,Line,[{atom,Line0,Name} |
                       record_inits(record_fields(Name, St), Is)]},
          St);
 expr({record_field,Line,R,Name,F}, St) ->
@@ -582,8 +586,9 @@ strict_get_record_field(Line, R, {atom,_,F}=Index, Name, St0) ->
             I = index_expr(F, Fs, 2),
             P = record_pattern(2, I, Var, length(Fs)+1, Line, [{atom,Line,Name}]),
             NLine = neg_line(Line),
+            RLine = record_offset(NLine, St),
 	    E = {'case',NLine,R,
-		     [{clause,NLine,[{tuple,NLine,P}],[],[Var]},
+		     [{clause,NLine,[{tuple,RLine,P}],[],[Var]},
 		      {clause,NLine,[{var,NLine,'_'}],[],
 		       [{call,NLine,{remote,NLine,
 				    {atom,NLine,erlang},
@@ -961,3 +966,10 @@ opt_remove_2(A, _) -> A.
 
 neg_line(L) ->
     erl_parse:set_line(L, fun(Line) -> -abs(Line) end).
+
+record_offset(L, St) ->
+    case lists:member(annotate_records, St#exprec.compile) of
+        true when L >= 0 -> L+?REC_OFFSET;
+        true when L < 0  -> L-?REC_OFFSET;
+        false -> L
+    end.