compiler: Introduce union types

Consider the type `{ok, #record{}} | {error,atom()}`; in our
current type representation this will be flattened down to
`{ok | error, #record{} | atom()}`, which is fairly useful but has
no connection between the elements. Testing that the first element
is 'error' lets us skip checking that it's 'ok' on failure, but the
second element is still `#record{} | atom()` and we'll eventually
need to test that, even though it can only be a `#record{}`.

Another example would be `false | {value, term()}`, the return
value of lists:keyfind/3, which we're forced to flatten to `any`
since there's nothing in common between an atom and a tuple.

Union types let us express these types directly, greatly improving
type optimization.

6 files changed, 751 insertions, 340 deletions

diff --git a/lib/compiler/src/beam_call_types.erl b/lib/compiler/src/beam_call_types.erl
index 2aba6f7961..a94a7caa74 100644
--- a/lib/compiler/src/beam_call_types.erl
+++ b/lib/compiler/src/beam_call_types.erl
@@ -37,7 +37,7 @@
 -spec types(Mod, Func, ArgTypes) -> {RetType, ArgTypes, CanSubtract} when
       Mod :: atom(),
       Func :: atom(),
-      ArgTypes :: [type()],
+      ArgTypes :: [normal_type()],
       RetType :: type(),
       CanSubtract :: boolean().
 
diff --git a/lib/compiler/src/beam_ssa_type.erl b/lib/compiler/src/beam_ssa_type.erl
index 5e7b54a064..f4fc33bf4f 100644
--- a/lib/compiler/src/beam_ssa_type.erl
+++ b/lib/compiler/src/beam_ssa_type.erl
@@ -84,7 +84,8 @@ join_arg_types(Args, ArgTypes, Anno) ->
               end, Ts0, ParamTypes).
 
 join_arg_types_1([Arg | Args], [TM | TMs], Ts) when map_size(TM) =/= 0 ->
