beam_ssa_type: Track the types of tuple elements

Prior to 294d66a295f6c2101fe3c2da630979ad4e736c08 there wasn't much
point to keeping track of tuple element types; they were only known
when we had inserted or extracted values from a tuple, and in
neither case was it likely that we'd extract the same values again.

It makes a lot more sense to do so now that type optimizations are
applied across functions; if we return a tuple it's very likely
that its elements will be extracted soon after, and knowing their
types lets us eliminate more type checks.

Co-authored-by: Björn Gustavsson <[email protected]>

4 files changed, 460 insertions, 190 deletions

diff --git a/lib/compiler/src/beam_ssa_pre_codegen.erl b/lib/compiler/src/beam_ssa_pre_codegen.erl
index 274f78052d..ad57a45ef2 100644
--- a/lib/compiler/src/beam_ssa_pre_codegen.erl
+++ b/lib/compiler/src/beam_ssa_pre_codegen.erl
@@ -1993,11 +1993,12 @@ reserve_zregs(Blocks, Intervals, Res) ->
         end,
     beam_ssa:fold_rpo(F, [0], Res, Blocks).
 
-reserve_zreg([#b_set{op=call,dst=Dst}],
-              #b_br{bool=Dst}, _ShortLived, A) ->
-    %% If type optimization has determined that the result of a call can be
-    %% used directly in a branch, we must avoid reserving a z register or code
-    %% generation will fail.
+reserve_zreg([#b_set{op=Op,dst=Dst}],
+              #b_br{bool=Dst}, _ShortLived, A) when Op =:= call;
+                                                    Op =:= get_tuple_element ->
+    %% If type optimization has determined that the result of these
+    %% instructions can be used directly in a branch, we must avoid reserving a
+    %% z register or code generation will fail.
     A;
 reserve_zreg([#b_set{op={bif,tuple_size},dst=Dst},
               #b_set{op={bif,'=:='},args=[Dst,Val]}], Last, ShortLived, A0) ->
diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl
index 87cd7a8c36..e51f8cdcb7 100644
--- a/lib/compiler/src/beam_ssa_type.erl
+++ b/lib/compiler/src/beam_ssa_type.erl
@@ -23,7 +23,7 @@
 
 -include("beam_ssa_opt.hrl").
 -import(lists, [all/2,any/2,droplast/1,foldl/3,last/1,member/2,
-                partition/2,reverse/1,sort/1]).
+                partition/2,reverse/1,seq/2,sort/1]).
 
 -define(UNICODE_INT, #t_integer{elements={0,16#10FFFF}}).
 
@@ -44,12 +44,13 @@
 -record(t_bs_match, {type :: type()}).
 -record(t_tuple, {size=0 :: integer(),
                   exact=false :: boolean(),
-                  elements=[] :: [any()]
-                 }).
+                  %% Known element types (1-based index), unknown elements are
+                  %% are assumed to be 'any'.
+                  elements=#{} :: #{ non_neg_integer() => type() }}).
 
 -type type() :: 'any' | 'none' |
                 #t_atom{} | #t_integer{} | #t_bs_match{} | #t_tuple{} |
-                {'binary',pos_integer()} | 'cons' | 'float' | 'list' | 'map' | 'nil' |'number'.
+                {'binary',pos_integer()} | 'cons' | 'float' | 'list' | 'map' | 'nil' | 'number'.
 -type type_db() :: #{beam_ssa:var_name():=type()}.
 
 -spec opt_start(Linear, Args, Anno, FuncDb) -> {Linear, FuncDb} when
@@ -166,8 +167,11 @@ opt_finish_1([Arg | Args], [TypeMap | TypeMaps], ParamInfo0) ->
 opt_finish_1([], [], ParamInfo) ->
     ParamInfo.
 
-validator_anno(#t_tuple{size=Size,exact=Exact}) ->
-    beam_validator:type_anno(tuple, Size, Exact);
+validator_anno(#t_tuple{size=Size,exact=Exact,elements=Elements0}) ->
+    Elements = maps:fold(fun(Index, Type, Acc) ->
+                                 Acc#{ Index => validator_anno(Type) }
+                         end, #{}, Elements0),
+    beam_validator:type_anno(tuple, Size, Exact, Elements);
 validator_anno(#t_integer{elements={Same,Same}}) ->
     beam_validator:type_anno(integer, Same);
 validator_anno(#t_integer{}) ->
@@ -292,6 +296,12 @@ opt_is([#b_set{op=call,args=Args0,dst=Dst}=I0 | Is],
             Ds = Ds0#{ Dst => I1 },
             opt_is(Is, Ts, Ds, Fdb0, Ls, D, Sub, [I1|Acc])
     end;
+opt_is([#b_set{op=set_tuple_element}=I0|Is],
+       Ts0, Ds0, Fdb, Ls, D, Sub, Acc) ->
+    %% This instruction lacks a return value and destructively updates its
+    %% source, so it needs special handling to update the source type.
+    {Ts, Ds, I} = opt_set_tuple_element(I0, Ts0, Ds0, Sub),
+    opt_is(Is, Ts, Ds, Fdb, Ls, D, Sub, [I|Acc]);
 opt_is([#b_set{op=succeeded,args=[Arg],dst=Dst}=I],
        Ts0, Ds0, Fdb, Ls, D, Sub0, Acc) ->
     case Ds0 of
@@ -396,6 +406,28 @@ update_arg_types([Arg | Args], [TypeMap0 | TypeMaps], CallId, Ts) ->
 update_arg_types([], [], _CallId, _Ts) ->
     [].
 
+opt_set_tuple_element(#b_set{op=set_tuple_element,args=Args0,dst=Dst}=I0,
+                      Ts0, Ds0, Sub) ->
+    Args = simplify_args(Args0, Sub, Ts0),
+    [Val,#b_var{}=Src,#b_literal{val=N}] = Args,
+
+    SrcType0 = get_type(Src, Ts0),
+    ValType = get_type(Val, Ts0),
+    Index = N + 1,
+
+    #t_tuple{size=Size,elements=Es0} = SrcType0,
+    true = Index =< Size,                     %Assertion.
+
+    Es = set_element_type(Index, ValType, Es0),
+    SrcType = SrcType0#t_tuple{elements=Es},
+
+    I = beam_ssa:normalize(I0#b_set{args=Args}),
+
+    Ts = Ts0#{ Dst => any, Src => SrcType },
+    Ds = Ds0#{ Dst => I },
+
+    {Ts, Ds, I}.
+
 simplify(#b_set{op={bif,'and'},args=Args}=I, Ts) ->
     case is_safe_bool_op(Args, Ts) of
         true ->
@@ -418,12 +450,14 @@ simplify(#b_set{op={bif,'or'},args=Args}=I, Ts) ->
         false ->
             I
     end;
-simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I, Ts) ->
+simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I0, Ts) ->
     case t_tuple_size(get_type(Tuple, Ts)) of
         {_,Size} when is_integer(Index), 1 =< Index, Index =< Size ->
-            I#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=Index-1}]};
+            I = I0#b_set{op=get_tuple_element,
+                         args=[Tuple,#b_literal{val=Index-1}]},
+            simplify(I, Ts);
         _ ->
-            eval_bif(I, Ts)
+            eval_bif(I0, Ts)
     end;
 simplify(#b_set{op={bif,hd},args=[List]}=I, Ts) ->
     case get_type(List, Ts) of
@@ -485,11 +519,17 @@ simplify(#b_set{op={bif,Op},args=Args}=I, Ts) ->
             AnnoArgs = [anno_float_arg(A) || A <- Types],
             eval_bif(beam_ssa:add_anno(float_op, AnnoArgs, I), Ts)
     end;
-simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=0}]}=I, Ts) ->
+simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=N}]}=I, Ts) ->
     case get_type(Tuple, Ts) of
-        #t_tuple{elements=[First]} ->
-            #b_literal{val=First};
-        #t_tuple{} ->
+        #t_tuple{size=Size,elements=Es} when Size > N ->
+            ElemType = get_element_type(N + 1, Es),
+            case get_literal_from_type(ElemType) of
+                #b_literal{}=Lit -> Lit;
+                none -> I
+            end;
+        none ->
+            %% Will never be executed because of type conflict.
+            %% #b_literal{val=ignored};
             I
     end;
 simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) ->
@@ -500,24 +540,8 @@ simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) ->
         _ ->    #b_literal{val=false}
     end;
 simplify(#b_set{op=is_tagged_tuple,
-                args=[Src,#b_literal{val=Size},#b_literal{val=Tag}]}=I, Ts) ->
-    case get_type(Src, Ts) of
-        #t_tuple{exact=true,size=Size,elements=[Tag]} ->
-            #b_literal{val=true};
-        #t_tuple{exact=true,size=ActualSize,elements=[]} ->
-            if
-                Size =/= ActualSize ->
-                    #b_literal{val=false};
-                true ->
-                    I
-            end;
-        #t_tuple{exact=false} ->
-            I;
-        any ->
-            I;
-        _ ->
-            #b_literal{val=false}
-    end;
+                args=[Src,#b_literal{val=Size},#b_literal{}=Tag]}=I, Ts) ->
+    simplify_is_record(I, get_type(Src, Ts), Size, Tag, Ts);
 simplify(#b_set{op=put_list,args=[#b_literal{val=H},
                                   #b_literal{val=T}]}, _Ts) ->
     #b_literal{val=[H|T]};
@@ -786,19 +810,40 @@ type(bs_get_tail, _Args, _Ts, _Ds) ->
 type(call, [#b_remote{mod=#b_literal{val=Mod},
                       name=#b_literal{val=Name}}|Args], Ts, _Ds) ->
     case {Mod,Name,Args} of
-        {erlang,setelement,[Pos,Tuple,_]} ->
+        {erlang,setelement,[Pos,Tuple,Arg]} ->
             case {get_type(Pos, Ts),get_type(Tuple, Ts)} of
-                {#t_integer{elements={MinIndex,_}},#t_tuple{}=T}
-                  when MinIndex > 1 ->
-                    %% First element is not updated. The result
-                    %% will have the same type.
-                    T;
+                {#t_integer{elements={Index,Index}},
+                 #t_tuple{elements=Es0,size=Size}=T} ->
+                    %% This is an exact index, update the type of said element
+                    %% or return 'none' if it's known to be out of bounds.
+                    Es = set_element_type(Index, get_type(Arg, Ts), Es0),
+                    case T#t_tuple.exact of
+                        false ->
+                            T#t_tuple{size=max(Index, Size),elements=Es};
+                        true when Index =< Size ->
+                            T#t_tuple{elements=Es};
+                        true ->
+                            none
+                    end;
+                {#t_integer{elements={Min,Max}},
+                 #t_tuple{elements=Es0,size=Size}=T} ->
+                    %% We know this will land between Min and Max, so kill the
+                    %% types for those indexes.
+                    Es = maps:without(seq(Min, Max), Es0),
+                    case T#t_tuple.exact of
+                        false ->
+                            T#t_tuple{elements=Es,size=max(Min, Size)};
+                        true when Min =< Size ->
+                            T#t_tuple{elements=Es,size=Size};
+                        true ->
+                            none
+                    end;
                 {_,#t_tuple{}=T} ->
-                    %% Position is 1 or unknown. May update the first
-                    %% element of the tuple.
-                    T#t_tuple{elements=[]};
-                {#t_integer{elements={MinIndex,_}},_} ->
-                    #t_tuple{size=MinIndex};
+                    %% Position unknown, so we have to discard all element
+                    %% information.
+                    T#t_tuple{elements=#{}};
+                {#t_integer{elements={Min,_Max}},_} ->
+                    #t_tuple{size=Min};
                 {_,_} ->
                     #t_tuple{}
             end;
@@ -821,6 +866,11 @@ type(call, [#b_remote{mod=#b_literal{val=Mod},
                 false -> any
             end
     end;
+type(get_tuple_element, [Tuple, Offset], Ts, _Ds) ->
+    #t_tuple{size=Size,elements=Es} = get_type(Tuple, Ts),
+    #b_literal{val=N} = Offset,
+    true = Size > N, %Assertion.
+    get_element_type(N + 1, Es);
 type(is_nonempty_list, [_], _Ts, _Ds) ->
     t_boolean();
 type(is_tagged_tuple, [_,#b_literal{},#b_literal{}], _Ts, _Ds) ->
@@ -829,13 +879,13 @@ type(put_map, _Args, _Ts, _Ds) ->
     map;
 type(put_list, _Args, _Ts, _Ds) ->
     cons;
-type(put_tuple, Args, _Ts, _Ds) ->
-    case Args of
-        [#b_literal{val=First}|_] ->
-            #t_tuple{exact=true,size=length(Args),elements=[First]};
-        _ ->
-            #t_tuple{exact=true,size=length(Args)}
-    end;
+type(put_tuple, Args, Ts, _Ds) ->
+    {Es, _} = foldl(fun(Arg, {Es0, Index}) ->
+                        Type = get_type(Arg, Ts),
+                        Es = set_element_type(Index, Type, Es0),
+                        {Es, Index + 1}
+                    end, {#{}, 1}, Args),
+    #t_tuple{exact=true,size=length(Args),elements=Es};
 type(succeeded, [#b_var{}=Src], Ts, Ds) ->
     case maps:get(Src, Ds) of
         #b_set{op={bif,Bif},args=BifArgs} ->
@@ -1048,6 +1098,34 @@ eq_ranges([H], H, H) -> true;
 eq_ranges([H|T], H, Max) -> eq_ranges(T, H+1, Max);
 eq_ranges(_, _, _) -> false.
 
+simplify_is_record(I, #t_tuple{exact=Exact,
+                               size=Size,
+                               elements=Es},
+                   RecSize, RecTag, Ts) ->
+    TagType = maps:get(1, Es, any),
+    TagMatch = case get_literal_from_type(TagType) of
+                   #b_literal{}=RecTag -> yes;
+                   #b_literal{} -> no;
+                   none ->
+                       %% Is it at all possible for the tag to match?
+                       case meet(get_type(RecTag, Ts), TagType) of
+                           none -> no;
+                           _ -> maybe
+                       end
+               end,
+    if
+        Size =/= RecSize, Exact; Size > RecSize; TagMatch =:= no ->
+            #b_literal{val=false};
+        Size =:= RecSize, Exact, TagMatch =:= yes ->
+            #b_literal{val=true};
+        true ->
+            I
+    end;
+simplify_is_record(I, any, _Size, _Tag, _Ts) ->
+    I;
+simplify_is_record(_I, _Type, _Size, _Tag, _Ts) ->
+    #b_literal{val=false}.
+
 simplify_switch_bool(#b_switch{arg=B,list=List0}=Sw, Ts, Ds) ->
     List = sort(List0),
     case List of
@@ -1150,8 +1228,12 @@ get_type(#b_literal{val=Val}, _Ts) ->
         Val =:= {} ->
             #t_tuple{exact=true};
         is_tuple(Val) ->
-            #t_tuple{exact=true,size=tuple_size(Val),
-                     elements=[element(1, Val)]};
+            {Es, _} = foldl(fun(E, {Es0, Index}) ->
+                                Type = get_type(#b_literal{val=E}, #{}),
+                                Es = set_element_type(Index, Type, Es0),
+                                {Es, Index + 1}
+                            end, {#{}, 1}, tuple_to_list(Val)),
+            #t_tuple{exact=true,size=tuple_size(Val),elements=Es};
         Val =:= [] ->
             nil;
         true ->
@@ -1221,8 +1303,7 @@ infer_types_switch(V, Lit, Ts, #d{ds=Ds}) ->
 infer_eq_type({bif,'=:='}, [#b_var{}=Src,#b_literal{}=Lit], Ts, Ds) ->
     Def = maps:get(Src, Ds),
     Type = get_type(Lit, Ts),
-    [{Src,Type}|infer_tuple_size(Def, Lit) ++
-         infer_first_element(Def, Lit)];
+    [{Src,Type} | infer_eq_lit(Def, Lit)];
 infer_eq_type({bif,'=:='}, [#b_var{}=Arg0,#b_var{}=Arg1], Ts, _Ds) ->
     %% As an example, assume that L1 is known to be 'list', and L2 is
     %% known to be 'cons'. Then if 'L1 =:= L2' evaluates to 'true', it can
@@ -1237,6 +1318,17 @@ infer_eq_type({bif,'=:='}, [#b_var{}=Arg0,#b_var{}=Arg1], Ts, _Ds) ->
 infer_eq_type(_Op, _Args, _Ts, _Ds) ->
     [].
 
+infer_eq_lit(#b_set{op={bif,tuple_size},args=[#b_var{}=Tuple]},
+             #b_literal{val=Size}) when is_integer(Size) ->
+    [{Tuple,#t_tuple{exact=true,size=Size}}];
+infer_eq_lit(#b_set{op=get_tuple_element,
+                    args=[#b_var{}=Tuple,#b_literal{val=N}]},
+             #b_literal{}=Lit) ->
+    Index = N + 1,
+    Es = set_element_type(Index, get_type(Lit, #{}), #{}),
+    [{Tuple,#t_tuple{size=Index,elements=Es}}];
+infer_eq_lit(_, _) -> [].
+
 infer_type({bif,element}, [#b_literal{val=Pos},#b_var{}=Tuple], _Ds) ->
     if
         is_integer(Pos), 1 =< Pos ->
@@ -1270,8 +1362,9 @@ infer_type(bs_start_match, [#b_var{}=Bin], _Ds) ->
 infer_type(is_nonempty_list, [#b_var{}=Src], _Ds) ->
     [{Src,cons}];
 infer_type(is_tagged_tuple, [#b_var{}=Src,#b_literal{val=Size},
-                             #b_literal{val=Tag}], _Ds) ->
-    [{Src,#t_tuple{exact=true,size=Size,elements=[Tag]}}];
+                             #b_literal{}=Tag], _Ds) ->
+    Es = set_element_type(1, get_type(Tag, #{}), #{}),
+    [{Src,#t_tuple{exact=true,size=Size,elements=Es}}];
 infer_type(succeeded, [#b_var{}=Src], Ds) ->
     #b_set{op=Op,args=Args} = maps:get(Src, Ds),
     infer_type(Op, Args, Ds);
@@ -1364,17 +1457,6 @@ inferred_bif_type('*', [_,_]) -> number;
 inferred_bif_type('/', [_,_]) -> number;
 inferred_bif_type(_, _) -> any.
 
-infer_tuple_size(#b_set{op={bif,tuple_size},args=[#b_var{}=Tuple]},
-                 #b_literal{val=Size}) when is_integer(Size) ->
-    [{Tuple,#t_tuple{exact=true,size=Size}}];
-infer_tuple_size(_, _) -> [].
-
-infer_first_element(#b_set{op=get_tuple_element,
-                           args=[#b_var{}=Tuple,#b_literal{val=0}]},
-                    #b_literal{val=First}) ->
-    [{Tuple,#t_tuple{size=1,elements=[First]}}];
-infer_first_element(_, _) -> [].
-
 is_math_bif(cos, 1) -> true;
 is_math_bif(cosh, 1) -> true;
 is_math_bif(sin, 1) -> true;
@@ -1473,6 +1555,19 @@ t_tuple_size(_) ->
 is_singleton_type(Type) ->
     get_literal_from_type(Type) =/= none.
 
+get_element_type(Index, Es) ->
+    case Es of
+        #{ Index := T } -> T;
+        #{} -> any
+    end.
+
+set_element_type(_Key, none, Es) ->
+    Es;
+set_element_type(Key, any, Es) ->
+    maps:remove(Key, Es);
+set_element_type(Key, Type, Es) ->
+    Es#{ Key => Type }.
+
 %% join(Type1, Type2) -> Type
 %%  Return the "join" of Type1 and Type2. The join is a more general
 %%  type than Type1 and Type2. For example:
@@ -1520,15 +1615,41 @@ join(#t_integer{}, number) -> number;
 join(number, #t_integer{}) -> number;
 join(float, number) -> number;
 join(number, float) -> number;
-join(#t_tuple{size=Sz,exact=Exact1}, #t_tuple{size=Sz,exact=Exact2}) ->
-    Exact = Exact1 and Exact2,
-    #t_tuple{size=Sz,exact=Exact};
-join(#t_tuple{size=Sz1}, #t_tuple{size=Sz2}) ->
-    #t_tuple{size=min(Sz1, Sz2)};
+join(#t_tuple{size=Sz,exact=ExactA,elements=EsA},
+     #t_tuple{size=Sz,exact=ExactB,elements=EsB}) ->
+    Exact = ExactA and ExactB,
+    Es = join_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,exact=Exact,elements=Es};
+join(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) ->
+    Sz = min(SzA, SzB),
+    Es = join_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,elements=Es};
 join(_T1, _T2) ->
     %%io:format("~p ~p\n", [_T1,_T2]),
     any.
 
+join_tuple_elements(MinSize, EsA, EsB) ->
+    Es0 = join_elements(EsA, EsB),
+    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
+
+join_elements(Es1, Es2) ->
+    Keys = if
+               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
+               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
+           end,
+    join_elements_1(Keys, Es1, Es2, #{}).
+
+join_elements_1([Key | Keys], Es1, Es2, Acc0) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            Acc = set_element_type(Key, join(Type1, Type2), Acc0),
+            join_elements_1(Keys, Es1, Es2, Acc);
+        {#{}, #{}} ->
+            join_elements_1(Keys, Es1, Es2, Acc0)
+    end;
+join_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
 gcd(A, B) ->
     case A rem B of
         0 -> B;
@@ -1625,9 +1746,6 @@ meet(_, _) ->
     %% Inconsistent types. There will be an exception at runtime.
     none.
 
-meet_tuples(#t_tuple{elements=[E1]}, #t_tuple{elements=[E2]})
-  when E1 =/= E2 ->
-    none;
 meet_tuples(#t_tuple{size=Sz1,exact=true},
             #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 ->
     none;
@@ -1635,12 +1753,31 @@ meet_tuples(#t_tuple{size=Sz1,exact=Ex1,elements=Es1},
             #t_tuple{size=Sz2,exact=Ex2,elements=Es2}) ->
     Size = max(Sz1, Sz2),
     Exact = Ex1 or Ex2,
-    Es = case {Es1,Es2} of
-             {[],[_|_]} -> Es2;
-             {[_|_],[]} -> Es1;
-             {_,_} -> Es1
-         end,
-    #t_tuple{size=Size,exact=Exact,elements=Es}.
+    case meet_elements(Es1, Es2) of
+        none ->
+            none;
+        Es ->
+            #t_tuple{size=Size,exact=Exact,elements=Es}
+    end.
+
+meet_elements(Es1, Es2) ->
+    Keys = maps:keys(Es1) ++ maps:keys(Es2),
+    meet_elements_1(Keys, Es1, Es2, #{}).
+
+meet_elements_1([Key | Keys], Es1, Es2, Acc) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            case meet(Type1, Type2) of
+                none -> none;
+                Type -> meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
+            end;
+        {#{ Key := Type1 }, _} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
+        {_, #{ Key := Type2 }} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
+    end;
+meet_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
 
 %% verified_type(Type) -> Type
 %%  Returns the passed in type if it is one of the defined types.
@@ -1679,5 +1816,13 @@ verified_type(map=T) -> T;
 verified_type(nil=T) -> T;
 verified_type(cons=T) -> T;
 verified_type(number=T) -> T;
-verified_type(#t_tuple{}=T) -> T;
+verified_type(#t_tuple{size=Size,elements=Es}=T) ->
+    %% All known elements must have a valid index and type. 'any' is prohibited
+    %% since it's implicit and should never be present in the map.
+    maps:fold(fun(Index, Element, _) when is_integer(Index),
+                                          1 =< Index, Index =< Size,
+                                          Element =/= any, Element =/= none ->
+                      verified_type(Element)
+              end, [], Es),
+    T;
 verified_type(float=T) -> T.
diff --git a/lib/compiler/src/beam_validator.erl b/lib/compiler/src/beam_validator.erl
index b66eb0074c..3b197f7bae 100644
--- a/lib/compiler/src/beam_validator.erl
+++ b/lib/compiler/src/beam_validator.erl
@@ -26,7 +26,7 @@
 
 %% Interface for compiler.
 -export([module/2, format_error/1]).
--export([type_anno/1, type_anno/2, type_anno/3]).
+-export([type_anno/1, type_anno/2, type_anno/4]).
 
 -import(lists, [any/2,dropwhile/2,foldl/3,map/2,foreach/2,reverse/1]).
 
@@ -65,11 +65,12 @@ type_anno(atom, Value) -> {atom, Value};
 type_anno(float, Value) -> {float, Value};
 type_anno(integer, Value) -> {integer, Value}.
 
--spec type_anno(term(), term(), term()) -> term().
-type_anno(tuple, Size, Exact) when is_integer(Size) ->
+-spec type_anno(term(), term(), term(), term()) -> term().
+type_anno(tuple, Size, Exact, Elements) when is_integer(Size), Size >= 0,
+                                             is_map(Elements) ->
     case Exact of
-        true -> {tuple, Size};
-        false -> {tuple, [Size]}
+        true -> {tuple, Size, Elements};
+        false -> {tuple, [Size], Elements}
     end.
 
 -spec format_error(term()) -> iolist().
@@ -367,13 +368,18 @@ valfun_1({put_tuple2,Dst,{list,Elements}}, Vst0) ->
     _ = [assert_not_fragile(El, Vst0) || El <- Elements],
     Size = length(Elements),
     Vst = eat_heap(Size+1, Vst0),
-    Type = {tuple,Size},
+    {Es,_} = foldl(fun(Val, {Es0, Index}) ->
+                       Type = get_term_type(Val, Vst0),
+                       Es = set_element_type(Index, Type, Es0),
+                       {Es, Index + 1}
+               end, {#{}, 1}, Elements),
+    Type = {tuple,Size,Es},
     create_term(Type, Dst, Vst);
 valfun_1({put_tuple,Sz,Dst}, Vst0) when is_integer(Sz) ->
     Vst1 = eat_heap(1, Vst0),
     Vst = create_term(tuple_in_progress, Dst, Vst1),
     #vst{current=St0} = Vst,
-    St = St0#st{puts_left={Sz,{Dst,{tuple,Sz}}}},
+    St = St0#st{puts_left={Sz,{Dst,Sz,#{}}}},
     Vst#vst{current=St};
 valfun_1({put,Src}, Vst0) ->
     assert_not_fragile(Src, Vst0),
@@ -382,11 +388,13 @@ valfun_1({put,Src}, Vst0) ->
     case St0 of
         #st{puts_left=none} ->
             error(not_building_a_tuple);
-        #st{puts_left={1,{Dst,Type}}} ->
+        #st{puts_left={1,{Dst,Sz,Es}}} ->
             St = St0#st{puts_left=none},
-            create_term(Type, Dst, Vst#vst{current=St});
-        #st{puts_left={PutsLeft,Info}} when is_integer(PutsLeft) ->
-            St = St0#st{puts_left={PutsLeft-1,Info}},
+            create_term({tuple,Sz,Es}, Dst, Vst#vst{current=St});
+        #st{puts_left={PutsLeft,{Dst,Sz,Es0}}} when is_integer(PutsLeft) ->
+            Index = Sz - PutsLeft + 1,
+            Es = Es0#{ Index => get_term_type(Src, Vst0) },
+            St = St0#st{puts_left={PutsLeft-1,{Dst,Sz,Es}}},
             Vst#vst{current=St}
     end;
 %% Instructions for optimization of selective receives.
@@ -492,10 +500,11 @@ valfun_1({get_tl,Src,Dst}, Vst) ->
     assert_not_literal(Src),
     assert_type(cons, Src, Vst),
     extract_term(term, [Src], Dst, Vst);
-valfun_1({get_tuple_element,Src,I,Dst}, Vst) ->
+valfun_1({get_tuple_element,Src,N,Dst}, Vst) ->
     assert_not_literal(Src),
-    assert_type({tuple_element,I+1}, Src, Vst),
-    extract_term(term, [Src], Dst, Vst);
+    assert_type({tuple_element,N+1}, Src, Vst),
+    Type = get_element_type(N+1, Src, Vst),
+    extract_term(Type, [Src], Dst, Vst);
 valfun_1({jump,{f,Lbl}}, Vst) ->
     kill_state(branch_state(Lbl, Vst));
 valfun_1(I, Vst) ->
@@ -595,14 +604,18 @@ valfun_4({make_fun2,_,_,_,Live}, Vst) ->
 %% Other BIFs
 valfun_4({bif,tuple_size,{f,Fail},[Tuple],Dst}=I, Vst0) ->
     Vst1 = branch_state(Fail, Vst0),
-    Vst = update_type(fun meet/2, {tuple,[0]}, Tuple, Vst1),
+    Vst = update_type(fun meet/2, {tuple,[0],#{}}, Tuple, Vst1),
     set_type_reg_expr({integer,[]}, I, Dst, Vst);
 valfun_4({bif,element,{f,Fail},[Pos,Tuple],Dst}, Vst0) ->
     PosType = get_durable_term_type(Pos, Vst0),
+    ElementType = case PosType of
+                      {integer,I} -> get_element_type(I, Tuple, Vst0);
+                      _ -> term
+                  end,
+    InferredType = {tuple,[get_tuple_size(PosType)],#{}},
     Vst1 = branch_state(Fail, Vst0),
-    Type = {tuple,[get_tuple_size(PosType)]},
-    Vst = update_type(fun meet/2, Type, Tuple, Vst1),
-    extract_term(term, [Tuple], Dst, Vst);
+    Vst = update_type(fun meet/2, InferredType, Tuple, Vst1),
+    extract_term(ElementType, [Tuple], Dst, Vst);
 valfun_4({bif,raise,{f,0},Src,_Dst}, Vst) ->
     validate_src(Src, Vst),
     kill_state(Vst);
@@ -671,10 +684,13 @@ valfun_4(timeout, #vst{current=St}=Vst) ->
     Vst#vst{current=St#st{x=init_regs(0, term)}};
 valfun_4(send, Vst) ->
     call(send, 2, Vst);
-valfun_4({set_tuple_element,Src,Tuple,I}, Vst) ->
+valfun_4({set_tuple_element,Src,Tuple,N}, Vst) ->
+    I = N + 1,
     assert_not_fragile(Src, Vst),
-    assert_type({tuple_element,I+1}, Tuple, Vst),
-    Vst;
+    assert_type({tuple_element,I}, Tuple, Vst),
+    {tuple, Sz, Es0} = get_term_type(Tuple, Vst),
+    Es = set_element_type(I, get_term_type(Src, Vst), Es0),
+    set_aliased_type({tuple, Sz, Es}, Tuple, Vst);
 %% Match instructions.
 valfun_4({select_val,Src,{f,Fail},{list,Choices}}, Vst0) ->
     assert_term(Src, Vst0),
@@ -748,7 +764,7 @@ valfun_4({test,is_boolean,{f,Lbl},[Src]}, Vst) ->
 valfun_4({test,is_float,{f,Lbl},[Src]}, Vst) ->
     type_test(Lbl, {float,[]}, Src, Vst);
 valfun_4({test,is_tuple,{f,Lbl},[Src]}, Vst) ->
-    type_test(Lbl, {tuple,[0]}, Src, Vst);
+    type_test(Lbl, {tuple,[0],#{}}, Src, Vst);
 valfun_4({test,is_integer,{f,Lbl},[Src]}, Vst) ->
     type_test(Lbl, {integer,[]}, Src, Vst);
 valfun_4({test,is_nonempty_list,{f,Lbl},[Src]}, Vst) ->
@@ -769,10 +785,11 @@ valfun_4({test,is_map,{f,Lbl},[Src]}, Vst) ->
     end;
 valfun_4({test,test_arity,{f,Lbl},[Tuple,Sz]}, Vst) when is_integer(Sz) ->
     assert_type(tuple, Tuple, Vst),
-    update_type(fun meet/2, {tuple,Sz}, Tuple, branch_state(Lbl, Vst));
-valfun_4({test,is_tagged_tuple,{f,Lbl},[Src,Sz,_Atom]}, Vst) ->
-    assert_term(Src, Vst),
-    update_type(fun meet/2, {tuple,Sz}, Src, branch_state(Lbl, Vst));
+    update_type(fun meet/2, {tuple,Sz,#{}}, Tuple, branch_state(Lbl, Vst));
+valfun_4({test,is_tagged_tuple,{f,Lbl},[Src,Sz,Atom]}, Vst0) ->
+    assert_term(Src, Vst0),
+    Vst = branch_state(Lbl, Vst0),
+    update_type(fun meet/2, {tuple,Sz,#{ 1 => Atom }}, Src, Vst);
 valfun_4({test,has_map_fields,{f,Lbl},Src,{list,List}}, Vst) ->
     assert_type(map, Src, Vst),
     assert_unique_map_keys(List),
@@ -1229,7 +1246,10 @@ assert_unique_map_keys([]) ->
 assert_unique_map_keys([_]) ->
     ok;
 assert_unique_map_keys([_,_|_]=Ls) ->
-    Vs = [get_literal(L) || L <- Ls],
+    Vs = [begin
+              assert_literal(L),
+              L
+          end || L <- Ls],
     case length(Vs) =:= sets:size(sets:from_list(Vs)) of
 	true -> ok;
 	false -> error(keys_not_unique)
@@ -1308,7 +1328,7 @@ infer_types(Src, Vst) ->
             end;
         {bif,tuple_size,{f,_},[Tuple],_} ->
             fun({integer,Arity}, S) ->
-                    update_type(fun meet/2, {tuple,Arity}, Tuple, S);
+                    update_type(fun meet/2, {tuple,Arity,#{}}, Tuple, S);
                (_, S) -> S
             end;
         {bif,'=:=',{f,_},[ArityReg,{integer,_}=Val],_} when ArityReg =/= Src ->
@@ -1547,6 +1567,13 @@ assert_not_fragile(Src, Vst) ->
         _ -> ok
     end.
 
+assert_literal(nil) -> ok;
+assert_literal({atom,A}) when is_atom(A) -> ok;
+assert_literal({float,F}) when is_float(F) -> ok;
+assert_literal({integer,I}) when is_integer(I) -> ok;
+assert_literal({literal,_L}) -> ok;
+assert_literal(T) -> error({literal_required,T}).
+
 assert_not_literal({x,_}) -> ok;
 assert_not_literal({y,_}) -> ok;
 assert_not_literal(Literal) -> error({literal_not_allowed,Literal}).
@@ -1593,11 +1620,12 @@ assert_not_literal(Literal) -> error({literal_not_allowed,Literal}).
 %%
 %% list                 List: [] or [_|_]
 %%
-%% {tuple,[Sz]}		Tuple. An element has been accessed using
-%%              	element/2 or setelement/3 so that it is known that
-%%              	the type is a tuple of size at least Sz.
+%% {tuple,[Sz],Es}      Tuple. An element has been accessed using
+%%                      element/2 or setelement/3 so that it is known that
+%%                      the type is a tuple of size at least Sz. Es is a map
+%%                      containing known types by tuple index.
 %%
-%% {tuple,Sz}		Tuple. A test_arity instruction has been seen
+%% {tuple,Sz,Es}	Tuple. A test_arity instruction has been seen
 %%           		so that it is known that the size is exactly Sz.
 %%
 %% {atom,[]}		Atom.
@@ -1632,6 +1660,10 @@ assert_not_literal(Literal) -> error({literal_not_allowed,Literal}).
 
 meet(Same, Same) ->
     Same;
+meet({literal,_}=T1, T2) ->
+    meet_literal(T1, T2);
+meet(T1, {literal,_}=T2) ->
+    meet_literal(T2, T1);
 meet(term, Other) ->
     Other;
 meet(Other, term) ->
@@ -1647,18 +1679,49 @@ meet(T1, T2) ->
         {list,nil} -> nil;
         {number,{integer,_}=T} -> T;
         {number,{float,_}=T} -> T;
-        {{tuple,Size1},{tuple,Size2}} ->
-            case {Size1,Size2} of
-                {[Sz1],[Sz2]} ->
-                    {tuple,[erlang:max(Sz1, Sz2)]};
-                {Sz1,[Sz2]} when Sz2 =< Sz1 ->
-                    {tuple,Sz1};
-                {_,_} ->
+        {{tuple,Size1,Es1},{tuple,Size2,Es2}} ->
+            Es = meet_elements(Es1, Es2),
+            case {Size1,Size2,Es} of
+                {_, _, none} ->
+                    none;
+                {[Sz1],[Sz2],_} ->
+                    {tuple,[erlang:max(Sz1, Sz2)],Es};
+                {Sz1,[Sz2],_} when Sz2 =< Sz1 ->
+                    {tuple,Sz1,Es};
+                {Sz,Sz,_} ->
+                    {tuple,Sz,Es};
+                {_,_,_} ->
                     none
             end;
         {_,_} -> none
     end.
 
+%% Meets types of literals.
+meet_literal({literal,_}=Lit, T) ->
+    meet_literal(T, get_literal_type(Lit));
+meet_literal(T1, T2) ->
+    %% We're done extracting the types, try merging them again.
+    meet(T1, T2).
+
+meet_elements(Es1, Es2) ->
+    Keys = maps:keys(Es1) ++ maps:keys(Es2),
+    meet_elements_1(Keys, Es1, Es2, #{}).
+
+meet_elements_1([Key | Keys], Es1, Es2, Acc) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            case meet(Type1, Type2) of
+                none -> none;
+                Type -> meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
+            end;
+        {#{ Key := Type1 }, _} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
+        {_, #{ Key := Type2 }} ->
+            meet_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
+    end;
+meet_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
 %% subtract(Type1, Type2) -> Type
 %%  Subtract Type2 from Type2. Example:
 %%      subtract(list, nil) -> cons
@@ -1677,12 +1740,12 @@ assert_type(WantedType, Term, Vst) ->
 
 assert_type(Correct, Correct) -> ok;
 assert_type(float, {float,_}) -> ok;
-assert_type(tuple, {tuple,_}) -> ok;
+assert_type(tuple, {tuple,_,_}) -> ok;
 assert_type(tuple, {literal,Tuple}) when is_tuple(Tuple) -> ok;
-assert_type({tuple_element,I}, {tuple,[Sz]})
+assert_type({tuple_element,I}, {tuple,[Sz],_})
   when 1 =< I, I =< Sz ->
     ok;
-assert_type({tuple_element,I}, {tuple,Sz})
+assert_type({tuple_element,I}, {tuple,Sz,_})
   when is_integer(Sz), 1 =< I, I =< Sz ->
     ok;
 assert_type({tuple_element,I}, {literal,Lit}) when I =< tuple_size(Lit) ->
@@ -1692,6 +1755,25 @@ assert_type(cons, {literal,[_|_]}) ->
 assert_type(Needed, Actual) ->
     error({bad_type,{needed,Needed},{actual,Actual}}).
 
+get_element_type(Key, Src, Vst) ->
+    get_element_type_1(Key, get_durable_term_type(Src, Vst)).
+
+get_element_type_1(Index, {tuple,Sz,Es}) ->
+    case Es of
+        #{ Index := Type } -> Type;
+        #{} when Index =< Sz -> term;
+        #{} -> none
+    end;
+get_element_type_1(_Index, _Type) ->
+    term.
+
+set_element_type(_Key, none, Es) ->
+    Es;
+set_element_type(Key, term, Es) ->
+    maps:remove(Key, Es);
+set_element_type(Key, Type, Es) ->
+    Es#{ Key => Type }.
+
 get_tuple_size({integer,[]}) -> 0;
 get_tuple_size({integer,Sz}) -> Sz;
 get_tuple_size(_) -> 0.
@@ -1739,16 +1821,6 @@ get_term_type(Src, Vst) ->
 get_special_y_type({y,_}=Reg, Vst) -> get_term_type_1(Reg, Vst);
 get_special_y_type(Src, _) -> error({source_not_y_reg,Src}).
 
-get_term_type_1(nil=T, _) -> T;
-get_term_type_1({atom,A}=T, _) when is_atom(A) -> T;
-get_term_type_1({float,F}=T, _) when is_float(F) -> T;
-get_term_type_1({integer,I}=T, _) when is_integer(I) -> T;
-get_term_type_1({literal,[_|_]}, _) -> cons;
-get_term_type_1({literal,Bitstring}, _) when is_bitstring(Bitstring) -> binary;
-get_term_type_1({literal,Map}, _) when is_map(Map) -> map;
-get_term_type_1({literal,Tuple}, _) when is_tuple(Tuple) ->
-    {tuple,tuple_size(Tuple)};
-get_term_type_1({literal,_}=T, _) -> T;
 get_term_type_1({x,X}=Reg, #vst{current=#st{x=Xs}}) when is_integer(X) ->
     case gb_trees:lookup(X, Xs) of
 	{value,Type} -> Type;
@@ -1760,7 +1832,8 @@ get_term_type_1({y,Y}=Reg, #vst{current=#st{y=Ys}}) when is_integer(Y) ->
 	{value,uninitialized} -> error({uninitialized_reg,Reg});
 	{value,Type} -> Type
     end;
-get_term_type_1(Src, _) -> error({bad_source,Src}).
+get_term_type_1(Src, _) ->
+    get_literal_type(Src).
 
 get_def(Src, #vst{current=#st{defs=Defs}}) ->
     case Defs of
@@ -1768,23 +1841,41 @@ get_def(Src, #vst{current=#st{defs=Defs}}) ->
         #{} -> none
     end.
 
-%% get_literal(Src) -> literal_value().
-get_literal(nil) -> [];
-get_literal({atom,A}) when is_atom(A) -> A;
-get_literal({float,F}) when is_float(F) -> F;
-get_literal({integer,I}) when is_integer(I) -> I;
-get_literal({literal,L}) -> L;
-get_literal(T) -> error({not_literal,T}).
-
-branch_arities([Sz,{f,L}|T], Tuple, {tuple,[_]}=Type0, Vst0) when is_integer(Sz) ->
-    Vst1 = set_aliased_type({tuple,Sz}, Tuple, Vst0),
+get_literal_type(nil=T) -> T;
+get_literal_type({atom,A}=T) when is_atom(A) -> T;
+get_literal_type({float,F}=T) when is_float(F) -> T;
+get_literal_type({integer,I}=T) when is_integer(I) -> T;
+get_literal_type({literal,[_|_]}) -> cons;
+get_literal_type({literal,Bitstring}) when is_bitstring(Bitstring) -> binary;
+get_literal_type({literal,Map}) when is_map(Map) -> map;
+get_literal_type({literal,Tuple}) when is_tuple(Tuple) -> value_to_type(Tuple);
+get_literal_type({literal,_}) -> term;
+get_literal_type(T) -> error({not_literal,T}).
+
+value_to_type([]) -> nil;
+value_to_type(A) when is_atom(A) -> {atom, A};
+value_to_type(F) when is_float(F) -> {float, F};
+value_to_type(I) when is_integer(I) -> {integer, I};
+value_to_type(T) when is_tuple(T) ->
+     {Es,_} = foldl(fun(Val, {Es0, Index}) ->
+                            Type = value_to_type(Val),
+                            Es = set_element_type(Index, Type, Es0),
+                            {Es, Index + 1}
+                    end, {#{}, 1}, tuple_to_list(T)),
+     {tuple, tuple_size(T), Es};
+value_to_type(L) -> {literal, L}.
+
+branch_arities([Sz,{f,L}|T], Tuple, {tuple,[_],Es0}=Type0, Vst0) when is_integer(Sz) ->
+    %% Filter out element types that are no longer valid.
+    Es = maps:filter(fun(Index, _Type) -> Index =< Sz end, Es0),
+    Vst1 = set_aliased_type({tuple,Sz,Es}, Tuple, Vst0),
     Vst = branch_state(L, Vst1),
     branch_arities(T, Tuple, Type0, Vst);
-branch_arities([Sz,{f,L}|T], Tuple, {tuple,Sz}=Type, Vst0) when is_integer(Sz) ->
+branch_arities([Sz,{f,L}|T], Tuple, {tuple,Sz,_Es}=Type, Vst0) when is_integer(Sz) ->
     %% The type is already correct. (This test is redundant.)
     Vst = branch_state(L, Vst0),
     branch_arities(T, Tuple, Type, Vst);
-branch_arities([Sz0,{f,_}|T], Tuple, {tuple,Sz}=Type, Vst)
+branch_arities([Sz0,{f,_}|T], Tuple, {tuple,Sz,_Es}=Type, Vst)
   when is_integer(Sz), Sz0 =/= Sz ->
     %% We already have an established different exact size for the tuple.
     %% This label can't possibly be reached.
@@ -1898,9 +1989,14 @@ join({catchtag,T0},{catchtag,T1}) ->
     {catchtag,ordsets:from_list(T0++T1)};
 join({trytag,T0},{trytag,T1}) ->
     {trytag,ordsets:from_list(T0++T1)};
-join({tuple,A}, {tuple,B}) ->
-    {tuple,[min(tuple_sz(A), tuple_sz(B))]};
-join({Type,A}, {Type,B}) 
+join({tuple,Size,EsA}, {tuple,Size,EsB}) ->
+    Es = join_tuple_elements(tuple_sz(Size), EsA, EsB),
+    {tuple, Size, Es};
+join({tuple,A,EsA}, {tuple,B,EsB}) ->
+    Size = [min(tuple_sz(A), tuple_sz(B))],
+    Es = join_tuple_elements(Size, EsA, EsB),
+    {tuple, Size, Es};
+join({Type,A}, {Type,B})
   when Type =:= atom; Type =:= integer; Type =:= float ->
     if A =:= B -> {Type,A};
        true -> {Type,[]}
@@ -1912,9 +2008,9 @@ join(number, {Type,_})
   when Type =:= integer; Type =:= float ->
     number;
 join(bool, {atom,A}) ->
-    merge_bool(A);
+    join_bool(A);
 join({atom,A}, bool) ->
-    merge_bool(A);
+    join_bool(A);
 join({atom,_}, {atom,_}) ->
     {atom,[]};
 join(#ms{id=Id1,valid=B1,slots=Slots1},
@@ -1929,19 +2025,35 @@ join(T1, T2) when T1 =/= T2 ->
     %% a 'term'.
     join_list(T1, T2).
 
-%% Merges types of literals. Note that the left argument must either be a
+join_tuple_elements(Size, EsA, EsB) ->
+    Es0 = join_elements(EsA, EsB),
+    MinSize = tuple_sz(Size),
+    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
+
+join_elements(Es1, Es2) ->
+    Keys = if
+               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
+               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
+           end,
+    join_elements_1(Keys, Es1, Es2, #{}).
+
+join_elements_1([Key | Keys], Es1, Es2, Acc0) ->
+    Type = case {Es1, Es2} of
+               {#{ Key := Same }, #{ Key := Same }} -> Same;
+               {#{ Key := Type1 }, #{ Key := Type2 }} -> join(Type1, Type2);
+               {#{}, #{}} -> term
+           end,
+    Acc = set_element_type(Key, Type, Acc0),
+    join_elements_1(Keys, Es1, Es2, Acc);
+join_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
+%% Joins types of literals; note that the left argument must either be a
 %% literal or exactly equal to the second argument.
 join_literal(Same, Same) ->
     Same;
-join_literal({literal,[_|_]}, T) ->
-    join_literal(T, cons);
-join_literal({literal,#{}}, T) ->
-    join_literal(T, map);
-join_literal({literal,Tuple}, T) when is_tuple(Tuple) ->
-    join_literal(T, {tuple, tuple_size(Tuple)});
-join_literal({literal,_}, T) ->
-    %% Bitstring, fun, or similar.
-    join_literal(T, term);
+join_literal({literal,_}=Lit, T) ->
+    join_literal(T, get_literal_type(Lit));
 join_literal(T1, T2) ->
     %% We're done extracting the types, try merging them again.
     join(T1, T2).
@@ -1955,14 +2067,14 @@ join_list(_, _) ->
     %% Not a list, so it must be a term.
     term.
 
+join_bool([]) -> {atom,[]};
+join_bool(true) -> bool;
+join_bool(false) -> bool;
+join_bool(_) -> {atom,[]}.
+
 tuple_sz([Sz]) -> Sz;
 tuple_sz(Sz) -> Sz.
 
-merge_bool([]) -> {atom,[]};
-merge_bool(true) -> bool;
-merge_bool(false) -> bool;
-merge_bool(_) -> {atom,[]}.
-
 merge_aliases(Al0, Al1) when map_size(Al0) =< map_size(Al1) ->
     maps:filter(fun(K, V) ->
                         case Al1 of
@@ -2165,26 +2277,27 @@ return_type({extfunc,M,F,A}, Vst) -> return_type_1(M, F, A, Vst);
 return_type(_, _) -> term.
 
 return_type_1(erlang, setelement, 3, Vst) ->
-    Tuple = {x,1},
+    IndexType = get_term_type({x,0}, Vst),
     TupleType =
-	case get_term_type(Tuple, Vst) of
-	    {tuple,_}=TT ->
-		TT;
-	    {literal,Lit} when is_tuple(Lit) ->
-		{tuple,tuple_size(Lit)};
-	    _ ->
-		{tuple,[0]}
-	end,
-    case get_term_type({x,0}, Vst) of
-        {integer,[]} ->
-            TupleType;
-        {integer,I} ->
-            case meet({tuple,[I]}, TupleType) of
-                none -> TupleType;
-                T -> T
+        case get_term_type({x,1}, Vst) of
+            {literal,Tuple}=Lit when is_tuple(Tuple) -> get_literal_type(Lit);
+            {tuple,_,_}=TT -> TT;
+            _ -> {tuple,[0],#{}}
+        end,
+    case IndexType of
+        {integer,I} when is_integer(I) ->
+            case meet({tuple,[I],#{}}, TupleType) of
+                {tuple, Sz, Es0} ->
+                    ValueType = get_term_type({x,2}, Vst),
+                    Es = set_element_type(I, ValueType, Es0),
+                    {tuple, Sz, Es};
+                none ->
+                    TupleType
             end;
         _ ->
-            TupleType
+            %% The index could point anywhere, so we must discard all element
+            %% information.
+            setelement(3, TupleType, #{})
     end;
 return_type_1(erlang, '++', 2, Vst) ->
     case get_term_type({x,0}, Vst) =:= cons orelse
diff --git a/lib/compiler/test/match_SUITE.erl b/lib/compiler/test/match_SUITE.erl
index 60ab969929..94bfbb0efe 100644
--- a/lib/compiler/test/match_SUITE.erl
+++ b/lib/compiler/test/match_SUITE.erl
@@ -25,7 +25,7 @@
 	 match_in_call/1,untuplify/1,shortcut_boolean/1,letify_guard/1,
 	 selectify/1,deselectify/1,underscore/1,match_map/1,map_vars_used/1,
 	 coverage/1,grab_bag/1,literal_binary/1,
-         unary_op/1,eq_types/1]).
+         unary_op/1,eq_types/1,match_after_return/1]).
 	 
 -include_lib("common_test/include/ct.hrl").
 
@@ -40,7 +40,8 @@ groups() ->
        match_in_call,untuplify,
        shortcut_boolean,letify_guard,selectify,deselectify,
        underscore,match_map,map_vars_used,coverage,
-       grab_bag,literal_binary,unary_op,eq_types]}].
+       grab_bag,literal_binary,unary_op,eq_types,
+       match_after_return]}].
 
 
 init_per_suite(Config) ->
@@ -890,5 +891,15 @@ eq_types(A, B) ->
 
     Ref22.
 
+match_after_return(Config) when is_list(Config) ->
+    %% The return type of the following call will never match the 'wont_happen'
+    %% clauses below, and the beam_ssa_type was clever enough to see that but
+    %% didn't remove the blocks, so it crashed when trying to extract A.
+    ok = case mar_test_tuple(erlang:unique_integer()) of
+            {gurka, never_matches, A} -> {wont_happen, A};
+            _ -> ok
+         end.
+
+mar_test_tuple(I) -> {gurka, I}.
 
 id(I) -> I.