dialyzer: New version for the R13B04 release

2 files changed, 545 insertions, 276 deletions

diff --git a/lib/hipe/cerl/erl_bif_types.erl b/lib/hipe/cerl/erl_bif_types.erl
index 8aa2cc76c7..ee0ddd6915 100644
--- a/lib/hipe/cerl/erl_bif_types.erl
+++ b/lib/hipe/cerl/erl_bif_types.erl
@@ -102,6 +102,7 @@
 		    t_list_elements/1,
 		    t_list_termination/1,
 		    t_mfa/0,
+		    t_module/0,
 		    t_nil/0,
 		    t_node/0,
 		    t_none/0,
@@ -694,6 +695,8 @@ type(erlang, binary_to_list, 3, Xs) ->
 	 fun (_) -> t_list(t_byte()) end);
 type(erlang, binary_to_term, 1, Xs) ->
   strict(arg_types(erlang, binary_to_term, 1), Xs, fun (_) -> t_any() end);
+type(erlang, binary_to_term, 2, Xs) ->
+  strict(arg_types(erlang, binary_to_term, 2), Xs, fun (_) -> t_any() end);
 type(erlang, bitsize, 1, Xs) ->	% XXX: TAKE OUT
   type(erlang, bit_size, 1, Xs);
 type(erlang, bit_size, 1, Xs) ->
@@ -3127,20 +3130,20 @@ arith(Op, X1, X2) ->
 	    end,
 	  %% io:format("done arith ~p = ~p~n", [Op, {NewMin, NewMax}]),
 	  {ok, t_from_range(NewMin, NewMax)};
-	false ->  
+	false ->
 	  %% Some of these arithmetic operations might throw a system_limit
 	  %% exception; for example, when trying to evaluate 1 bsl 100000000.
 	  try case Op of
-	        '+'    -> [X + Y    || X <- L1, Y <- L2];
-	        '-'    -> [X - Y    || X <- L1, Y <- L2];
-	        '*'    -> [X * Y    || X <- L1, Y <- L2];
-	        'div'  -> [X div Y  || X <- L1, Y <- L2,Y =/= 0];
-	        'rem'  -> [X rem Y  || X <- L1, Y <- L2,Y =/= 0];
-	        'bsl'  -> [X bsl Y  || X <- L1, Y <- L2];
-	        'bsr'  -> [X bsr Y  || X <- L1, Y <- L2];
-	        'band' -> [X band Y || X <- L1, Y <- L2];
-	        'bor'  -> [X bor Y  || X <- L1, Y <- L2];
-	        'bxor' -> [X bxor Y || X <- L1, Y <- L2]
+		'+'    -> [X + Y    || X <- L1, Y <- L2];
+		'-'    -> [X - Y    || X <- L1, Y <- L2];
+		'*'    -> [X * Y    || X <- L1, Y <- L2];
+		'div'  -> [X div Y  || X <- L1, Y <- L2, Y =/= 0];
+		'rem'  -> [X rem Y  || X <- L1, Y <- L2, Y =/= 0];
+		'bsl'  -> [X bsl Y  || X <- L1, Y <- L2];
+		'bsr'  -> [X bsr Y  || X <- L1, Y <- L2];
+		'band' -> [X band Y || X <- L1, Y <- L2];
+		'bor'  -> [X bor Y  || X <- L1, Y <- L2];
+		'bxor' -> [X bxor Y || X <- L1, Y <- L2]
 	      end of
 	    AllVals ->
 	      {ok, t_integers(ordsets:from_list(AllVals))}
@@ -3338,8 +3341,7 @@ arg_types(erlang, abs, 1) ->
 arg_types(erlang, append_element, 2) ->
   [t_tuple(), t_any()];
 arg_types(erlang, apply, 2) ->