-    join_arg_types_1(Args, TMs, Ts#{ Arg => beam_types:join(maps:values(TM))});
+    Type = beam_types:join(maps:values(TM)),
+    join_arg_types_1(Args, TMs, Ts#{ Arg => Type });
 join_arg_types_1([Arg | Args], [_TM | TMs], Ts) ->
     join_arg_types_1(Args, TMs, Ts#{ Arg => any });
 join_arg_types_1([], [], Ts) ->
@@ -388,9 +389,9 @@ opt_call(#b_set{dst=Dst,args=[#b_local{}=Callee|Args]}=I0, D, Ts0, Ds0, Fdb0) ->
             %% Match contexts are treated as bitstrings when optimizing
             %% arguments, as we don't yet support removing the
             %% "bs_start_match3" instruction.
-            Types = [case get_type(Arg, Ts) of
-                          #t_bs_context{} -> #t_bitstring{};
-                          Type -> Type
+            Types = [case raw_type(Arg, Ts) of
+                         #t_bs_context{} -> #t_bitstring{};
+                         Type -> Type
                      end || Arg <- Args],
 
             %% Update the argument types of *this exact call*, the types
@@ -443,7 +444,7 @@ opt_make_fun(#b_set{op=make_fun,
         #{ Callee := #func_info{exported=false,arg_types=ArgTypes0}=Info } ->
             ArgCount = Callee#b_local.arity - length(FreeVars),
 
-            FVTypes = [get_type(FreeVar, Ts) || FreeVar <- FreeVars],
+            FVTypes = [raw_type(FreeVar, Ts) || FreeVar <- FreeVars],
             Types = duplicate(ArgCount, any) ++ FVTypes,
 
             CallId = {D#d.func_id, Dst},
@@ -486,8 +487,10 @@ simplify(#b_set{op={bif,'or'},args=Args}=I, Ts) ->
             I
     end;
 simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I0, Ts) ->
-    case beam_types:get_tuple_size(get_type(Tuple, Ts)) of
-        {_,Size} when is_integer(Index), 1 =< Index, Index =< Size ->
+    case normalized_type(Tuple, Ts) of
+        #t_tuple{size=Size} when is_integer(Index),
+                                 1 =< Index,
+                                 Index =< Size ->
             I = I0#b_set{op=get_tuple_element,
                          args=[Tuple,#b_literal{val=Index-1}]},
             simplify(I, Ts);
@@ -495,28 +498,28 @@ simplify(#b_set{op={bif,element},args=[#b_literal{val=Index},Tuple]}=I0, Ts) ->
             eval_bif(I0, Ts)
     end;
 simplify(#b_set{op={bif,hd},args=[List]}=I, Ts) ->
-    case get_type(List, Ts) of
+    case normalized_type(List, Ts) of
         cons ->
             I#b_set{op=get_hd};
         _ ->
             eval_bif(I, Ts)
     end;
 simplify(#b_set{op={bif,tl},args=[List]}=I, Ts) ->
-    case get_type(List, Ts) of
+    case normalized_type(List, Ts) of
         cons ->
             I#b_set{op=get_tl};
         _ ->
             eval_bif(I, Ts)
     end;
 simplify(#b_set{op={bif,size},args=[Term]}=I, Ts) ->
-    case get_type(Term, Ts) of
+    case normalized_type(Term, Ts) of
         #t_tuple{} ->
             simplify(I#b_set{op={bif,tuple_size}}, Ts);
         _ ->
             eval_bif(I, Ts)
     end;
 simplify(#b_set{op={bif,tuple_size},args=[Term]}=I, Ts) ->
-    case get_type(Term, Ts) of
+    case normalized_type(Term, Ts) of
         #t_tuple{size=Size,exact=true} ->
             #b_literal{val=Size};
         _ ->
@@ -524,7 +527,7 @@ simplify(#b_set{op={bif,tuple_size},args=[Term]}=I, Ts) ->
     end;
 simplify(#b_set{op={bif,is_function},args=[Fun,#b_literal{val=Arity}]}=I, Ts)
   when is_integer(Arity), Arity >= 0 ->
-    case get_type(Fun, Ts) of
+    case normalized_type(Fun, Ts) of
         #t_fun{arity=any} ->
             I;
         #t_fun{arity=Arity} ->
@@ -535,15 +538,15 @@ simplify(#b_set{op={bif,is_function},args=[Fun,#b_literal{val=Arity}]}=I, Ts)
             #b_literal{val=false}
     end;
 simplify(#b_set{op={bif,Op0},args=Args}=I, Ts) when Op0 =:= '=='; Op0 =:= '/=' ->
-    Types = get_types(Args, Ts),
+    Types = normalized_types(Args, Ts),
     EqEq0 = case {beam_types:meet(Types),beam_types:join(Types)} of
-               {none,any} -> true;
-               {#t_integer{},#t_integer{}} -> true;
-               {float,float} -> true;
-               {#t_bitstring{},_} -> true;
-               {#t_atom{},_} -> true;
-               {_,_} -> false
-           end,
+                {none,any} -> true;
+                {#t_integer{},#t_integer{}} -> true;
+                {float,float} -> true;
+                {#t_bitstring{},_} -> true;
+                {#t_atom{},_} -> true;
+                {_,_} -> false
+            end,
     EqEq = EqEq0 orelse any_non_numeric_argument(Args, Ts),
     case EqEq of
         true ->
@@ -557,33 +560,35 @@ simplify(#b_set{op={bif,Op0},args=Args}=I, Ts) when Op0 =:= '=='; Op0 =:= '/=' -
     end;
 simplify(#b_set{op={bif,'=:='},args=[Same,Same]}, _Ts) ->
     #b_literal{val=true};
-simplify(#b_set{op={bif,'=:='},args=[A1,_A2]=Args}=I, Ts) ->
-    [T1,T2] = get_types(Args, Ts),
-    case beam_types:meet(T1, T2) of
+simplify(#b_set{op={bif,'=:='},args=[LHS,RHS]}=I, Ts) ->
+    LType = raw_type(LHS, Ts),
+    RType = raw_type(RHS, Ts),
+    case beam_types:meet(LType, RType) of
         none ->
             #b_literal{val=false};
         _ ->
-            case {beam_types:is_boolean_type(T1),T2} of
+            case {beam_types:is_boolean_type(LType),
+                  beam_types:normalize(RType)} of
                 {true,#t_atom{elements=[true]}} ->
                     %% Bool =:= true  ==>  Bool
-                    A1;
+                    LHS;
                 {true,#t_atom{elements=[false]}} ->
                     %% Bool =:= false ==> not Bool
                     %%
                     %% This will be further optimized to eliminate the
                     %% 'not', swapping the success and failure
-                    %% branches in the br instruction. If A1 comes
+                    %% branches in the br instruction. If LHS comes
                     %% from a type test (such as is_atom/1) or a
                     %% comparison operator (such as >=) that can be
                     %% translated to test instruction, this
                     %% optimization will eliminate one instruction.
-                    simplify(I#b_set{op={bif,'not'},args=[A1]}, Ts);
+                    simplify(I#b_set{op={bif,'not'},args=[LHS]}, Ts);
                 {_,_} ->
                     eval_bif(I, Ts)
             end
     end;
 simplify(#b_set{op={bif,Op},args=Args}=I, Ts) ->
-    Types = get_types(Args, Ts),
+    Types = normalized_types(Args, Ts),
     case is_float_op(Op, Types) of
         false ->
             eval_bif(I, Ts);
@@ -592,7 +597,7 @@ simplify(#b_set{op={bif,Op},args=Args}=I, Ts) ->
             eval_bif(beam_ssa:add_anno(float_op, AnnoArgs, I), Ts)
     end;
 simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=N}]}=I, Ts) ->
-    case get_type(Tuple, Ts) of
+    case normalized_type(Tuple, Ts) of
         #t_tuple{size=Size,elements=Es} when Size > N ->
             ElemType = beam_types:get_element_type(N + 1, Es),
             case beam_types:get_singleton_value(ElemType) of
@@ -605,7 +610,7 @@ simplify(#b_set{op=get_tuple_element,args=[Tuple,#b_literal{val=N}]}=I, Ts) ->
             I
     end;
 simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) ->
-    case get_type(Src, Ts) of
+    case normalized_type(Src, Ts) of
         any ->  I;
         list -> I;
         cons -> #b_literal{val=true};
@@ -613,7 +618,7 @@ simplify(#b_set{op=is_nonempty_list,args=[Src]}=I, Ts) ->
     end;
 simplify(#b_set{op=is_tagged_tuple,
                 args=[Src,#b_literal{val=Size},#b_literal{}=Tag]}=I, Ts) ->
-    simplify_is_record(I, get_type(Src, Ts), Size, Tag, Ts);
+    simplify_is_record(I, normalized_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]};
@@ -631,7 +636,7 @@ simplify(I, _Ts) -> I.
 any_non_numeric_argument([#b_literal{val=Lit}|_], _Ts) ->
     is_non_numeric(Lit);
 any_non_numeric_argument([#b_var{}=V|T], Ts) ->
-    is_non_numeric_type(get_type(V, Ts)) orelse any_non_numeric_argument(T, Ts);
+    is_non_numeric_type(raw_type(V, Ts)) orelse any_non_numeric_argument(T, Ts);
 any_non_numeric_argument([], _Ts) -> false.
 
 is_non_numeric([H|T]) ->
@@ -649,7 +654,7 @@ is_non_numeric(_) -> true.
 
 is_non_numeric_tuple(Tuple, El) when El >= 1 ->
     is_non_numeric(element(El, Tuple)) andalso
-	is_non_numeric_tuple(Tuple, El-1);
+        is_non_numeric_tuple(Tuple, El-1);
 is_non_numeric_tuple(_Tuple, 0) -> true.
 
 is_non_numeric_type(#t_atom{}) -> true;
@@ -676,9 +681,11 @@ make_literal_list([_|_], _) ->
 make_literal_list([], Acc) ->
     reverse(Acc).
 
-is_safe_bool_op(Args, Ts) ->
-    [T1,T2] = get_types(Args, Ts),
-    beam_types:is_boolean_type(T1) andalso beam_types:is_boolean_type(T2).
+is_safe_bool_op([LHS, RHS], Ts) ->
+    LType = raw_type(LHS, Ts),
+    RType = raw_type(RHS, Ts),
+    beam_types:is_boolean_type(LType) andalso
+        beam_types:is_boolean_type(RType).
 
 all_same([{H,_}|T]) ->
     all(fun({E,_}) -> E =:= H end, T).
@@ -691,7 +698,7 @@ eval_bif(#b_set{op={bif,Bif},args=Args}=I, Ts) ->
         true ->
             case make_literal_list(Args) of
                 none ->
-                    case get_types(Args, Ts) of
+                    case normalized_types(Args, Ts) of
                         [any] ->
                             I;
                         [Type] ->
@@ -724,8 +731,7 @@ simplify_arg(#b_var{}=Arg0, Sub, Ts) ->
         #b_literal{}=LitArg ->
             LitArg;
         #b_var{}=Arg ->
-            Type = get_type(Arg, Ts),
-            case beam_types:get_singleton_value(Type) of
+            case beam_types:get_singleton_value(raw_type(Arg, Ts)) of
                 {ok, Val} -> #b_literal{val=Val};
                 error -> Arg
             end
@@ -766,7 +772,7 @@ opt_terminator(#b_br{bool=#b_var{}}=Br, Ts, Ds) ->
 opt_terminator(#b_switch{arg=#b_literal{}}=Sw, _Ts, _Ds) ->
     beam_ssa:normalize(Sw);
 opt_terminator(#b_switch{arg=#b_var{}=V}=Sw, Ts, Ds) ->
-    case get_type(V, Ts) of
+    case normalized_type(V, Ts) of
         any ->
             beam_ssa:normalize(Sw);
         Type ->
@@ -796,7 +802,7 @@ opt_switch(#b_switch{fail=Fail,list=List0}=Sw0, Type, Ts, Ds) ->
 prune_switch_list([{_,Fail}|T], Fail, Type, Ts) ->
     prune_switch_list(T, Fail, Type, Ts);
 prune_switch_list([{Arg,_}=Pair|T], Fail, Type, Ts) ->
-    case beam_types:meet(get_type(Arg, Ts), Type) of
+    case beam_types:meet(raw_type(Arg, Ts), Type) of
         none ->
             %% Different types. This value can never match.
             prune_switch_list(T, Fail, Type, Ts);
@@ -860,7 +866,7 @@ update_successors(#b_ret{arg=Arg}=Last, Ts, D0) ->
                 %% type.
                 D0;
             #{} ->
-                RetType = beam_types:join([get_type(Arg, Ts) | D0#d.ret_type]),
+                RetType = beam_types:join([raw_type(Arg, Ts) | D0#d.ret_type]),
                 D0#d{ret_type=[RetType]}
         end,
     {Last, D}.
@@ -881,13 +887,13 @@ update_switch([], _V, _UsedOnce, _Ts, Acc, D) ->
     {Acc, D}.
 
 subtract_sw_list(V, List, Ts) ->
-    case sub_sw_list_1(get_type(V, Ts), List, Ts) of
+    case sub_sw_list_1(raw_type(V, Ts), List, Ts) of
         none -> none;
         Type -> Ts#{ V := Type }
     end.
 
 sub_sw_list_1(Type, [{Val,_}|T], Ts) ->
-    ValType = get_type(Val, Ts),
+    ValType = raw_type(Val, Ts),
     sub_sw_list_1(beam_types:subtract(Type, ValType), T, Ts);
 sub_sw_list_1(Type, [], _Ts) ->
     Type.
@@ -911,10 +917,11 @@ update_types(#b_set{op=Op,dst=Dst,args=Args}, Ts, Ds) ->
     Ts#{Dst=>T}.
 
 type(phi, Args, Ts, _Ds) ->
-    Types = [get_type(A, Ts) || {A,_} <- Args],
+    Types = [raw_type(A, Ts) || {A,_} <- Args],
     beam_types:join(Types);
 type({bif,Bif}, Args, Ts, _Ds) ->
-    {RetType, _, _} = beam_call_types:types(erlang, Bif, get_types(Args, Ts)),
+    ArgTypes = normalized_types(Args, Ts),
+    {RetType, _, _} = beam_call_types:types(erlang, Bif, ArgTypes),
     RetType;
 type(bs_init, _Args, _Ts, _Ds) ->
     #t_bitstring{};
@@ -927,10 +934,11 @@ type(bs_get_tail, _Args, _Ts, _Ds) ->
     #t_bitstring{};
 type(call, [#b_remote{mod=#b_literal{val=Mod},
                       name=#b_literal{val=Name}}|Args], Ts, _Ds) ->
-    {RetType, _, _} = beam_call_types:types(Mod, Name, get_types(Args, Ts)),
+    ArgTypes = normalized_types(Args, Ts),
+    {RetType, _, _} = beam_call_types:types(Mod, Name, ArgTypes),
     RetType;
 type(get_tuple_element, [Tuple, Offset], Ts, _Ds) ->
-    #t_tuple{size=Size,elements=Es} = get_type(Tuple, Ts),
+    #t_tuple{size=Size,elements=Es} = normalized_type(Tuple, Ts),
     #b_literal{val=N} = Offset,
     true = Size > N, %Assertion.
     beam_types:get_element_type(N + 1, Es);
@@ -946,7 +954,7 @@ type(put_list, _Args, _Ts, _Ds) ->
     cons;
 type(put_tuple, Args, Ts, _Ds) ->
     {Es, _} = foldl(fun(Arg, {Es0, Index}) ->
-                            Type = get_type(Arg, Ts),
+                            Type = raw_type(Arg, Ts),
                             Es = beam_types:set_element_type(Index, Type, Es0),
                             {Es, Index + 1}
                     end, {#{}, 1}, Args),
@@ -954,7 +962,7 @@ type(put_tuple, Args, Ts, _Ds) ->
 type(succeeded, [#b_var{}=Src], Ts, Ds) ->
     case maps:get(Src, Ds) of
         #b_set{op={bif,Bif},args=BifArgs} ->
-            Types = get_types(BifArgs, Ts),
+            Types = normalized_types(BifArgs, Ts),
             case {Bif,Types} of
                 {BoolOp,[T1,T2]} when BoolOp =:= 'and'; BoolOp =:= 'or' ->
                     BothBool = beam_types:is_boolean_type(T1) andalso
@@ -1151,7 +1159,7 @@ simplify_is_record(I, #t_tuple{exact=Exact,
                    {ok, _} -> no;
                    error ->
                        %% Is it at all possible for the tag to match?
-                       case beam_types:meet(get_type(RecTag, Ts), TagType) of
+                       case beam_types:meet(raw_type(RecTag, Ts), TagType) of
                            none -> no;
                            _ -> maybe
                        end
@@ -1181,7 +1189,7 @@ simplify_switch_bool(#b_switch{arg=B,fail=Fail,list=List0}, Ts, Ds) ->
 simplify_not(#b_br{bool=#b_var{}=V,succ=Succ,fail=Fail}=Br0, Ts, Ds) ->
     case Ds of
         #{V:=#b_set{op={bif,'not'},args=[Bool]}} ->
-            case beam_types:is_boolean_type(get_type(Bool, Ts)) of
+            case beam_types:is_boolean_type(raw_type(Bool, Ts)) of
                 true ->
                     Br = Br0#b_br{bool=Bool,succ=Fail,fail=Succ},
                     beam_ssa:normalize(Br);
@@ -1249,16 +1257,18 @@ used_once_last_uses([V|Vs], L, Uses) ->
     end;
 used_once_last_uses([], _, Uses) -> Uses.
 
+normalized_types(Values, Ts) ->
+    [normalized_type(Val, Ts) || Val <- Values].
+
+normalized_type(V, Ts) ->
+    beam_types:normalize(raw_type(V, Ts)).
 
-get_types(Values, Ts) ->
-    [get_type(Val, Ts) || Val <- Values].
--spec get_type(beam_ssa:value(), type_db()) -> type().
+-spec raw_type(beam_ssa:value(), type_db()) -> type().
 
-get_type(#b_var{}=V, Ts) ->
-    #{V:=T} = Ts,
-    T;
-get_type(#b_literal{val=Val}, _Ts) ->
-    beam_types:make_type_from_value(Val).
+raw_type(#b_literal{val=Value}, _Ts) ->
+    beam_types:make_type_from_value(Value);
+raw_type(V, Ts) ->
+    map_get(V, Ts).
 
 %% infer_types(Var, Types, #d{}) -> {SuccTypes,FailTypes}
 %%  Looking at the expression that defines the variable Var, infer
@@ -1332,14 +1342,14 @@ 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),
+    Type = raw_type(Lit, Ts),
     [{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
     %% be inferred that L1 is 'cons' (the meet of 'cons' and 'list').
-    Type0 = get_type(Arg0, Ts),
-    Type1 = get_type(Arg1, Ts),
+    Type0 = raw_type(Arg0, Ts),
+    Type1 = raw_type(Arg1, Ts),
     Type = beam_types:meet(Type0, Type1),
     [{V,MeetType} ||
         {V,OrigType,MeetType} <-
@@ -1355,7 +1365,7 @@ infer_eq_lit(#b_set{op=get_tuple_element,
                     args=[#b_var{}=Tuple,#b_literal{val=N}]},
              #b_literal{}=Lit) ->
     Index = N + 1,
-    Es = beam_types:set_element_type(Index, get_type(Lit, #{}), #{}),
+    Es = beam_types:set_element_type(Index, raw_type(Lit, #{}), #{}),
     [{Tuple,#t_tuple{size=Index,elements=Es}}];
 infer_eq_lit(_, _) -> [].
 
@@ -1368,7 +1378,7 @@ infer_type(succeeded, [#b_var{}=Src], Ts, Ds) ->
 %% not branching on 'succeeded'.
 infer_type(is_tagged_tuple, [#b_var{}=Src,#b_literal{val=Size},
                              #b_literal{}=Tag], _Ts, _Ds) ->
-    Es = beam_types:set_element_type(1, get_type(Tag, #{}), #{}),
+    Es = beam_types:set_element_type(1, raw_type(Tag, #{}), #{}),
     T = {Src,#t_tuple{exact=true,size=Size,elements=Es}},
     {[T], [T]};
 infer_type(is_nonempty_list, [#b_var{}=Src], _Ts, _Ds) ->
@@ -1408,7 +1418,7 @@ infer_type(_Op, _Args, _Ts, _Ds) ->
     {[], []}.
 
 infer_success_type({bif,Op}, Args, Ts, _Ds) ->
-    ArgTypes = get_types(Args, Ts),
+    ArgTypes = normalized_types(Args, Ts),
 
     {_, PosTypes0, CanSubtract} = beam_call_types:types(erlang, Op, ArgTypes),
     PosTypes = [T || {#b_var{},_}=T <- zip(Args, PosTypes0)],
diff --git a/lib/compiler/src/beam_types.erl b/lib/compiler/src/beam_types.erl
index 4f8ba0ada5..821ccd31bb 100644
--- a/lib/compiler/src/beam_types.erl
+++ b/lib/compiler/src/beam_types.erl
@@ -22,14 +22,14 @@
 
 -include("beam_types.hrl").
 
--import(lists, [foldl/3]).
+-import(lists, [foldl/3, reverse/1, reverse/2]).
 
 -export([meet/1, meet/2, join/1, join/2, subtract/2]).
 
 -export([get_singleton_value/1,
-         get_tuple_size/1,
          is_singleton_type/1,
-         is_boolean_type/1]).
+         is_boolean_type/1,
+         normalize/1]).
 
 -export([get_element_type/2, set_element_type/3]).
 
@@ -38,223 +38,276 @@
 -export([make_atom/1,
          make_boolean/0,
          make_integer/1,
-         make_integer/2,
-         make_tuple/2,
-         make_tuple/3]).
+         make_integer/2]).
 
-%% Return the "join" of Type1 and Type2. The join is a more general
-%% type than Type1 and Type2. For example:
+-define(IS_LIST_TYPE(N),
+        N =:= list orelse
+        N =:= cons orelse
+        N =:= nil).
+
+-define(IS_NUMBER_TYPE(N),
+        N =:= number orelse
+        N =:= float orelse
+        is_record(N, t_integer)).
+
+-define(TUPLE_SET_LIMIT, 20).
+
+%% Folds meet/2 over a list.
+
+-spec meet([type()]) -> type().
+
+meet([T1, T2 | Ts]) ->
+    meet([meet(T1, T2) | Ts]);
+meet([T]) -> T.
+
+%% Return the "meet" of Type1 and Type2, which is more general than Type1 and
+%% Type2. This is identical to glb/2 but can operate on and produce unions.
 %%
-%%    join(#t_integer{elements=any}, #t_integer=elements={0,3}}) ->
-%%         #t_integer{}
+%%    A = #t_union{list=nil, number=[number], other=[#t_map{}]}
+%%    B = #t_union{number=[#t_integer{}], other=[#t_map{}]}
 %%
-%% The join for two different types result in 'any', which is
-%% the top element for our type lattice:
+%%    meet(A, B) ->
+%%         #t_union{number=[#t_integer{}], other=[#t_map{}]}
 %%
-%%    join(#t_integer{}, #t_map{}) -> any
+%% The meet of two different types result in 'none', which is the bottom
+%% element for our type lattice:
+%%
+%%    meet(#t_integer{}, #t_map{}) -> none
 
--spec join(type(), type()) -> type().
+-spec meet(type(), type()) -> type().
 
-join(T, T) ->
+meet(T, T) ->
     verified_type(T);
-join(none, T) ->
+meet(any, T) ->
     verified_type(T);
-join(T, none) ->
+meet(T, any) ->
     verified_type(T);
-join(any, _) -> any;
-join(_, any) -> any;
-join(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
-    Set = ordsets:union(Set1, Set2),
-    case ordsets:size(Set) of
-        Size when Size =< ?ATOM_SET_SIZE ->
-            #t_atom{elements=Set};
-        _Size ->
-            #t_atom{elements=any}
+meet(#t_union{}=A, B) ->
+    meet_unions(A, B);
+meet(A, #t_union{}=B) ->
+    meet_unions(B, A);
+meet(A, B) ->
+    glb(A, B).
+
+meet_unions(#t_union{atom=AtomA,list=ListA,number=NumberA,
+                     tuple_set=TSetA,other=OtherA},
+            #t_union{atom=AtomB,list=ListB,number=NumberB,
+                     tuple_set=TSetB,other=OtherB}) ->
+    Union = #t_union{atom=glb(AtomA, AtomB),
+                     list=glb(ListA, ListB),
+                     number=glb(NumberA, NumberB),
+                     tuple_set=meet_tuple_sets(TSetA, TSetB),
+                     other=glb(OtherA, OtherB)},
+    shrink_union(Union);
+meet_unions(#t_union{atom=AtomA}, #t_atom{}=B) ->
+    case glb(AtomA, B) of
+        none -> none;
+        Atom -> Atom
     end;
-join(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T;
-join(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T;
-join(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) ->
-    #t_bitstring{unit=gcd(U1, U2)};
-join(#t_fun{}, #t_fun{}) ->
-    #t_fun{};
-join(#t_integer{elements={MinA,MaxA}},
-     #t_integer{elements={MinB,MaxB}}) ->
-    #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}};
-join(#t_bs_context{slots=SlotsA,valid=ValidA},
-     #t_bs_context{slots=SlotsB,valid=ValidB}) ->
-    #t_bs_context{slots=min(SlotsA, SlotsB),
-                  valid=ValidA band ValidB};
-join(#t_integer{}, #t_integer{}) -> #t_integer{};
-join(list, cons) -> list;
-join(cons, list) -> list;
-join(nil, cons) -> list;
-join(cons, nil) -> list;
-join(nil, list) -> list;
-join(list, nil) -> list;
-join(#t_integer{}, float) -> number;
-join(float, #t_integer{}) -> number;
-join(#t_integer{}, number) -> number;
-join(number, #t_integer{}) -> number;
-join(float, number) -> number;
-join(number, float) -> number;
-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.
+meet_unions(#t_union{number=NumberA}, B) when ?IS_NUMBER_TYPE(B) ->
+    case glb(NumberA, B) of
+        none -> none;
+        Number -> Number
+    end;
+meet_unions(#t_union{list=ListA}, B) when ?IS_LIST_TYPE(B) ->
+    case glb(ListA, B) of
+        none -> none;
+        List -> List
+    end;
+meet_unions(#t_union{tuple_set=Tuples}, #t_tuple{}=B) ->
+    Set = meet_tuple_sets(Tuples, new_tuple_set(B)),
+    shrink_union(#t_union{tuple_set=Set});
+meet_unions(#t_union{other=OtherA}, OtherB) ->
+    case glb(OtherA, OtherB) of
+        none -> none;
+        Other -> Other
+    end.
 
-join_tuple_elements(MinSize, EsA, EsB) ->
-    Es0 = join_elements(EsA, EsB),
-    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
+meet_tuple_sets(none, _) ->
+    none;
+meet_tuple_sets(_, none) ->
+    none;
+meet_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) ->
+    new_tuple_set(glb(A, B));
+meet_tuple_sets(#t_tuple{}=Tuple, Records) ->
+    mts_tuple(Records, Tuple, []);
+meet_tuple_sets(Records, #t_tuple{}=Tuple) ->
+    meet_tuple_sets(Tuple, Records);
+meet_tuple_sets(RecordsA, RecordsB) ->
+    mts_records(RecordsA, RecordsB).
+
+mts_tuple([{Key, Type} | Records], Tuple, Acc) ->
+    case glb(Type, Tuple) of
+        none -> mts_tuple(Records, Tuple, Acc);
+        T -> mts_tuple(Records, Tuple, [{Key, T} | Acc])
+    end;
+mts_tuple([], _Tuple, [_|_]=Acc) ->
+    reverse(Acc);
+mts_tuple([], _Tuple, []) ->
+    none.
 
-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, #{}).
+mts_records(RecordsA, RecordsB) ->
+    mts_records(RecordsA, RecordsB, []).
 
-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)
+mts_records([{Key, A} | RsA], [{Key, B} | RsB], Acc) ->
+    case glb(A, B) of
+        none -> mts_records(RsA, RsB, Acc);
+        T -> mts_records(RsA, RsB, [{Key, T} | Acc])
     end;
-join_elements_1([], _Es1, _Es2, Acc) ->
-    Acc.
+mts_records([{KeyA, _} | _ ]=RsA, [{KeyB, _} | RsB], Acc) when KeyA > KeyB ->
+    mts_records(RsA, RsB, Acc);
+mts_records([{KeyA, _} | RsA], [{KeyB, _} | _] = RsB, Acc) when KeyA < KeyB ->
+    mts_records(RsA, RsB, Acc);
+mts_records(_RsA, [], [_|_]=Acc) ->
+    reverse(Acc);
+mts_records([], _RsB, [_|_]=Acc) ->
+    reverse(Acc);
+mts_records(_RsA, _RsB, []) ->
+    none.
 
-gcd(A, B) ->
-    case A rem B of
-        0 -> B;
-        X -> gcd(B, X)
-    end.
+%% Folds join/2 over a list.
 
-%% Joins all the given types into a single type.
 -spec join([type()]) -> type().
 
-join([T1,T2|Ts]) ->
-    join([join(T1, T2)|Ts]);
+join([T1, T2| Ts]) ->
+    join([join(T1, T2) | Ts]);
 join([T]) -> T.
 
-%% Return the "meet" of Type1 and Type2. The meet is a narrower
-%% type than Type1 and Type2. For example:
-%%
-%%    meet(#t_integer{elements=any}, #t_integer{elements={0,3}}) ->
-%%         #t_integer{elements={0,3}}
-%%
-%% The meet for two different types result in 'none', which is
-%% the bottom element for our type lattice:
+%% Return the "join" of Type1 and Type2, which is more general than Type1 and
+%% Type2. This is identical to lub/2 but can operate on and produce unions.
 %%
-%%    meet(#t_integer{}, #t_map{}) -> none
+%%    join(#t_integer{}, #t_map{}) -> #t_union{number=[#t_integer{}],
+%%                                             other=[#t_map{}]}
 
--spec meet(type(), type()) -> type().
+-spec join(type(), type()) -> type().
 
-meet(T, T) ->
-    verified_type(T);
-meet(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
-    case ordsets:intersection(Set1, Set2) of
-        [] ->
-            none;
-        [_|_]=Set ->
-            #t_atom{elements=Set}
+join(T, T) -> T;
+join(_T, any) -> any;
+join(any, _T) -> any;
+join(T, none) -> T;
+join(none, T) -> T;
+
+join(#t_union{}=A, B) ->
+    join_unions(A, B);
+join(A, #t_union{}=B) ->
+    join_unions(B, A);
+
+%% Union creation...
+join(#t_atom{}=A, #t_atom{}=B) ->
+    lub(A, B);
+join(#t_atom{}=A, B) when ?IS_LIST_TYPE(B) ->
+    #t_union{atom=A,list=B};
+join(#t_atom{}=A, B) when ?IS_NUMBER_TYPE(B) ->
+    #t_union{atom=A,number=B};
+join(#t_atom{}=A, #t_tuple{}=B) ->
+    #t_union{atom=A,tuple_set=new_tuple_set(B)};
+join(#t_atom{}=A, B) ->
+    #t_union{atom=A,other=B};
+join(A, #t_atom{}=B) ->
+    join(B, A);
+
+join(A, B) when ?IS_LIST_TYPE(A), ?IS_LIST_TYPE(B) ->
+    lub(A, B);
+join(A, B) when ?IS_LIST_TYPE(A), ?IS_NUMBER_TYPE(B) ->
+    #t_union{list=A,number=B};
+join(A, #t_tuple{}=B) when ?IS_LIST_TYPE(A) ->
+    #t_union{list=A,tuple_set=new_tuple_set(B)};
+join(A, B) when ?IS_LIST_TYPE(A) ->
+    #t_union{list=A,other=B};
+join(A, B) when ?IS_LIST_TYPE(B) ->
+    join(B, A);
+
+join(A, B) when ?IS_NUMBER_TYPE(A), ?IS_NUMBER_TYPE(B) ->
+    lub(A, B);
+join(A, #t_tuple{}=B) when ?IS_NUMBER_TYPE(A) ->
+    #t_union{number=A,tuple_set=new_tuple_set(B)};
+join(A, B) when ?IS_NUMBER_TYPE(A) ->
+    #t_union{number=A,other=B};
+join(A, B) when ?IS_NUMBER_TYPE(B) ->
+    join(B, A);
+
+join(#t_tuple{}=A, #t_tuple{}=B) ->
+    case {record_key(A), record_key(B)} of
+        {Same, Same} ->
+            lub(A, B);
+        {none, _Key} ->
+            lub(A, B);
+        {_Key, none} ->
+            lub(A, B);
+        {KeyA, KeyB} when KeyA < KeyB ->
+            #t_union{tuple_set=[{KeyA, A}, {KeyB, B}]};
+        {KeyA, KeyB} when KeyA > KeyB ->
+            #t_union{tuple_set=[{KeyB, B}, {KeyA, A}]}
     end;
-meet(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) ->
-    T;
-meet(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) ->
-    T;
-meet(#t_bs_context{slots=SlotCountA,valid=ValidSlotsA},
-     #t_bs_context{slots=SlotCountB,valid=ValidSlotsB}) ->
-    CommonSlotMask = (1 bsl min(SlotCountA, SlotCountB)) - 1,
-    CommonSlotsA = ValidSlotsA band CommonSlotMask,
-    CommonSlotsB = ValidSlotsB band CommonSlotMask,
-    if
-        CommonSlotsA =:= CommonSlotsB ->
-            #t_bs_context{slots=max(SlotCountA, SlotCountB),
-                          valid=ValidSlotsA bor ValidSlotsB};
-        CommonSlotsA =/= CommonSlotsB ->
-            none
-    end;
-meet(#t_fun{arity=any}, #t_fun{}=T) ->
-    T;
-meet(#t_fun{}=T, #t_fun{arity=any}) ->
-    T;
-meet(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) ->
-    T;
-meet(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) ->
-    T;
-meet(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}})
-  when MinA >= MinB, MinA =< MaxB;
-       MinB >= MinA, MinB =< MaxA ->
-    true = MinA =< MaxA andalso MinB =< MaxB,   %Assertion.
-    #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}};
-meet(#t_integer{}=T, number) -> T;
-meet(float=T, number) -> T;
-meet(number, #t_integer{}=T) -> T;
-meet(number, float=T) -> T;
-meet(list, cons) -> cons;
-meet(list, nil) -> nil;
-meet(cons, list) -> cons;
-meet(nil, list) -> nil;
-meet(#t_tuple{}=T1, #t_tuple{}=T2) ->
-    meet_tuples(T1, T2);
-meet(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) ->
-    #t_bitstring{unit=U1 * U2 div gcd(U1, U2)};
-meet(any, T) ->
-    verified_type(T);
-meet(T, any) ->
-    verified_type(T);
-meet(_, _) ->
-    %% Inconsistent types. There will be an exception at runtime.
-    none.
-
-meet_tuples(#t_tuple{size=Sz1,exact=true},
-            #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 ->
-    none;
-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,
-    case meet_elements(Es1, Es2) of
-        none ->
-            none;
-        Es ->
-            #t_tuple{size=Size,exact=Exact,elements=Es}
+join(#t_tuple{}=A, B) ->
+    %% All other combinations have been tried already, so B must be 'other'
+    #t_union{tuple_set=new_tuple_set(A),other=B};
+join(A, #t_tuple{}=B) ->
+    join(B, A);
+
+join(A, B) ->
+    lub(A, B).
+
+join_unions(#t_union{atom=AtomA,list=ListA,number=NumberA,
+                     tuple_set=TSetA,other=OtherA},
+            #t_union{atom=AtomB,list=ListB,number=NumberB,
+                     tuple_set=TSetB,other=OtherB}) ->
+    Union = #t_union{atom=lub(AtomA, AtomB),
+                     list=lub(ListA, ListB),
+                     number=lub(NumberA, NumberB),
+                     tuple_set=join_tuple_sets(TSetA, TSetB),
+                     other=lub(OtherA, OtherB)},
+    shrink_union(Union);
+join_unions(#t_union{atom=AtomA}=A, #t_atom{}=B) ->
+    A#t_union{atom=lub(AtomA, B)};
+join_unions(#t_union{list=ListA}=A, B) when ?IS_LIST_TYPE(B) ->
+    A#t_union{list=lub(ListA, B)};
+join_unions(#t_union{number=NumberA}=A, B) when ?IS_NUMBER_TYPE(B) ->
+    A#t_union{number=lub(NumberA, B)};
+join_unions(#t_union{tuple_set=TSetA}=A, #t_tuple{}=B) ->
+    Set = join_tuple_sets(TSetA, new_tuple_set(B)),
+    shrink_union(A#t_union{tuple_set=Set});
+join_unions(#t_union{other=OtherA}=A, B) ->
+    case lub(OtherA, B) of
+        any -> any;
+        T -> A#t_union{other=T}
     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) ->
+join_tuple_sets(A, none) ->
+    A;
+join_tuple_sets(none, B) ->
+    B;
+join_tuple_sets(#t_tuple{}=A, #t_tuple{}=B) ->
+    lub(A, B);
+join_tuple_sets(#t_tuple{}=Tuple, Records) ->
+    jts_tuple(Records, Tuple);
+join_tuple_sets(Records, #t_tuple{}=Tuple) ->
+    join_tuple_sets(Tuple, Records);
+join_tuple_sets(RecordsA, RecordsB) ->
+    jts_records(RecordsA, RecordsB).
+
+jts_tuple([{_Key, Tuple} | Records], Acc) ->
+    jts_tuple(Records, lub(Tuple, Acc));
+jts_tuple([], Acc) ->
     Acc.
 
-%% Meets all the given types into a single type.
--spec meet([type()]) -> type().
-
-meet([T1,T2|Ts]) ->
-    meet([meet(T1, T2)|Ts]);
-meet([T]) -> T.
+jts_records(RsA, RsB) ->
+    jts_records(RsA, RsB, 0, []).
+
+jts_records(RsA, RsB, N, Acc) when N > ?TUPLE_SET_LIMIT ->
+    A = normalize_tuple_set(RsA, none),
+    B = normalize_tuple_set(RsB, A),
+    #t_tuple{} = normalize_tuple_set(Acc, B);
+jts_records([{Key, A} | RsA], [{Key, B} | RsB], N, Acc) ->
+    jts_records(RsA, RsB, N + 1, [{Key, lub(A, B)} | Acc]);
+jts_records([{KeyA, _} | _]=RsA, [{KeyB, B} | RsB], N, Acc) when KeyA > KeyB ->
+    jts_records(RsA, RsB, N + 1, [{KeyB, B} | Acc]);
+jts_records([{KeyA, A} | RsA], [{KeyB, _} | _] = RsB, N, Acc) when KeyA < KeyB ->
+    jts_records(RsA, RsB, N + 1, [{KeyA, A} | Acc]);
+jts_records([], RsB, _N, Acc) ->
+    reverse(Acc, RsB);
+jts_records(RsA, [], _N, Acc) ->
+    reverse(Acc, RsA).
 
 %% Subtract Type2 from Type1. Example:
 %%    subtract(list, cons) -> nil
@@ -270,38 +323,28 @@ subtract(number, float) -> #t_integer{};
 subtract(number, #t_integer{elements=any}) -> float;
 subtract(list, cons) -> nil;
 subtract(list, nil) -> cons;
-subtract(T, _) -> T.
 
-%% Verifies that the given type is well-formed.
-
--spec verified_type(T) -> T when
-      T :: type().
+subtract(#t_union{atom=Atom}=A, #t_atom{}=B)->
+    shrink_union(A#t_union{atom=subtract(Atom, B)});
+subtract(#t_union{number=Number}=A, B) when ?IS_NUMBER_TYPE(B) ->
+    shrink_union(A#t_union{number=subtract(Number, B)});
+subtract(#t_union{list=List}=A, B) when ?IS_LIST_TYPE(B) ->
+    shrink_union(A#t_union{list=subtract(List, B)});
+subtract(#t_union{tuple_set=[_|_]=Records0}=A, #t_tuple{}=B) ->
+    %% Filter out all records that are strictly more specific than B.
+    NewSet = case [{Key, T} || {Key, T} <- Records0, meet(T, B) =/= T] of
+                 [_|_]=Records -> Records;
+                 [] -> none
+             end,
+    shrink_union(A#t_union{tuple_set=NewSet});
+subtract(#t_union{tuple_set=#t_tuple{}=Tuple}=A, #t_tuple{}=B) ->
+    %% Exclude Tuple if it's strictly more specific than B.
+    case meet(Tuple, B) of
+        Tuple -> shrink_union(A#t_union{tuple_set=none});
+        _ -> A
+    end;
 
-verified_type(any=T) -> T;
-verified_type(none=T) -> T;
-verified_type(#t_atom{elements=any}=T) -> T;
-verified_type(#t_atom{elements=[_|_]}=T) -> T;
-verified_type(#t_bitstring{unit=U}=T) when is_integer(U), U >= 1 -> T;
-verified_type(#t_bs_context{}=T) -> T;
-verified_type(#t_fun{arity=Arity}=T) when Arity =:= any; is_integer(Arity) -> T;
-verified_type(#t_integer{elements=any}=T) -> T;
-verified_type(#t_integer{elements={Min,Max}}=T)
-  when is_integer(Min), is_integer(Max), Min =< Max -> T;
-verified_type(list=T) -> T;
-verified_type(#t_map{}=T) -> T;
-verified_type(nil=T) -> T;
-verified_type(cons=T) -> T;
-verified_type(number=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.
+subtract(T, _) -> T.
 
 %%%
 %%% Type operators
@@ -319,23 +362,15 @@ get_singleton_value(nil) ->
 get_singleton_value(_) ->
     error.
 
--spec get_tuple_size(Type) -> Result when
-      Type :: type(),
-      Result :: none | {at_least, Size} | {exact, Size},
-      Size :: non_neg_integer().
-get_tuple_size(#t_tuple{size=Size,exact=false}) ->
-    {at_least,Size};
-get_tuple_size(#t_tuple{size=Size,exact=true}) ->
-    {exact,Size};
-get_tuple_size(_) ->
-    none.
-
 -spec is_boolean_type(type()) -> boolean().
 is_boolean_type(#t_atom{elements=[F,T]}) ->
     F =:= false andalso T =:= true;
 is_boolean_type(#t_atom{elements=[B]}) ->
     is_boolean(B);
-is_boolean_type(_) -> false.
+is_boolean_type(#t_union{}=T) ->
+    is_boolean_type(normalize(T));
+is_boolean_type(_) ->
+    false.
 
 -spec is_singleton_type(type()) -> boolean().
 is_singleton_type(Type) ->
@@ -361,6 +396,23 @@ get_element_type(Index, Es) ->
         #{} -> any
     end.
 
+-spec normalize(type()) -> normal_type().
+normalize(#t_union{atom=Atom,list=List,number=Number,
+                   tuple_set=Tuples,other=Other}) ->
+    A = lub(Atom, List),
+    B = lub(A, Number),
+    C = lub(B, Other),
+    normalize_tuple_set(Tuples, C);
+normalize(T) ->
+    verified_normal_type(T).
+
+normalize_tuple_set([{_, A} | Records], B) ->
+    normalize_tuple_set(Records, lub(A, B));
+normalize_tuple_set([], B) ->
+    B;
+normalize_tuple_set(A, B) ->
+    lub(A, B).
+
 %%%
 %%% Type constructors
 %%%
@@ -408,17 +460,319 @@ make_integer(Int) when is_integer(Int) ->
 make_integer(Min, Max) when is_integer(Min), is_integer(Max), Min =< Max ->
     #t_integer{elements={Min,Max}}.
 
--spec make_tuple(Size, Exact) -> type() when
-      Size :: non_neg_integer(),
-      Exact :: boolean().
-make_tuple(Size, Exact) ->
-    make_tuple(Size, Exact, #{}).
-
--spec make_tuple(Size, Exact, Elements) -> type() when
-      Size :: non_neg_integer(),
-      Exact :: boolean(),
-      Elements :: #{ non_neg_integer() => type() }.
-make_tuple(Size, Exact, Elements) ->
-    #t_tuple{size=Size,
-             exact=Exact,
-             elements=Elements}.
+%%%
+%%% Helpers
+%%%
+
+%% Return the greatest lower bound of the types Type1 and Type2. The GLB is a
+%% more specific type than Type1 and Type2, and is always a normal type.
+%%
+%%    glb(#t_integer{elements=any}, #t_integer{elements={0,3}}) ->
+%%         #t_integer{elements={0,3}}
+%%
+%% The GLB of two different types result in 'none', which is the bottom
+%% element for our type lattice:
+%%
+%%    glb(#t_integer{}, #t_map{}) -> none
+
+-spec glb(normal_type(), normal_type()) -> normal_type().
+
+glb(T, T) ->
+    verified_normal_type(T);
+glb(any, T) ->
+    verified_normal_type(T);
+glb(T, any) ->
+    verified_normal_type(T);
+glb(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
+    case ordsets:intersection(Set1, Set2) of
+        [] ->
+            none;
+        [_|_]=Set ->
+            #t_atom{elements=Set}
+    end;
+glb(#t_atom{elements=[_|_]}=T, #t_atom{elements=any}) ->
+    T;
+glb(#t_atom{elements=any}, #t_atom{elements=[_|_]}=T) ->
+    T;
+glb(#t_bs_context{slots=SlotCountA,valid=ValidSlotsA},
+    #t_bs_context{slots=SlotCountB,valid=ValidSlotsB}) ->
+    CommonSlotMask = (1 bsl min(SlotCountA, SlotCountB)) - 1,
+    CommonSlotsA = ValidSlotsA band CommonSlotMask,
+    CommonSlotsB = ValidSlotsB band CommonSlotMask,
+    if
+        CommonSlotsA =:= CommonSlotsB ->
+            #t_bs_context{slots=max(SlotCountA, SlotCountB),
+                          valid=ValidSlotsA bor ValidSlotsB};
+        CommonSlotsA =/= CommonSlotsB ->
+            none
+    end;
+glb(#t_fun{arity=any}, #t_fun{}=T) ->
+    T;
+glb(#t_fun{}=T, #t_fun{arity=any}) ->
+    T;
+glb(#t_integer{elements={_,_}}=T, #t_integer{elements=any}) ->
+    T;
+glb(#t_integer{elements=any}, #t_integer{elements={_,_}}=T) ->
+    T;
+glb(#t_integer{elements={MinA,MaxA}}, #t_integer{elements={MinB,MaxB}})
+  when MinA >= MinB, MinA =< MaxB;
+       MinB >= MinA, MinB =< MaxA ->
+    true = MinA =< MaxA andalso MinB =< MaxB,   %Assertion.
+    #t_integer{elements={max(MinA, MinB),min(MaxA, MaxB)}};
+glb(#t_integer{}=T, number) -> T;
+glb(float=T, number) -> T;
+glb(number, #t_integer{}=T) -> T;
+glb(number, float=T) -> T;
+glb(list, cons) -> cons;
+glb(list, nil) -> nil;
+glb(cons, list) -> cons;
+glb(nil, list) -> nil;
+glb(#t_tuple{}=T1, #t_tuple{}=T2) ->
+    glb_tuples(T1, T2);
+glb(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) ->
+    #t_bitstring{unit=U1 * U2 div gcd(U1, U2)};
+glb(_, _) ->
+    %% Inconsistent types. There will be an exception at runtime.
+    none.
+
+glb_tuples(#t_tuple{size=Sz1,exact=true},
+           #t_tuple{size=Sz2,exact=true}) when Sz1 =/= Sz2 ->
+    none;
+glb_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,
+    case glb_elements(Es1, Es2) of
+        none ->
+            none;
+        Es ->
+            #t_tuple{size=Size,exact=Exact,elements=Es}
+    end.
+
+glb_elements(Es1, Es2) ->
+    Keys = maps:keys(Es1) ++ maps:keys(Es2),
+    glb_elements_1(Keys, Es1, Es2, #{}).
+
+glb_elements_1([Key | Keys], Es1, Es2, Acc) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            %% Note the use of meet/2; elements don't need to be normal types.
+            case meet(Type1, Type2) of
+                none -> none;
+                Type -> glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type })
+            end;
+        {#{ Key := Type1 }, _} ->
+            glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type1 });
+        {_, #{ Key := Type2 }} ->
+            glb_elements_1(Keys, Es1, Es2, Acc#{ Key => Type2 })
+    end;
+glb_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
+%% Return the least upper bound of the types Type1 and Type2. The LUB is a more
+%% general type than Type1 and Type2, and is always a normal type.
+%%
+%% For example:
+%%
+%%    lub(#t_integer{elements=any}, #t_integer=elements={0,3}}) ->
+%%         #t_integer{}
+%%
+%% The LUB for two different types result in 'any' (not a union type!), which
+%% is the top element for our type lattice:
+%%
+%%    lub(#t_integer{}, #t_map{}) -> any
+
+-spec lub(normal_type(), normal_type()) -> normal_type().
+
+lub(T, T) ->
+    verified_normal_type(T);
+lub(none, T) ->
+    verified_normal_type(T);
+lub(T, none) ->
+    verified_normal_type(T);
+lub(any, _) ->
+    any;
+lub(_, any) ->
+    any;
+lub(#t_atom{elements=[_|_]=Set1}, #t_atom{elements=[_|_]=Set2}) ->
+    Set = ordsets:union(Set1, Set2),
+    case ordsets:size(Set) of
+        Size when Size =< ?ATOM_SET_SIZE ->
+            #t_atom{elements=Set};
+        _Size ->
+            #t_atom{elements=any}
+    end;
+lub(#t_atom{elements=any}=T, #t_atom{elements=[_|_]}) -> T;
+lub(#t_atom{elements=[_|_]}, #t_atom{elements=any}=T) -> T;
+lub(#t_bitstring{unit=U1}, #t_bitstring{unit=U2}) ->
+    #t_bitstring{unit=gcd(U1, U2)};
+lub(#t_fun{}, #t_fun{}) ->
+    #t_fun{};
+lub(#t_integer{elements={MinA,MaxA}},
+    #t_integer{elements={MinB,MaxB}}) ->
+    #t_integer{elements={min(MinA,MinB),max(MaxA,MaxB)}};
+lub(#t_bs_context{slots=SlotsA,valid=ValidA},
+    #t_bs_context{slots=SlotsB,valid=ValidB}) ->
+    #t_bs_context{slots=min(SlotsA, SlotsB),
+                  valid=ValidA band ValidB};
+lub(#t_integer{}, #t_integer{}) -> #t_integer{};
+lub(list, cons) -> list;
+lub(cons, list) -> list;
+lub(nil, cons) -> list;
+lub(cons, nil) -> list;
+lub(nil, list) -> list;
+lub(list, nil) -> list;
+lub(#t_integer{}, float) -> number;
+lub(float, #t_integer{}) -> number;
+lub(#t_integer{}, number) -> number;
+lub(number, #t_integer{}) -> number;
+lub(float, number) -> number;
+lub(number, float) -> number;
+lub(#t_tuple{size=Sz,exact=ExactA,elements=EsA},
+    #t_tuple{size=Sz,exact=ExactB,elements=EsB}) ->
+    Exact = ExactA and ExactB,
+    Es = lub_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,exact=Exact,elements=Es};
+lub(#t_tuple{size=SzA,elements=EsA}, #t_tuple{size=SzB,elements=EsB}) ->
+    Sz = min(SzA, SzB),
+    Es = lub_tuple_elements(Sz, EsA, EsB),
+    #t_tuple{size=Sz,elements=Es};
+lub(_T1, _T2) ->
+    %%io:format("~p ~p\n", [_T1,_T2]),
+    any.
+
+lub_tuple_elements(MinSize, EsA, EsB) ->
+    Es0 = lub_elements(EsA, EsB),
+    maps:filter(fun(Index, _Type) -> Index =< MinSize end, Es0).
+
+lub_elements(Es1, Es2) ->
+    Keys = if
+               map_size(Es1) =< map_size(Es2) -> maps:keys(Es1);
+               map_size(Es1) > map_size(Es2) -> maps:keys(Es2)
+           end,
+    lub_elements_1(Keys, Es1, Es2, #{}).
+
+lub_elements_1([Key | Keys], Es1, Es2, Acc0) ->
+    case {Es1, Es2} of
+        {#{ Key := Type1 }, #{ Key := Type2 }} ->
+            %% Note the use of join/2; elements don't need to be normal types.
+            Acc = set_element_type(Key, join(Type1, Type2), Acc0),
+            lub_elements_1(Keys, Es1, Es2, Acc);
+        {#{}, #{}} ->
+            lub_elements_1(Keys, Es1, Es2, Acc0)
+    end;
+lub_elements_1([], _Es1, _Es2, Acc) ->
+    Acc.
+
+%%
+
+gcd(A, B) ->
+    case A rem B of
+        0 -> B;
+        X -> gcd(B, X)
+    end.
+
+%%
+
+record_key(#t_tuple{exact=true,size=Size,elements=#{ 1 := Tag }}) ->
+    case is_singleton_type(Tag) of
+        true -> {Size, Tag};
+        false -> none
+    end;
+record_key(_) ->
+    none.
+
+new_tuple_set(T) ->
+    case record_key(T) of
+        none -> T;
+        Key -> [{Key, T}]
+    end.
+
+%%
+
+shrink_union(#t_union{other=any}) ->
+    any;
+shrink_union(#t_union{atom=Atom,list=none,number=none,
+                      tuple_set=none,other=none}) ->
+    Atom;
+shrink_union(#t_union{atom=none,list=List,number=none,
+                      tuple_set=none,other=none}) ->
+    List;
+shrink_union(#t_union{atom=none,list=none,number=Number,
+                      tuple_set=none,other=none}) ->
+    Number;
+shrink_union(#t_union{atom=none,list=none,number=none,
+                      tuple_set=#t_tuple{}=Tuple,other=none}) ->
+    Tuple;
+shrink_union(#t_union{atom=none,list=none,number=none,
+                      tuple_set=[{_Key, Record}],other=none}) ->
+    #t_tuple{} = Record;                        %Assertion.
+shrink_union(#t_union{atom=none,list=none,number=none,
+                      tuple_set=none,other=Other}) ->
+    Other;
+shrink_union(#t_union{}=T) ->
+    T.
+
+%% Verifies that the given type is well-formed.
+
+-spec verified_type(T) -> T when
+      T :: type().
+
+verified_type(#t_union{atom=Atom,
+                       list=List,
+                       number=Number,
+                       tuple_set=TSet,
+                       other=Other}=T) ->
+    _ = verified_normal_type(Atom),
+    _ = verified_normal_type(List),
+    _ = verified_normal_type(Number),
+    _ = verify_tuple_set(TSet),
+    _ = verified_normal_type(Other),
+    T;
+verified_type(T) ->
+    verified_normal_type(T).
+
+verify_tuple_set([_|_]=T) ->
+    _ = [verified_normal_type(Rec) || {_, Rec} <- T],
+    T;
+verify_tuple_set(#t_tuple{}=T) ->
+    none = record_key(T),                       %Assertion.
+    T;
+verify_tuple_set(none=T) ->
+    T.
+
+-spec verified_normal_type(T) -> T when
+      T :: normal_type().
+
+verified_normal_type(any=T) -> T;
+verified_normal_type(none=T) -> T;
+verified_normal_type(#t_atom{elements=any}=T) -> T;
+verified_normal_type(#t_atom{elements=[_|_]}=T) -> T;
+verified_normal_type(#t_bitstring{unit=U}=T)
+  when is_integer(U), U >= 1 ->
+    T;
+verified_normal_type(#t_bs_context{}=T) -> T;
+verified_normal_type(#t_fun{arity=Arity}=T)
+  when Arity =:= any; is_integer(Arity) ->
+    T;
+verified_normal_type(float=T) -> T;
+verified_normal_type(#t_integer{elements=any}=T) -> T;
+verified_normal_type(#t_integer{elements={Min,Max}}=T)
+  when is_integer(Min), is_integer(Max), Min =< Max ->
+    T;
+verified_normal_type(list=T) -> T;
+verified_normal_type(#t_map{}=T) -> T;
+verified_normal_type(nil=T) -> T;
+verified_normal_type(cons=T) -> T;
+verified_normal_type(number=T) -> T;
+verified_normal_type(#t_tuple{size=Size,elements=Es}=T) ->
+    %% All known elements must have a valid index and type (which may be a
+    %% union). 'any' is prohibited since it's implicit and should never be
+    %% present in the map, and a 'none' element ought to have reduced the
+    %% entire tuple to 'none'.
+    maps:fold(fun(Index, Element, _) when is_integer(Index),
+                                          1 =< Index, Index =< Size,
+                                          Element =/= any, Element =/= none ->
+                      verified_type(Element)
+              end, [], Es),
+    T.
diff --git a/lib/compiler/src/beam_types.hrl b/lib/compiler/src/beam_types.hrl
index 212fe62063..09f87d61ba 100644
--- a/lib/compiler/src/beam_types.hrl
+++ b/lib/compiler/src/beam_types.hrl
@@ -39,6 +39,13 @@
 %%    - #t_tuple{}       Tuple.
 %%
 %%  none                 No type (bottom element).
+%%
+%% We also use #t_union{} to represent conflicting types produced by certain
+%% expressions, e.g. the "#t_atom{} or #t_tuple{}" of lists:keyfind/3, which is
+%% very useful for preserving type information when we would otherwise have
+%% reduced it to 'any'. Since few operations can make direct use of this extra
+%% type information, types should generally be normalized to one of the above
+%% before use.
 
 -define(ATOM_SET_SIZE, 5).
 
@@ -62,8 +69,20 @@
 
 -type elements() :: tuple_elements() | map_elements().
 
--type type() :: any | none |
-                list | number |
-                #t_atom{} | #t_bitstring{} | #t_bs_context{} |
-                #t_fun{} | #t_integer{} | #t_map{} | #t_tuple{} |
-                'cons' | 'float' | 'nil'.
+-type normal_type() :: any | none |
+                       list | number |
+                       #t_atom{} | #t_bitstring{} | #t_bs_context{} |
+                       #t_fun{} | #t_integer{} | #t_map{} | #t_tuple{} |
+                       'cons' | 'float' | 'nil'.
+
+-type record_key() :: {Arity :: integer(), Tag :: normal_type() }.
+-type record_set() :: ordsets:ordset({record_key(), #t_tuple{}}).
+-type tuple_set() :: #t_tuple{} | record_set().
+
+-record(t_union, {atom=none :: none | #t_atom{},
+                  list=none :: none | list | cons | nil,
+                  number=none :: none | number | float | #t_integer{},
+                  tuple_set=none :: none | tuple_set(),
+                  other=none :: normal_type()}).
+
+-type type() :: #t_union{} | normal_type().
diff --git a/lib/compiler/src/beam_validator.erl b/lib/compiler/src/beam_validator.erl
index d959700b88..923a0b4a4e 100644
--- a/lib/compiler/src/beam_validator.erl
+++ b/lib/compiler/src/beam_validator.erl
@@ -570,7 +570,7 @@ valfun_1({get_tuple_element,Src,N,Dst}, Vst) ->
     Index = N+1,
     assert_not_literal(Src),
     assert_type(#t_tuple{size=Index}, Src, Vst),
-    #t_tuple{elements=Es} = get_term_type(Src, Vst),
+    #t_tuple{elements=Es} = normalize(get_term_type(Src, Vst)),
     Type = beam_types:get_element_type(Index, Es),
     extract_term(Type, {bif,element}, [{integer,Index}, Src], Dst, Vst);
 valfun_1({jump,{f,Lbl}}, Vst) ->
@@ -762,7 +762,7 @@ valfun_4({set_tuple_element,Src,Tuple,N}, Vst) ->
     %% helpers as we must support overwriting (rather than just widening or
     %% narrowing) known elements, and we can't use extract_term either since
     %% the source tuple may be aliased.
-    #t_tuple{elements=Es0}=Type = get_term_type(Tuple, Vst),
+    #t_tuple{elements=Es0}=Type = normalize(get_term_type(Tuple, Vst)),
     Es = beam_types:set_element_type(I, get_term_type(Src, Vst), Es0),
     override_type(Type#t_tuple{elements=Es}, Tuple, Vst);
 %% Match instructions.
@@ -1927,6 +1927,9 @@ is_literal(_) -> false.
 %% The funny-looking abstract types produced here are intended to provoke
 %% errors on actual use; they do no harm just lying around.
 
+normalize(#t_abstract{}=A) -> error({abstract_type, A});
+normalize(T) -> beam_types:normalize(T).
+
 join(Same, Same) -> Same;
 join(#t_abstract{}=A, B) -> #t_abstract{kind={join, A, B}};
 join(A, #t_abstract{}=B) -> #t_abstract{kind={join, A, B}};
@@ -2369,7 +2372,7 @@ assert_not_fragile(Lit, #vst{}) ->
 %%%
 
 bif_types(Op, Ss, Vst) ->
-    Args = [get_term_type(Arg, Vst) || Arg <- Ss],
+    Args = [normalize(get_term_type(Arg, Vst)) || Arg <- Ss],
     beam_call_types:types(erlang, Op, Args).
 
 call_types({extfunc,M,F,A}, A, Vst) ->
@@ -2384,7 +2387,8 @@ get_call_args(Arity, Vst) ->
 get_call_args_1(Arity, Arity, _) ->
     [];
 get_call_args_1(N, Arity, Vst) when N < Arity ->
-    [get_movable_term_type({x,N}, Vst) | get_call_args_1(N + 1, Arity, Vst)].
+    ArgType = normalize(get_movable_term_type({x,N}, Vst)),
+    [ArgType | get_call_args_1(N + 1, Arity, Vst)].
 
 check_limit({x,X}=Src) when is_integer(X) ->
     if
diff --git a/lib/compiler/test/property_test/beam_types_prop.erl b/lib/compiler/test/property_test/beam_types_prop.erl
index e797440ba5..8199d1bd5a 100644
--- a/lib/compiler/test/property_test/beam_types_prop.erl
+++ b/lib/compiler/test/property_test/beam_types_prop.erl
@@ -49,10 +49,10 @@ absorption_1() ->
 
 absorption_check(A, B) ->
     %% a ∨ (a ∧ b) = a,
-    A = beam_types:join(A, beam_types:meet(A, B)),
+    A = join(A, meet(A, B)),
 
     %% a ∧ (a ∨ b) = a.
-    A = beam_types:meet(A, beam_types:join(A, B)),
+    A = meet(A, join(A, B)),
 
     true.
 
@@ -68,13 +68,13 @@ associativity_1() ->
 
 associativity_check(A, B, C) ->
     %% a ∨ (b ∨ c) = (a ∨ b) ∨ c,
-    LHS_Join = beam_types:join(A, beam_types:join(B, C)),
-    RHS_Join = beam_types:join(beam_types:join(A, B), C),
+    LHS_Join = join(A, join(B, C)),
+    RHS_Join = join(join(A, B), C),
     LHS_Join = RHS_Join,
 
     %% a ∧ (b ∧ c) = (a ∧ b) ∧ c.
-    LHS_Meet = beam_types:meet(A, beam_types:meet(B, C)),
-    RHS_Meet = beam_types:meet(beam_types:meet(A, B), C),
+    LHS_Meet = meet(A, meet(B, C)),
+    RHS_Meet = meet(meet(A, B), C),
     LHS_Meet = RHS_Meet,
 
     true.
@@ -90,10 +90,10 @@ commutativity_1() ->
 
 commutativity_check(A, B) ->
     %% a ∨ b = b ∨ a,
-    true = beam_types:join(A, B) =:= beam_types:join(B, A),
+    true = join(A, B) =:= join(B, A),
 
     %% a ∧ b = b ∧ a.
-    true = beam_types:meet(A, B) =:= beam_types:meet(B, A),
+    true = meet(A, B) =:= meet(B, A),
 
     true.
 
@@ -105,10 +105,10 @@ idempotence_1() ->
 
 idempotence_check(Type) ->
     %% a ∨ a = a,
-    Type = beam_types:join(Type, Type),
+    Type = join(Type, Type),
 
     %% a ∧ a = a.
-    Type = beam_types:meet(Type, Type),
+    Type = meet(Type, Type),
 
     true.
 
@@ -117,13 +117,16 @@ identity() ->
 
 identity_check(Type) ->
     %% a ∨ [bottom element] = a,
-    Type = beam_types:join(Type, none),
+    Type = join(Type, none),
 
     %% a ∧ [top element] = a.
-    Type = beam_types:meet(Type, any),
+    Type = meet(Type, any),
 
     true.
 
+meet(A, B) -> beam_types:meet(A, B).
+join(A, B) -> beam_types:join(A, B).
+
 %%%
 %%% Generators
 %%%
@@ -149,8 +152,8 @@ list_types() ->
 numerical_types() ->
     [gen_integer(), float, number].
 
-nested_types(Depth) when Depth >= 3 -> [];
-nested_types(Depth) -> [#t_map{}, gen_tuple(Depth + 1)].
+nested_types(Depth) when Depth >= 3 -> [none];
+nested_types(Depth) -> [#t_map{}, gen_union(Depth + 1), gen_tuple(Depth + 1)].
 
 gen_atom() ->
     ?LET(Size, range(0, ?ATOM_SET_SIZE),
@@ -158,12 +161,15 @@ gen_atom() ->
              0 ->
                  #t_atom{};
              _ ->
-                 ?LET(Set, sized_list(Size, atom()),
+                 ?LET(Set, sized_list(Size, gen_atom_val()),
                       begin
                           #t_atom{elements=ordsets:from_list(Set)}
                       end)
          end).
 
+gen_atom_val() ->
+    ?LET(N, range($0, $~), list_to_atom([N])).
+
 gen_binary() ->
     ?SHRINK(#t_bitstring{unit=range(1, 128)}, [#t_bitstring{unit=1}]).
 
@@ -185,6 +191,25 @@ gen_tuple(Depth) ->
                              elements=Elements}
                 end)).
 
+gen_union(Depth) ->
+    ?LAZY(oneof([gen_wide_union(Depth), gen_tuple_union(Depth)])).
+
+gen_wide_union(Depth) ->
+    ?LET({A, B, C, D}, {oneof(nested_types(Depth)),
+                        oneof(numerical_types()),
+                        oneof(list_types()),
+                        oneof(other_types())},
+          begin
+              T0 = join(A, B),
+              T1 = join(T0, C),
+              join(T1, D)
+          end).
+
+gen_tuple_union(Depth) ->
+    ?SIZED(Size,
+           ?LET(Tuples, sized_list(Size, gen_tuple(Depth)),
+                lists:foldl(fun join/2, none, Tuples))).
+
 gen_tuple_elements(Size, Depth) ->
     ?LET(Types, sized_list(rand:uniform(Size div 4 + 1), gen_element(Depth)),
          maps:from_list([{rand:uniform(Size), T} || T <- Types])).
@@ -197,7 +222,6 @@ gen_element(Depth) ->
                         _ -> true
                     end)).
 
-
 sized_list(0, _Gen) -> [];
 sized_list(N, Gen) -> [Gen | sized_list(N - 1, Gen)].