-  [t_sup(t_tuple([t_sup(t_atom(),   % module name
-			t_tuple()), % parameterized module	    
+  [t_sup(t_tuple([t_module(),
 		  t_atom()]),
 	 t_fun()),
    t_list()];
@@ -3359,6 +3361,8 @@ arg_types(erlang, binary_to_list, 3) ->
   [t_binary(), t_pos_integer(), t_pos_integer()]; % I want fixnum, but cannot
 arg_types(erlang, binary_to_term, 1) ->
   [t_binary()];
+arg_types(erlang, binary_to_term, 2) ->
+  [t_binary(), t_list(t_atom('safe'))];
 arg_types(erlang, bitsize, 1) ->	% XXX: TAKE OUT
   arg_types(erlang, bit_size, 1);
 arg_types(erlang, bit_size, 1) ->
@@ -4351,6 +4355,7 @@ structure_inspecting_args(erlang, is_pid, 1) -> [1];
 structure_inspecting_args(erlang, is_port, 1) -> [1];
 structure_inspecting_args(erlang, is_reference, 1) -> [1];
 structure_inspecting_args(erlang, is_tuple, 1) -> [1];
+structure_inspecting_args(erlang, length, 1) -> [1];
 %%structure_inspecting_args(erlang, setelement, 3) -> [2].
 structure_inspecting_args(_, _, _) -> []. % XXX: assume no arg needs inspection
 
diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl
index fac308d0c6..871856da83 100644
--- a/lib/hipe/cerl/erl_types.erl
+++ b/lib/hipe/cerl/erl_types.erl
@@ -97,6 +97,7 @@
 	 t_inf/3,
 	 t_inf_lists/2,
 	 t_inf_lists/3,
+	 t_inf_lists_masked/3,
 	 t_integer/0,
 	 t_integer/1,
 	 t_non_neg_integer/0,
@@ -167,6 +168,7 @@
 	 t_opaque_match_record/2,
 	 t_opaque_matching_structure/2,
 	 t_opaque_structure/1,
+	 %% t_parameterized_module/0,
 	 t_pid/0,
 	 t_port/0,
 	 t_maybe_improper_list/0,
@@ -194,9 +196,11 @@
 	 t_tuple_sizes/1,
 	 t_tuple_subtypes/1,
 	 t_unify/2,
+	 t_unify/3,
 	 t_unit/0,
 	 t_unopaque/1,
 	 t_unopaque/2,
+	 t_unopaque_on_mismatch/3,
 	 t_var/1,
 	 t_var_name/1,
 	 %% t_assign_variables_to_subtype/2,
@@ -227,6 +231,8 @@
 %% Limits
 %%
 
+-define(REC_TYPE_LIMIT, 2).
+
 -define(TUPLE_TAG_LIMIT, 5).
 -define(TUPLE_ARITY_LIMIT, 10).
 -define(SET_LIMIT, 13).
@@ -590,33 +596,48 @@ t_opaque_tuple_tags(OpaqueStruct) ->
   end.
 
 %% Decompose opaque instances of type arg2 to structured types, in arg1
--spec t_struct_from_opaque(erl_type(), erl_type()) -> erl_type().
-
-t_struct_from_opaque(?function(Domain, Range), Opaque) ->
-  ?function(t_struct_from_opaque(Domain, Opaque),  
-	    t_struct_from_opaque(Range, Opaque));
-t_struct_from_opaque(?list(Types, Term, Size), Opaque) -> 
-  ?list(t_struct_from_opaque(Types, Opaque), Term, Size);
-t_struct_from_opaque(?opaque(_) = T, Opaque) -> 
-  case T =:= Opaque of
+%% XXX: Same as t_unopaque
+-spec t_struct_from_opaque(erl_type(), [erl_type()]) -> erl_type().
+
+t_struct_from_opaque(?function(Domain, Range), Opaques) ->
+  ?function(t_struct_from_opaque(Domain, Opaques),
+	    t_struct_from_opaque(Range, Opaques));
+t_struct_from_opaque(?list(Types, Term, Size), Opaques) ->
+  ?list(t_struct_from_opaque(Types, Opaques), Term, Size);
+t_struct_from_opaque(?opaque(_) = T, Opaques) ->
+  case lists:member(T, Opaques) of
     true  -> t_opaque_structure(T);
     false -> T
   end;
-t_struct_from_opaque(?product(Types), Opaque) -> 
-  ?product(list_struct_from_opaque(Types, Opaque));
-t_struct_from_opaque(?tuple(?any, _, _) = T, _Opaque) -> T;
-t_struct_from_opaque(?tuple(Types, Arity, Tag), Opaque)  ->
-  ?tuple(list_struct_from_opaque(Types, Opaque), Arity, Tag);
-t_struct_from_opaque(?tuple_set(Set), Opaque) ->
-  NewSet = [{Sz, [t_struct_from_opaque(T, Opaque) || T <- Tuples]}
+t_struct_from_opaque(?product(Types), Opaques) ->
+  ?product(list_struct_from_opaque(Types, Opaques));
+t_struct_from_opaque(?tuple(?any, _, _) = T, _Opaques) -> T;
+t_struct_from_opaque(?tuple(Types, Arity, Tag), Opaques) ->
+  ?tuple(list_struct_from_opaque(Types, Opaques), Arity, Tag);
+t_struct_from_opaque(?tuple_set(Set), Opaques) ->
+  NewSet = [{Sz, [t_struct_from_opaque(T, Opaques) || T <- Tuples]}
 	    || {Sz, Tuples} <- Set],
   ?tuple_set(NewSet);
-t_struct_from_opaque(?union(List), Opaque) ->
-  t_sup(list_struct_from_opaque(List, Opaque));
-t_struct_from_opaque(Type, _Opaque) -> Type.
-
-list_struct_from_opaque(Types, Opaque) ->
-  [t_struct_from_opaque(Type, Opaque) || Type <- Types].
+t_struct_from_opaque(?union(List), Opaques) ->
+  t_sup(list_struct_from_opaque(List, Opaques));
+t_struct_from_opaque(Type, _Opaques) -> Type.
+
+list_struct_from_opaque(Types, Opaques) ->
+  [t_struct_from_opaque(Type, Opaques) || Type <- Types].
+
+-spec t_unopaque_on_mismatch(erl_type(), erl_type(), [erl_type()]) -> erl_type().
+
+t_unopaque_on_mismatch(GenType, Type, Opaques) ->
+  case t_inf(GenType, Type) of
+    ?none ->
+      Unopaqued = t_unopaque(Type, Opaques),
+      %% Unions might be a problem, must investigate.
+      case t_inf(GenType, Unopaqued) of
+	?none -> Type;
+	_ -> Unopaqued
+      end;
+     _ -> Type
+  end.
 
 -spec module_builtin_opaques(module()) -> [erl_type()].
 
@@ -630,7 +651,7 @@ module_builtin_opaques(Module) ->
 -spec t_remote(module(), atom(), [_]) -> erl_type().
 
 t_remote(Mod, Name, Args) ->
-  ?remote(set_singleton(#remote{mod=Mod, name=Name, args=Args})).
+  ?remote(set_singleton(#remote{mod = Mod, name = Name, args = Args})).
 
 -spec t_is_remote(erl_type()) -> boolean().
 
@@ -640,78 +661,124 @@ t_is_remote(_) -> false.
 -spec t_solve_remote(erl_type(), dict()) -> erl_type().
 
 t_solve_remote(Type , Records) ->
-  t_solve_remote(Type, Records, ordsets:new()).
+  {RT, _RR} = t_solve_remote(Type, Records, []),
+  RT.
 
 t_solve_remote(?function(Domain, Range), R, C) ->
-  ?function(t_solve_remote(Domain, R, C), t_solve_remote(Range, R, C));
+  {RT1, RR1} = t_solve_remote(Domain, R, C),
+  {RT2, RR2} = t_solve_remote(Range, R, C),
+  {?function(RT1, RT2), RR1 ++ RR2};
 t_solve_remote(?list(Types, Term, Size), R, C) ->
-  ?list(t_solve_remote(Types, R, C), Term, Size); 
+  {RT, RR} = t_solve_remote(Types, R, C),
+  {?list(RT, Term, Size), RR};
 t_solve_remote(?product(Types), R, C) ->
-  ?product(list_solve_remote(Types, R, C));
+  {RL, RR} = list_solve_remote(Types, R, C),
+  {?product(RL), RR};
 t_solve_remote(?opaque(Set), R, C) ->
   List = ordsets:to_list(Set),
-  NewList = [Remote#opaque{struct = t_solve_remote(Struct, R, C)}
-	     || Remote = #opaque{struct = Struct} <- List],
-  ?opaque(ordsets:from_list(NewList));
-t_solve_remote(?tuple(?any, _, _) = T, _R, _C) -> T;
+  {NewList, RR} = opaques_solve_remote(List, R, C),
+  {?opaque(ordsets:from_list(NewList)), RR};
+t_solve_remote(?tuple(?any, _, _) = T, _R, _C) -> {T, []};
 t_solve_remote(?tuple(Types, Arity, Tag), R, C)  ->
-  ?tuple(list_solve_remote(Types, R, C), Arity, Tag);
-t_solve_remote(?tuple_set(Set), R, C)     ->
-  NewSet = [{Sz, [t_solve_remote(T, R, C) || T <- Tuples]} || {Sz, Tuples} <- Set],
-  ?tuple_set(NewSet);
+  {RL, RR} = list_solve_remote(Types, R, C),
+  {?tuple(RL, Arity, Tag), RR};
+t_solve_remote(?tuple_set(Set), R, C) ->
+  {NewSet, RR} = tuples_solve_remote(Set, R, C),
+  {?tuple_set(NewSet), RR};
 t_solve_remote(?remote(Set), R, C) ->
-  Cycle = ordsets:intersection(Set, C),
-  case ordsets:size(Cycle) of
-    0 -> ok;
-    _ -> 
-      CycleMsg = "Cycle detected while processing remote types: " ++
-	t_to_string(?remote(C), dict:new()),
-      throw({error, CycleMsg})
-  end,
-  NewCycle = ordsets:union(C, Set),
-  TypeFun = 
-    fun(#remote{mod = RemoteModule, name = Name, args = Args}) ->
-	case dict:find(RemoteModule, R) of
-	  error ->
-	    Msg = io_lib:format("Cannot locate module ~w to "
-				"resolve the remote type: ~w:~w()~n", 
-				[RemoteModule, RemoteModule, Name]),
-	    throw({error, Msg});
-	  {ok, RemoteDict} ->
-	    case lookup_type(Name, RemoteDict) of
-	      {type, {_TypeMod, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
-		List = lists:zip(ArgNames, Args),
-		TmpVardict = dict:from_list(List),
-		NewType = t_from_form(Type, RemoteDict, TmpVardict),
-		t_solve_remote(NewType, R, NewCycle);
-	      {opaque, {OpModule, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
-		List = lists:zip(ArgNames, Args),
-		TmpVardict = dict:from_list(List),
-		Rep = t_from_form(Type, RemoteDict, TmpVardict),
-		NewRep = t_solve_remote(Rep, R, NewCycle),
-		t_from_form({opaque, -1, Name, {OpModule, Args, NewRep}},
-			    RemoteDict, TmpVardict);
-	      {type, _} ->
-		Msg = io_lib:format("Unknown remote type ~w\n", [Name]),
-		throw({error, Msg});
-	      {opaque, _} ->
-		Msg = io_lib:format("Unknown remote opaque type ~w\n", [Name]),
-		throw({error, Msg});
-	      error ->
-		Msg = io_lib:format("Unable to find remote type ~w:~w()\n",
-				    [RemoteModule, Name]),
-		throw({error, Msg}) 
-	    end
-	end
-    end,
   RemoteList = ordsets:to_list(Set),
-  t_sup([TypeFun(RemoteType) || RemoteType <- RemoteList]);
-t_solve_remote(?union(List), R, C) -> 
-  t_sup(list_solve_remote(List, R, C));
-t_solve_remote(T, _R, _C) -> T.
+  {RL, RR} = list_solve_remote_type(RemoteList, R, C),
+  {t_sup(RL), RR};
+t_solve_remote(?union(List), R, C) ->
+  {RL, RR} = list_solve_remote(List, R, C),
+  {t_sup(RL), RR};
+t_solve_remote(T, _R, _C) -> {T, []}.
+
+t_solve_remote_type(#remote{mod = RemMod, name = Name, args = Args} = RemType,
+                    R, C) ->
+  case dict:find(RemMod, R) of
+    error ->
+      Msg = io_lib:format("Cannot locate module ~w to "
+                          "resolve the remote type: ~w:~w()~n",
+                          [RemMod, RemMod, Name]),
+      throw({error, Msg});
+    {ok, RemDict} ->
+      case lookup_type(Name, RemDict) of
+        {type, {_Mod, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
+          {NewType, NewCycle, NewRR} =
+            case unfold(RemType, C) of
+              true ->
+                List = lists:zip(ArgNames, Args),
+                TmpVarDict = dict:from_list(List),
+                {t_from_form(Type, RemDict, TmpVarDict), [RemType|C], []};
+              false -> {t_any(), C, [RemType]}
+            end,
+          {RT, RR} = t_solve_remote(NewType, R, NewCycle),
+          RetRR = NewRR ++ RR,
+          RT1 =
+            case lists:member(RemType, RetRR) of
+              true -> t_limit(RT, ?REC_TYPE_LIMIT);
+              false -> RT
+            end,
+          {RT1, RetRR};
+        {opaque, {Mod, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
+          List = lists:zip(ArgNames, Args),
+          TmpVarDict = dict:from_list(List),
+          {Rep, NewCycle, NewRR} =
+            case unfold(RemType, C) of
+              true -> {t_from_form(Type, RemDict, TmpVarDict), [RemType|C], []};
+              false -> {t_any(), C, [RemType]}
+            end,
+          {NewRep, RR} = t_solve_remote(Rep, R, NewCycle),
+          RetRR = NewRR ++ RR,
+          RT1 =
+            case lists:member(RemType, RetRR) of
+              true -> t_limit(NewRep, ?REC_TYPE_LIMIT);
+              false -> NewRep
+            end,
+          {t_from_form({opaque, -1, Name, {Mod, Args, RT1}},
+                       RemDict, TmpVarDict),
+           RetRR};
+        {type, _} ->
+          Msg = io_lib:format("Unknown remote type ~w\n", [Name]),
+          throw({error, Msg});
+        {opaque, _} ->
+          Msg = io_lib:format("Unknown remote opaque type ~w\n", [Name]),
+          throw({error, Msg});
+        error ->
+          Msg = io_lib:format("Unable to find remote type ~w:~w()\n",
+                              [RemMod, Name]),
+          throw({error, Msg})
+      end
+  end.
 
-list_solve_remote(Types, R, C) ->
-  [t_solve_remote(Type, R, C) || Type <- Types].
+list_solve_remote([], _R, _C) ->
+  {[], []};
+list_solve_remote([Type|Types], R, C) ->
+  {RT, RR1} = t_solve_remote(Type, R, C),
+  {RL, RR2} = list_solve_remote(Types, R, C),
+  {[RT|RL], RR1 ++ RR2}.
+
+list_solve_remote_type([], _R, _C) ->
+  {[], []};
+list_solve_remote_type([Type|Types], R, C) ->
+  {RT, RR1} = t_solve_remote_type(Type, R, C),
+  {RL, RR2} = list_solve_remote_type(Types, R, C),
+  {[RT|RL], RR1 ++ RR2}.
+
+opaques_solve_remote([], _R, _C) ->
+  {[], []};
+opaques_solve_remote([#opaque{struct = Struct} = Remote|Tail], R, C) ->
+  {RT, RR1} = t_solve_remote(Struct, R, C),
+  {LOp, RR2} = opaques_solve_remote(Tail, R, C),
+  {[Remote#opaque{struct = RT}|LOp], RR1 ++ RR2}.
+
+tuples_solve_remote([], _R, _C) ->
+  {[], []};
+tuples_solve_remote([{Sz, Tuples}|Tail], R, C) ->
+  {RL, RR1} = list_solve_remote(Tuples, R, C),
+  {LSzTpls, RR2} = tuples_solve_remote(Tail, R, C),
+  {[{Sz, RL}|LSzTpls], RR1 ++ RR2}.
 
 %%-----------------------------------------------------------------------------
 %% Unit type. Signals non termination.
@@ -1432,7 +1499,7 @@ t_mfa() ->
 -spec t_module() -> erl_type().
 
 t_module() ->
-  t_atom().
+  t_sup(t_atom(), t_parameterized_module()).
 
 -spec t_node() -> erl_type().
 
@@ -1457,6 +1524,11 @@ t_iolist(N) when N > 0 ->
 t_iolist(0) ->
   t_maybe_improper_list(t_any(), t_sup(t_binary(), t_nil())).
 
+-spec t_parameterized_module() -> erl_type().
+
+t_parameterized_module() ->
+  t_tuple().
+
 -spec t_timeout() -> erl_type().
 
 t_timeout() ->
@@ -2219,9 +2291,23 @@ t_inf(T, ?union(U2), Mode) ->
   ?union(U1) = force_union(T),
   inf_union(U1, U2, Mode);
 %% and as a result, the cases for ?opaque should appear *after* ?union
-t_inf(?opaque(Set1), ?opaque(Set2), _Mode) ->
+t_inf(?opaque(Set1) = T1, ?opaque(Set2) = T2, Mode) ->
   case set_intersection(Set1, Set2) of
-    ?none -> ?none;
+    ?none ->
+      case Mode =:= opaque of
+	true ->
+	  Struct1 = t_opaque_structure(T1),
+	  case t_inf(Struct1, T2) of
+	    ?none ->
+	      Struct2 = t_opaque_structure(T2),
+	      case t_inf(Struct2, T1) of
+		?none -> ?none;
+		_ -> T2
+	      end;
+	    _ -> T1
+	  end;
+	false -> ?none
+      end;
     NewSet -> ?opaque(NewSet)
   end;
 t_inf(?opaque(_) = T1, T2, opaque) ->
@@ -2272,6 +2358,12 @@ t_inf_lists_strict([T1|Left1], [T2|Left2], Acc, Mode) ->
 t_inf_lists_strict([], [], Acc, _Mode) ->
   lists:reverse(Acc).
 
+-spec t_inf_lists_masked([erl_type()], [erl_type()], [t_inf_mode()]) -> [erl_type()].
+
+t_inf_lists_masked(List1, List2, Mask) ->
+  List = lists:zip3(List1, List2, Mask),
+  [t_inf(T1, T2, Mode) || {T1, T2, Mode} <- List].
+
 inf_tuple_sets(L1, L2, Mode) ->
   case inf_tuple_sets(L1, L2, [], Mode) of
     [] -> ?none;
@@ -2434,82 +2526,112 @@ t_subst(T, _Dict, _Fun) ->
 -spec t_unify(erl_type(), erl_type()) -> {erl_type(), [{_, erl_type()}]}.
 
 t_unify(T1, T2) ->
-  {T, Dict} = t_unify(T1, T2, dict:new()),
+  t_unify(T1, T2, []).
+
+-spec t_unify(erl_type(), erl_type(), [erl_type()]) -> {erl_type(), [{_, erl_type()}]}.
+
+t_unify(T1, T2, Opaques) ->
+  {T, Dict} = t_unify(T1, T2, dict:new(), Opaques),
   {t_subst(T, Dict), lists:keysort(1, dict:to_list(Dict))}.
 
-t_unify(?var(Id) = T, ?var(Id), Dict) ->
+t_unify(?var(Id) = T, ?var(Id), Dict, _Opaques) ->
   {T, Dict};
-t_unify(?var(Id1) = T, ?var(Id2), Dict) ->
+t_unify(?var(Id1) = T, ?var(Id2), Dict, Opaques) ->
   case dict:find(Id1, Dict) of
     error -> 
       case dict:find(Id2, Dict) of
 	error -> {T, dict:store(Id2, T, Dict)};
-	{ok, Type} -> {Type, t_unify(T, Type, Dict)}
+	{ok, Type} -> {Type, t_unify(T, Type, Dict, Opaques)}
       end;
     {ok, Type1} ->
       case dict:find(Id2, Dict) of
 	error -> {Type1, dict:store(Id2, T, Dict)};
-	{ok, Type2} -> t_unify(Type1, Type2, Dict)
+	{ok, Type2} -> t_unify(Type1, Type2, Dict, Opaques)
       end
   end;
-t_unify(?var(Id), Type, Dict) ->
+t_unify(?var(Id), Type, Dict, Opaques) ->
   case dict:find(Id, Dict) of
     error -> {Type, dict:store(Id, Type, Dict)};
-    {ok, VarType} -> t_unify(VarType, Type, Dict)
+    {ok, VarType} -> t_unify(VarType, Type, Dict, Opaques)
   end;
-t_unify(Type, ?var(Id), Dict) ->
+t_unify(Type, ?var(Id), Dict, Opaques) ->
   case dict:find(Id, Dict) of
     error -> {Type, dict:store(Id, Type, Dict)};
-    {ok, VarType} -> t_unify(VarType, Type, Dict)
+    {ok, VarType} -> t_unify(VarType, Type, Dict, Opaques)
   end;
-t_unify(?function(Domain1, Range1), ?function(Domain2, Range2), Dict) ->
-  {Domain, Dict1} = t_unify(Domain1, Domain2, Dict),
-  {Range, Dict2} = t_unify(Range1, Range2, Dict1),
+t_unify(?function(Domain1, Range1), ?function(Domain2, Range2), Dict, Opaques) ->
+  {Domain, Dict1} = t_unify(Domain1, Domain2, Dict, Opaques),
+  {Range, Dict2} = t_unify(Range1, Range2, Dict1, Opaques),
   {?function(Domain, Range), Dict2};
 t_unify(?list(Contents1, Termination1, Size), 
-	?list(Contents2, Termination2, Size), Dict) ->
-  {Contents, Dict1} = t_unify(Contents1, Contents2, Dict),
-  {Termination, Dict2} = t_unify(Termination1, Termination2, Dict1),
+	?list(Contents2, Termination2, Size), Dict, Opaques) ->
+  {Contents, Dict1} = t_unify(Contents1, Contents2, Dict, Opaques),
+  {Termination, Dict2} = t_unify(Termination1, Termination2, Dict1, Opaques),
   {?list(Contents, Termination, Size), Dict2};
-t_unify(?product(Types1), ?product(Types2), Dict) -> 
-  {Types, Dict1} = unify_lists(Types1, Types2, Dict),
+t_unify(?product(Types1), ?product(Types2), Dict, Opaques) ->
+  {Types, Dict1} = unify_lists(Types1, Types2, Dict, Opaques),
   {?product(Types), Dict1};
-t_unify(?tuple(?any, ?any, ?any) = T, ?tuple(?any, ?any, ?any), Dict) ->
+t_unify(?tuple(?any, ?any, ?any) = T, ?tuple(?any, ?any, ?any), Dict, _Opaques) ->
   {T, Dict};
 t_unify(?tuple(Elements1, Arity, _), 
-	?tuple(Elements2, Arity, _), Dict) when Arity =/= ?any ->
-  {NewElements, Dict1} = unify_lists(Elements1, Elements2, Dict),
+	?tuple(Elements2, Arity, _), Dict, Opaques) when Arity =/= ?any ->
+  {NewElements, Dict1} = unify_lists(Elements1, Elements2, Dict, Opaques),
   {t_tuple(NewElements), Dict1};
 t_unify(?tuple_set([{Arity, _}]) = T1, 
-	?tuple(_, Arity, _) = T2, Dict) when Arity =/= ?any ->
-  unify_tuple_set_and_tuple(T1, T2, Dict);
+	?tuple(_, Arity, _) = T2, Dict, Opaques) when Arity =/= ?any ->
+  unify_tuple_set_and_tuple(T1, T2, Dict, Opaques);
 t_unify(?tuple(_, Arity, _) = T1,
-	?tuple_set([{Arity, _}]) = T2, Dict) when Arity =/= ?any ->
-  unify_tuple_set_and_tuple(T2, T1, Dict);
-t_unify(?tuple_set(List1), ?tuple_set(List2), Dict) ->
+	?tuple_set([{Arity, _}]) = T2, Dict, Opaques) when Arity =/= ?any ->
+  unify_tuple_set_and_tuple(T2, T1, Dict, Opaques);
+t_unify(?tuple_set(List1), ?tuple_set(List2), Dict, Opaques) ->
   {Tuples, NewDict} = 
     unify_lists(lists:append([T || {_Arity, T} <- List1]), 
-		lists:append([T || {_Arity, T} <- List2]), Dict),
+		lists:append([T || {_Arity, T} <- List2]), Dict, Opaques),
   {t_sup(Tuples), NewDict};
-t_unify(T, T, Dict) ->
+t_unify(?opaque(Elements) = T, ?opaque(Elements), Dict, _Opaques) ->
   {T, Dict};
-t_unify(T1, T2, _) ->
+t_unify(?opaque(_) = T1, ?opaque(_) = T2, _Dict, _Opaques) ->
+  throw({mismatch, T1, T2});
+t_unify(Type, ?opaque(_) = OpType, Dict, Opaques) ->
+  t_unify_with_opaque(Type, OpType, Dict, Opaques);
+t_unify(?opaque(_) = OpType, Type, Dict, Opaques) ->
+  t_unify_with_opaque(Type, OpType, Dict, Opaques);
+t_unify(T, T, Dict, _Opaques) ->
+  {T, Dict};
+t_unify(T1, T2, _, _) ->
   throw({mismatch, T1, T2}).
 
+t_unify_with_opaque(Type, OpType, Dict, Opaques) ->
+  case lists:member(OpType, Opaques) of
+    true ->
+      Struct = t_opaque_structure(OpType),
+      try t_unify(Type, Struct, Dict, Opaques) of
+	{_T, Dict1} -> {OpType, Dict1}
+      catch
+	throw:{mismatch, _T1, _T2} ->
+	  case t_inf(OpType, Type, opaque) of
+	    ?none -> throw({mismatch, Type, OpType});
+	    _ -> {OpType, Dict}
+	  end
+      end;
+    false ->
+      throw({mismatch, Type, OpType})
+  end.
+
 unify_tuple_set_and_tuple(?tuple_set([{Arity, List}]), 
-			  ?tuple(Elements2, Arity, _), Dict) ->
+			  ?tuple(Elements2, Arity, _), Dict, Opaques) ->
   %% Can only work if the single tuple has variables at correct places.
   %% Collapse the tuple set.
-  {NewElements, Dict1} = unify_lists(sup_tuple_elements(List), Elements2, Dict),
+  {NewElements, Dict1} = unify_lists(sup_tuple_elements(List), Elements2, Dict, Opaques),
   {t_tuple(NewElements), Dict1}.
 
-unify_lists(L1, L2, Dict) ->
-  unify_lists(L1, L2, Dict, []).
+unify_lists(L1, L2, Dict, Opaques) ->
+  unify_lists(L1, L2, Dict, [], Opaques).
 
-unify_lists([T1|Left1], [T2|Left2], Dict, Acc) ->
-  {NewT, NewDict} = t_unify(T1, T2, Dict),
-  unify_lists(Left1, Left2, NewDict, [NewT|Acc]);
-unify_lists([], [], Dict, Acc) ->
+unify_lists([T1|Left1], [T2|Left2], Dict, Acc, Opaques) ->
+  {NewT, NewDict} = t_unify(T1, T2, Dict, Opaques),
+  unify_lists(Left1, Left2, NewDict, [NewT|Acc], Opaques);
+unify_lists([], [], Dict, Acc, _Opaques) ->
   {lists:reverse(Acc), Dict}.
 
 %%t_assign_variables_to_subtype(T1, T2) ->
@@ -3237,123 +3359,218 @@ t_from_form(Form, RecDict) ->
 
 -spec t_from_form(parse_form(), dict(), dict()) -> erl_type().
 
-t_from_form({var, _L, '_'}, _RecDict, _VarDict) -> t_any();
-t_from_form({var, _L, Name}, _RecDict, VarDict) ->
+t_from_form(Form, RecDict, VarDict) ->
+  {T, _R} = t_from_form(Form, [], RecDict, VarDict),
+  T.
+
+-type type_names() :: [{'type' | 'opaque' | 'record', atom()}].
+-spec t_from_form(parse_form(), type_names(), dict(), dict()) ->
+                     {erl_type(), type_names()}.
+
+t_from_form({var, _L, '_'}, _TypeNames, _RecDict, _VarDict) ->
+  {t_any(), []};
+t_from_form({var, _L, Name}, _TypeNames, _RecDict, VarDict) ->
   case dict:find(Name, VarDict) of
-    error -> t_var(Name);
-    {ok, Val} -> Val
+    error -> {t_var(Name), []};
+    {ok, Val} -> {Val, []}
   end;
-t_from_form({ann_type, _L, [_Var, Type]}, RecDict, VarDict) ->
-  t_from_form(Type, RecDict, VarDict);
-t_from_form({paren_type, _L, [Type]}, RecDict, VarDict) ->
-  t_from_form(Type, RecDict, VarDict);
+t_from_form({ann_type, _L, [_Var, Type]}, TypeNames, RecDict, VarDict) ->
+  t_from_form(Type, TypeNames, RecDict, VarDict);
+t_from_form({paren_type, _L, [Type]}, TypeNames, RecDict, VarDict) ->
+  t_from_form(Type, TypeNames, RecDict, VarDict);
 t_from_form({remote_type, _L, [{atom, _, Module}, {atom, _, Type}, Args]},
-	    RecDict, VarDict) ->
-  t_remote(Module, Type, [t_from_form(A, RecDict, VarDict) || A <- Args]);
-t_from_form({atom, _L, Atom}, _RecDict, _VarDict) -> t_atom(Atom);
-t_from_form({integer, _L, Int}, _RecDict, _VarDict) -> t_integer(Int);
-t_from_form({type, _L, any, []}, _RecDict, _VarDict) -> t_any();
-t_from_form({type, _L, arity, []}, _RecDict, _VarDict) -> t_arity();
-t_from_form({type, _L, array, []}, _RecDict, _VarDict) -> t_array();
-t_from_form({type, _L, atom, []}, _RecDict, _VarDict) -> t_atom();
-t_from_form({type, _L, binary, []}, _RecDict, _VarDict) -> t_binary();
+	    TypeNames, RecDict, VarDict) ->
+  {L, R} = list_from_form(Args, TypeNames, RecDict, VarDict),
+  {t_remote(Module, Type, L), R};
+t_from_form({atom, _L, Atom}, _TypeNames, _RecDict, _VarDict) ->
+  {t_atom(Atom), []};
+t_from_form({integer, _L, Int}, _TypeNames, _RecDict, _VarDict) ->
+  {t_integer(Int), []};
+t_from_form({type, _L, any, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_any(), []};
+t_from_form({type, _L, arity, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_arity(), []};
+t_from_form({type, _L, array, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_array(), []};
+t_from_form({type, _L, atom, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_atom(), []};
+t_from_form({type, _L, binary, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_binary(), []};
 t_from_form({type, _L, binary, [{integer, _, Base}, {integer, _, Unit}]}, 
-	    _RecDict, _VarDict) -> 
-  t_bitstr(Unit, Base);
-t_from_form({type, _L, bitstring, []}, _RecDict, _VarDict) -> t_bitstr();
-t_from_form({type, _L, bool, []}, _RecDict, _VarDict) -> t_boolean();	% XXX: Temporarily
-t_from_form({type, _L, boolean, []}, _RecDict, _VarDict) -> t_boolean();
-t_from_form({type, _L, byte, []}, _RecDict, _VarDict) -> t_byte();
-t_from_form({type, _L, char, []}, _RecDict, _VarDict) -> t_char();
-t_from_form({type, _L, dict, []}, _RecDict, _VarDict) -> t_dict();
-t_from_form({type, _L, digraph, []}, _RecDict, _VarDict) -> t_digraph();
-t_from_form({type, _L, float, []}, _RecDict, _VarDict) -> t_float();
-t_from_form({type, _L, function, []}, _RecDict, _VarDict) -> t_fun();
-t_from_form({type, _L, 'fun', []}, _RecDict, _VarDict) -> t_fun();
-t_from_form({type, _L, 'fun', [{type, _, any, []}, Range]}, RecDict, VarDict) ->
-  t_fun(t_from_form(Range, RecDict, VarDict));
-t_from_form({type, _L, 'fun', [{type, _, product, Domain}, Range]}, 
-	    RecDict, VarDict) -> 
-  t_fun([t_from_form(D, RecDict, VarDict) || D <- Domain], 
-	t_from_form(Range, RecDict, VarDict));
-t_from_form({type, _L, gb_set, []}, _RecDict, _VarDict) -> t_gb_set();
-t_from_form({type, _L, gb_tree, []}, _RecDict, _VarDict) -> t_gb_tree();
-t_from_form({type, _L, identifier, []}, _RecDict, _VarDict) -> t_identifier();
-t_from_form({type, _L, integer, []}, _RecDict, _VarDict) -> t_integer();
-t_from_form({type, _L, iodata, []}, _RecDict, _VarDict) -> t_iodata();
-t_from_form({type, _L, iolist, []}, _RecDict, _VarDict) -> t_iolist();
-t_from_form({type, _L, list, []}, _RecDict, _VarDict) -> t_list();
-t_from_form({type, _L, list, [Type]}, RecDict, VarDict) -> 
-  t_list(t_from_form(Type, RecDict, VarDict));
-t_from_form({type, _L, mfa, []}, _RecDict, _VarDict) -> t_mfa();
-t_from_form({type, _L, module, []}, _RecDict, _VarDict) -> t_module();
-t_from_form({type, _L, nil, []}, _RecDict, _VarDict) -> t_nil();
-t_from_form({type, _L, neg_integer, []}, _RecDict, _VarDict) -> t_neg_integer();
-t_from_form({type, _L, non_neg_integer, []}, _RecDict, _VarDict) -> 
-  t_non_neg_integer();
-t_from_form({type, _L, no_return, []}, _RecDict, _VarDict) -> t_unit();
-t_from_form({type, _L, node, []}, _RecDict, _VarDict) -> t_node();
-t_from_form({type, _L, none, []}, _RecDict, _VarDict) -> t_none();
-t_from_form({type, _L, nonempty_list, []}, _RecDict, _VarDict) -> 
-  t_nonempty_list();
-t_from_form({type, _L, nonempty_list, [Type]}, RecDict, VarDict) -> 
-  t_nonempty_list(t_from_form(Type, RecDict, VarDict));
-t_from_form({type, _L, nonempty_improper_list, [Cont, Term]}, 
-	    RecDict, VarDict) -> 
-  t_cons(t_from_form(Cont, RecDict, VarDict), 
-	 t_from_form(Term, RecDict, VarDict));
-t_from_form({type, _L, nonempty_maybe_improper_list, []}, _RecDict, _VarDict) ->
-  t_cons(?any, ?any);
-t_from_form({type, _L, nonempty_maybe_improper_list, [Cont, Term]}, 
-	    RecDict, VarDict) -> 
-  t_cons(t_from_form(Cont, RecDict, VarDict), 
-	 t_from_form(Term, RecDict, VarDict));
-t_from_form({type, _L, nonempty_string, []}, _RecDict, _VarDict) -> 
-  t_nonempty_string();
-t_from_form({type, _L, number, []}, _RecDict, _VarDict) -> t_number();
-t_from_form({type, _L, pid, []}, _RecDict, _VarDict) -> t_pid();
-t_from_form({type, _L, port, []}, _RecDict, _VarDict) -> t_port();
-t_from_form({type, _L, pos_integer, []}, _RecDict, _VarDict) -> t_pos_integer();
-t_from_form({type, _L, maybe_improper_list, []}, _RecDict, _VarDict) -> 
-  t_maybe_improper_list();
-t_from_form({type, _L, maybe_improper_list, [Content, Termination]}, 
-	    RecDict, VarDict) ->
-  t_maybe_improper_list(t_from_form(Content, RecDict, VarDict), 
-			t_from_form(Termination, RecDict, VarDict));
-t_from_form({type, _L, product, Elements}, RecDict, VarDict) ->
-  t_product([t_from_form(E, RecDict, VarDict) || E <- Elements]);
-t_from_form({type, _L, queue, []}, _RecDict, _VarDict) -> t_queue();
+	    _TypeNames, _RecDict, _VarDict) ->
+  {t_bitstr(Unit, Base), []};
+t_from_form({type, _L, bitstring, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_bitstr(), []};
+t_from_form({type, _L, bool, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_boolean(), []};	% XXX: Temporarily
+t_from_form({type, _L, boolean, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_boolean(), []};
+t_from_form({type, _L, byte, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_byte(), []};
+t_from_form({type, _L, char, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_char(), []};
+t_from_form({type, _L, dict, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_dict(), []};
+t_from_form({type, _L, digraph, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_digraph(), []};
+t_from_form({type, _L, float, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_float(), []};
+t_from_form({type, _L, function, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_fun(), []};
+t_from_form({type, _L, 'fun', []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_fun(), []};
+t_from_form({type, _L, 'fun', [{type, _, any, []}, Range]}, TypeNames,
+            RecDict, VarDict) ->
+  {T, R} = t_from_form(Range, TypeNames, RecDict, VarDict),
+  {t_fun(T), R};
+t_from_form({type, _L, 'fun', [{type, _, product, Domain}, Range]},
+            TypeNames, RecDict, VarDict) ->
+  {L, R1} = list_from_form(Domain, TypeNames, RecDict, VarDict),
+  {T, R2} = t_from_form(Range, TypeNames, RecDict, VarDict),
+  {t_fun(L, T), R1 ++ R2};
+t_from_form({type, _L, gb_set, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_gb_set(), []};
+t_from_form({type, _L, gb_tree, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_gb_tree(), []};
+t_from_form({type, _L, identifier, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_identifier(), []};
+t_from_form({type, _L, integer, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_integer(), []};
+t_from_form({type, _L, iodata, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_iodata(), []};
+t_from_form({type, _L, iolist, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_iolist(), []};
+t_from_form({type, _L, list, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_list(), []};
+t_from_form({type, _L, list, [Type]}, TypeNames, RecDict, VarDict) ->
+  {T, R} = t_from_form(Type, TypeNames, RecDict, VarDict),
+  {t_list(T), R};
+t_from_form({type, _L, mfa, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_mfa(), []};
+t_from_form({type, _L, module, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_module(), []};
+t_from_form({type, _L, nil, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_nil(), []};
+t_from_form({type, _L, neg_integer, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_neg_integer(), []};
+t_from_form({type, _L, non_neg_integer, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_non_neg_integer(), []};
+t_from_form({type, _L, no_return, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_unit(), []};
+t_from_form({type, _L, node, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_node(), []};
+t_from_form({type, _L, none, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_none(), []};
+t_from_form({type, _L, nonempty_list, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_nonempty_list(), []};
+t_from_form({type, _L, nonempty_list, [Type]}, TypeNames, RecDict, VarDict) ->
+  {T, R} = t_from_form(Type, TypeNames, RecDict, VarDict),
+  {t_nonempty_list(T), R};
+t_from_form({type, _L, nonempty_improper_list, [Cont, Term]}, TypeNames,
+            RecDict, VarDict) ->
+  {T1, R1} = t_from_form(Cont, TypeNames, RecDict, VarDict),
+  {T2, R2} = t_from_form(Term, TypeNames, RecDict, VarDict),
+  {t_cons(T1, T2), R1 ++ R2};
+t_from_form({type, _L, nonempty_maybe_improper_list, []}, _TypeNames,
+            _RecDict, _VarDict) ->
+  {t_cons(?any, ?any), []};
+t_from_form({type, _L, nonempty_maybe_improper_list, [Cont, Term]}, TypeNames,
+            RecDict, VarDict) ->
+  {T1, R1} = t_from_form(Cont, TypeNames, RecDict, VarDict),
+  {T2, R2} = t_from_form(Term, TypeNames, RecDict, VarDict),
+  {t_cons(T1, T2), R1 ++ R2};
+t_from_form({type, _L, nonempty_string, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_nonempty_string(), []};
+t_from_form({type, _L, number, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_number(), []};
+t_from_form({type, _L, pid, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_pid(), []};
+t_from_form({type, _L, port, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_port(), []};
+t_from_form({type, _L, pos_integer, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_pos_integer(), []};
+t_from_form({type, _L, maybe_improper_list, []}, _TypeNames, _RecDict,
+            _VarDict) ->
+  {t_maybe_improper_list(), []};
+t_from_form({type, _L, maybe_improper_list, [Content, Termination]}, TypeNames,
+            RecDict, VarDict) ->
+  {T1, R1} = t_from_form(Content, TypeNames, RecDict, VarDict),
+  {T2, R2} = t_from_form(Termination, TypeNames, RecDict, VarDict),
+  {t_maybe_improper_list(T1, T2), R1 ++ R2};
+t_from_form({type, _L, product, Elements}, TypeNames, RecDict, VarDict) ->
+  {L, R} = list_from_form(Elements, TypeNames, RecDict, VarDict),
+  {t_product(L), R};
+t_from_form({type, _L, queue, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_queue(), []};
 t_from_form({type, _L, range, [{integer, _, From}, {integer, _, To}]}, 
-	    _RecDict, _VarDict) -> 
-  t_from_range(From, To);
-t_from_form({type, _L, record, [Name|Fields]}, RecDict, VarDict) -> 
-  record_from_form(Name, Fields, RecDict, VarDict);
-t_from_form({type, _L, reference, []}, _RecDict, _VarDict) -> t_reference();
-t_from_form({type, _L, set, []}, _RecDict, _VarDict) -> t_set();
-t_from_form({type, _L, string, []}, _RecDict, _VarDict) -> t_string();
-t_from_form({type, _L, term, []}, _RecDict, _VarDict) -> t_any();
-t_from_form({type, _L, tid, []}, _RecDict, _VarDict) -> t_tid();
-t_from_form({type, _L, timeout, []}, _RecDict, _VarDict) -> t_timeout();
-t_from_form({type, _L, tuple, any}, _RecDict, _VarDict) -> t_tuple();
-t_from_form({type, _L, tuple, Args}, RecDict, VarDict) -> 
-  t_tuple([t_from_form(A, RecDict, VarDict) || A <- Args]);
-t_from_form({type, _L, union, Args}, RecDict, VarDict) -> 
-  t_sup([t_from_form(A, RecDict, VarDict) || A <- Args]);
-t_from_form({type, _L, Name, Args}, RecDict, VarDict) ->
+	    _TypeNames, _RecDict, _VarDict) ->
+  {t_from_range(From, To), []};
+t_from_form({type, _L, record, [Name|Fields]}, TypeNames, RecDict, VarDict) ->
+  record_from_form(Name, Fields, TypeNames, RecDict, VarDict);
+t_from_form({type, _L, reference, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_reference(), []};
+t_from_form({type, _L, set, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_set(), []};
+t_from_form({type, _L, string, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_string(), []};
+t_from_form({type, _L, term, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_any(), []};
+t_from_form({type, _L, tid, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_tid(), []};
+t_from_form({type, _L, timeout, []}, _TypeNames, _RecDict, _VarDict) ->
+  {t_timeout(), []};
+t_from_form({type, _L, tuple, any}, _TypeNames, _RecDict, _VarDict) ->
+  {t_tuple(), []};
+t_from_form({type, _L, tuple, Args}, TypeNames, RecDict, VarDict) ->
+  {L, R} = list_from_form(Args, TypeNames, RecDict, VarDict),
+  {t_tuple(L), R};
+t_from_form({type, _L, union, Args}, TypeNames, RecDict, VarDict) ->
+  {L, R} = list_from_form(Args, TypeNames, RecDict, VarDict),
+  {t_sup(L), R};
+t_from_form({type, _L, Name, Args}, TypeNames, RecDict, VarDict) ->
   case lookup_type(Name, RecDict) of
     {type, {_Module, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
-      List = lists:zipwith(fun(ArgName, ArgType) -> 
-			       {ArgName, t_from_form(ArgType, RecDict, VarDict)}
-			   end, ArgNames, Args),
-      TmpVardict = dict:from_list(List),
-      t_from_form(Type, RecDict, TmpVardict);
+      case unfold({type, Name}, TypeNames) of
+        true ->
+          List = lists:zipwith(
+                   fun(ArgName, ArgType) ->
+                       {Ttemp, _R} = t_from_form(ArgType, TypeNames,
+                                                     RecDict, VarDict),
+                       {ArgName, Ttemp}
+                   end,
+                   ArgNames, Args),
+          TmpVarDict = dict:from_list(List),
+          {T, R} = t_from_form(Type, [{type, Name}|TypeNames], RecDict,
+                               TmpVarDict),
+          case lists:member({type, Name}, R) of
+            true -> {t_limit(T, ?REC_TYPE_LIMIT), R};
+            false -> {T, R}
+          end;
+        false -> {t_any(), [{type, Name}]}
+      end;
     {opaque, {Module, Type, ArgNames}} when length(Args) =:= length(ArgNames) ->
-      List = lists:zipwith(fun(ArgName, ArgType) -> 
-			       {ArgName, t_from_form(ArgType, RecDict, VarDict)}
-			   end, ArgNames, Args),
-      TmpVardict = dict:from_list(List),
-      Rep = t_from_form(Type, RecDict, TmpVardict),
-      t_from_form({opaque, -1, Name, {Module, Args, Rep}}, RecDict, VarDict);
+      {Rep, Rret} =
+        case unfold({opaque, Name}, TypeNames) of
+          true ->
+            List = lists:zipwith(
+                     fun(ArgName, ArgType) ->
+                         {Ttemp, _R} =  t_from_form(ArgType, TypeNames,
+                                                    RecDict, VarDict),
+                         {ArgName, Ttemp}
+                     end,
+                     ArgNames, Args),
+            TmpVarDict = dict:from_list(List),
+            {T, R} = t_from_form(Type, [{opaque, Name}|TypeNames], RecDict,
+                                 TmpVarDict),
+            case lists:member({opaque, Name}, R) of
+              true -> {t_limit(T, ?REC_TYPE_LIMIT), R};
+              false -> {T, R}
+            end;
+          false -> {t_any(), [{opaque, Name}]}
+        end,
+      Tret = t_from_form({opaque, -1, Name, {Module, Args, Rep}},
+                         RecDict, VarDict),
+      {Tret, Rret};
     {type, _} ->
       throw({error, io_lib:format("Unknown type ~w\n", [Name])});
     {opaque, _} ->
@@ -3361,48 +3578,70 @@ t_from_form({type, _L, Name, Args}, RecDict, VarDict) ->
     error ->
       throw({error, io_lib:format("Unable to find type ~w\n", [Name])}) 
   end;
-t_from_form({opaque, _L, Name, {Mod, Args, Rep}}, _RecDict, _VarDict) -> 
+t_from_form({opaque, _L, Name, {Mod, Args, Rep}}, _TypeNames, _RecDict,
+            _VarDict) ->
   case Args of
-    [] -> t_opaque(Mod, Name, Args, Rep);
+    [] -> {t_opaque(Mod, Name, Args, Rep), []};
     _ -> throw({error, "Polymorphic opaque types not supported yet"})
   end.
 
-record_from_form({atom, _, Name}, ModFields, RecDict, VarDict) ->
-  case lookup_record(Name, RecDict) of
-    {ok, DeclFields} ->
-      case get_mod_record(ModFields, DeclFields, RecDict, VarDict) of
-	{error, FieldName} ->
-	  throw({error, io_lib:format("Illegal declaration of ~w#{~w}\n", 
-				      [Name, FieldName])});
-	{ok, NewFields} ->
-	  t_tuple([t_atom(Name)|[Type || {_FieldName, Type} <- NewFields]])
+record_from_form({atom, _, Name}, ModFields, TypeNames, RecDict, VarDict) ->
+  case unfold({record, Name}, TypeNames) of
+    true ->
+      case lookup_record(Name, RecDict) of
+        {ok, DeclFields} ->
+          TypeNames1 = [{record, Name}|TypeNames],
+          AreTyped = [is_erl_type(FieldType)
+                      || {_FieldName, FieldType} <- DeclFields],
+          {DeclFields1, R1} =
+            case lists:all(fun(Elem) -> Elem end, AreTyped) of
+              true -> {DeclFields, []};
+              false -> fields_from_form(DeclFields, TypeNames1,
+                                        RecDict, dict:new())
+            end,
+          {GetModRec, R2} = get_mod_record(ModFields, DeclFields1,
+                                           TypeNames1, RecDict, VarDict),
+          case GetModRec of
+            {error, FieldName} ->
+              throw({error, io_lib:format("Illegal declaration of ~w#{~w}\n",
+                                          [Name, FieldName])});
+            {ok, NewFields} ->
+              {t_tuple(
+                 [t_atom(Name)|[Type || {_FieldName, Type} <- NewFields]]),
+               R1 ++ R2}
+          end;
+        error ->
+          throw({error, erlang:error(io_lib:format("Unknown record #~w{}\n",
+                                                   [Name]))})
       end;
-    error ->
-      throw({error, 
-	     erlang:error(io_lib:format("Unknown record #~w{}\n", [Name]))})
+    false -> {t_any(), []}
   end.
 
-get_mod_record([], DeclFields, _RecDict, _VarDict) ->
-  {ok, DeclFields};
-get_mod_record(ModFields, DeclFields, RecDict, VarDict) ->
+get_mod_record([], DeclFields, _TypeNames, _RecDict, _VarDict) ->
+  {{ok, DeclFields}, []};
+get_mod_record(ModFields, DeclFields, TypeNames, RecDict, VarDict) ->
   DeclFieldsDict = orddict:from_list(DeclFields),
-  ModFieldsDict = build_field_dict(ModFields, RecDict, VarDict),
+  {ModFieldsDict, R} = build_field_dict(ModFields, TypeNames,
+                                        RecDict, VarDict),
   case get_mod_record(DeclFieldsDict, ModFieldsDict, []) of
-    {error, _FieldName} = Error -> Error;
+    {error, _FieldName} = Error -> {Error, R};
     {ok, FinalOrdDict} ->
-      {ok, [{FieldName, orddict:fetch(FieldName, FinalOrdDict)}
-	    || {FieldName, _} <- DeclFields]}
+      {{ok, [{FieldName, orddict:fetch(FieldName, FinalOrdDict)}
+             || {FieldName, _} <- DeclFields]},
+       R}
   end.
 
-build_field_dict(FieldTypes, RecDict, VarDict) ->
-  build_field_dict(FieldTypes, RecDict, VarDict, []).
+build_field_dict(FieldTypes, TypeNames, RecDict, VarDict) ->
+  build_field_dict(FieldTypes, TypeNames, RecDict, VarDict, []).
 
 build_field_dict([{type, _, field_type, [{atom, _, Name}, Type]}|Left], 
-		 RecDict, VarDict, Acc) ->
-  NewAcc = [{Name, t_from_form(Type, RecDict, VarDict)}|Acc],
-  build_field_dict(Left, RecDict, VarDict, NewAcc);
-build_field_dict([], _RecDict, _VarDict, Acc) ->
-  orddict:from_list(Acc).
+		 TypeNames, RecDict, VarDict, Acc) ->
+  {T, R1} = t_from_form(Type, TypeNames, RecDict, VarDict),
+  NewAcc = [{Name, T}|Acc],
+  {D, R2} = build_field_dict(Left, TypeNames, RecDict, VarDict, NewAcc),
+  {D, R1 ++ R2};
+build_field_dict([], _TypeNames, _RecDict, _VarDict, Acc) ->
+  {orddict:from_list(Acc), []}.
 
 get_mod_record([{FieldName, DeclType}|Left1], 
 	       [{FieldName, ModType}|Left2], Acc) ->
@@ -3419,6 +3658,20 @@ get_mod_record(DeclFields, [], Acc) ->
 get_mod_record(_, [{FieldName2, _ModType}|_], _Acc) ->
   {error, FieldName2}.
 
+fields_from_form([], _TypeNames, _RecDict, _VarDict) ->
+  {[], []};
+fields_from_form([{Name, Type}|Tail], TypeNames, RecDict, VarDict) ->
+  {T, R1} = t_from_form(Type, TypeNames, RecDict, VarDict),
+  {F, R2} = fields_from_form(Tail, TypeNames, RecDict, VarDict),
+  {[{Name, T}|F], R1 ++ R2}.
+
+list_from_form([], _TypeNames, _RecDict, _VarDict) ->
+  {[], []};
+list_from_form([H|Tail], TypeNames, RecDict, VarDict) ->
+  {T, R1} = t_from_form(H, TypeNames, RecDict, VarDict),
+  {L, R2} = list_from_form(Tail, TypeNames, RecDict, VarDict),
+  {[T|L], R1 ++ R2}.
+
 -spec t_form_to_string(parse_form()) -> string().
 
 t_form_to_string({var, _L, '_'}) -> "_";
@@ -3510,11 +3763,19 @@ any_none_or_unit([?unit|_]) -> true;
 any_none_or_unit([_|Left]) -> any_none_or_unit(Left);
 any_none_or_unit([]) -> false.
 
--spec lookup_record(atom(), dict()) -> 'error' | {'ok', [{atom(), erl_type()}]}.
+is_erl_type(?any) -> true;
+is_erl_type(?none) -> true;
+is_erl_type(?unit) -> true;
+is_erl_type(#c{}) -> true;
+is_erl_type(_) -> false.
+
+-spec lookup_record(atom(), dict()) ->
+        'error' | {'ok', [{atom(), parse_form() | erl_type()}]}.
 
 lookup_record(Tag, RecDict) when is_atom(Tag) ->
   case dict:find({record, Tag}, RecDict) of
-    {ok, [{_Arity, Fields}]} -> {ok, Fields};
+    {ok, [{_Arity, Fields}]} ->
+      {ok, Fields};
     {ok, List} when is_list(List) ->
       %% This will have to do, since we do not know which record we
       %% are looking for.
@@ -3547,6 +3808,9 @@ lookup_type(Name, RecDict) ->
 type_is_defined(TypeOrOpaque, Name, RecDict) ->
   dict:is_key({TypeOrOpaque, Name}, RecDict).
 
+unfold(TypeName, TypeNames) ->
+  not lists:member(TypeName, TypeNames).
+
 %% -----------------------------------
 %% Set
 %%