add type constraints in dynamic types

git-svn-id: https://svn.cs.ru.nl/repos/clean-compiler/trunk@2221 1f8540f1-abd5-4d5b-9d24-4c5ce8603e2d

8 files changed, 191 insertions, 103 deletions

diff --git a/frontend/analtypes.icl b/frontend/analtypes.icl
index 6019bd8..694e66a 100644
--- a/frontend/analtypes.icl
+++ b/frontend/analtypes.icl
@@ -1110,7 +1110,7 @@ where
 
 	check_kinds_of_icl_fuction common_defs fun_index (icl_fun_defs, class_infos, expression_heap, as)
 		# ({fun_type,fun_ident,fun_info,fun_pos}, icl_fun_defs) = icl_fun_defs![fun_index]
-		  (expression_heap,as) = check_kinds_of_dynamics common_defs fun_info.fi_dynamics expression_heap as
+		  (expression_heap,class_infos,as) = check_kinds_of_dynamics common_defs fun_info.fi_dynamics expression_heap class_infos as
 		= case fun_type of
 			Yes symbol_type
 				# as_error = pushErrorAdmin (newPosition fun_ident fun_pos) as.as_error
@@ -1135,38 +1135,56 @@ where
 	check_kinds_of_symbol_type common_defs {st_vars,st_result,st_args,st_context} class_infos as=:{as_type_var_heap,as_kind_heap}
 		# (as_type_var_heap, as_kind_heap) = bindFreshKindVariablesToTypeVars st_vars as_type_var_heap as_kind_heap
 		  as = {as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
-		  as = determine_kinds_type_list common_defs [st_result:st_args] as
+		  as = force_star_kind common_defs st_result as
+		  (class_infos,as) = check_kinds_of_function_arguments st_args common_defs class_infos as
 		= determine_kinds_of_type_contexts common_defs st_context class_infos as
-
-	check_kinds_of_dynamics :: {#CommonDefs} [DynamicPtr] *ExpressionHeap *AnalyseState -> (*ExpressionHeap, *AnalyseState)
-	check_kinds_of_dynamics common_defs dynamic_ptrs expr_heap as
-		= foldSt (check_kinds_of_dynamic common_defs) dynamic_ptrs (expr_heap, as)
 	where
-		check_kinds_of_dynamic :: {#CommonDefs} DynamicPtr (*ExpressionHeap, *AnalyseState) -> (*ExpressionHeap, *AnalyseState)
-		check_kinds_of_dynamic common_defs dynamic_ptr (expr_heap,as)
+		check_kinds_of_function_arguments :: [AType] {#CommonDefs} !*ClassDefInfos !*AnalyseState -> (!*ClassDefInfos, !*AnalyseState)
+		check_kinds_of_function_arguments [{at_type=TFAC vars type contexts}:types] common_defs class_infos as
+			# (as_type_var_heap, as_kind_heap) = new_local_kind_variables_for_universal_vars vars as.as_type_var_heap as.as_kind_heap
+			  as = {as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
+			  as = force_star_kind common_defs type as
+			  (class_infos,as) = determine_kinds_of_type_contexts common_defs contexts class_infos as
+			= check_kinds_of_function_arguments types common_defs class_infos as
+		check_kinds_of_function_arguments [type:types] common_defs class_infos as
+			= check_kinds_of_function_arguments types common_defs class_infos (force_star_kind common_defs type as)
+		check_kinds_of_function_arguments [] common_defs class_infos as
+			= (class_infos,as)
+
+	check_kinds_of_dynamics :: {#CommonDefs} [DynamicPtr] *ExpressionHeap *ClassDefInfos *AnalyseState -> (!*ExpressionHeap,!*ClassDefInfos,!*AnalyseState)
+	check_kinds_of_dynamics common_defs dynamic_ptrs expr_heap class_infos as
+		= foldSt (check_kinds_of_dynamic common_defs) dynamic_ptrs (expr_heap,class_infos,as)
+	where
+		check_kinds_of_dynamic :: {#CommonDefs} DynamicPtr (*ExpressionHeap,*ClassDefInfos,*AnalyseState) -> (!*ExpressionHeap,!*ClassDefInfos,!*AnalyseState)
+		check_kinds_of_dynamic common_defs dynamic_ptr (expr_heap,class_infos,as)
 			# (dynamic_info, expr_heap) = readPtr dynamic_ptr expr_heap
-			= check_kinds_of_dynamic_info common_defs dynamic_info (expr_heap, as)
+			= check_kinds_of_dynamic_info dynamic_info common_defs (expr_heap,class_infos,as)
 
-		check_kinds_of_dynamic_info :: {#CommonDefs} ExprInfo (*ExpressionHeap, *AnalyseState) -> (*ExpressionHeap, *AnalyseState)
-		check_kinds_of_dynamic_info	common_defs (EI_Dynamic opt_type locals) (expr_heap, as)
-			# as = check_kinds_of_opt_dynamic_type common_defs opt_type as
-			= check_kinds_of_dynamics common_defs locals expr_heap as
-		check_kinds_of_dynamic_info	common_defs (EI_DynamicTypeWithVars	vars type locals) (expr_heap, as=:{as_type_var_heap,as_kind_heap})
+		check_kinds_of_dynamic_info :: ExprInfo {#CommonDefs} (*ExpressionHeap,*ClassDefInfos,*AnalyseState) -> (!*ExpressionHeap,!*ClassDefInfos,!*AnalyseState)
+		check_kinds_of_dynamic_info	(EI_Dynamic opt_type locals) common_defs (expr_heap,class_infos,as)
+			# (class_infos,as) = check_kinds_of_opt_dynamic_type common_defs opt_type class_infos as
+			= check_kinds_of_dynamics common_defs locals expr_heap class_infos as
+		check_kinds_of_dynamic_info	(EI_DynamicTypeWithVars	vars type locals) common_defs (expr_heap,class_infos,as=:{as_type_var_heap,as_kind_heap})
 			# (as_type_var_heap, as_kind_heap) = bindFreshKindVariablesToTypeVars vars as_type_var_heap as_kind_heap
-			  as = check_kinds_of_dynamic_type common_defs type { as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
-			= check_kinds_of_dynamics common_defs locals expr_heap as
-
-		check_kinds_of_opt_dynamic_type :: {#CommonDefs} (Optional DynamicType) *AnalyseState -> *AnalyseState
-		check_kinds_of_opt_dynamic_type	common_defs (Yes type) as
-			= check_kinds_of_dynamic_type common_defs type as
-		check_kinds_of_opt_dynamic_type	common_defs No as
-			= as
-
-		check_kinds_of_dynamic_type :: {#CommonDefs} DynamicType *AnalyseState -> *AnalyseState
-		check_kinds_of_dynamic_type	common_defs {dt_type, dt_uni_vars, dt_global_vars} as=:{as_type_var_heap,as_kind_heap}
-			# (as_type_var_heap, as_kind_heap) = bindFreshKindVariablesToTypeVars [atv_variable \\ {atv_variable} <- dt_uni_vars] as_type_var_heap as_kind_heap
+			  (class_infos,as) = check_kinds_of_dynamic_type common_defs type class_infos {as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
+			= check_kinds_of_dynamics common_defs locals expr_heap class_infos as
+		check_kinds_of_dynamic_info	(EI_UnmarkedDynamic _ _) common_defs (expr_heap,class_infos,as)
+			// EI_UnmarkedDynamic can only occur here (instead of EI_Dynamic) in an unused local function,
+			// because collectVariables is not called for unused local functions, therefore we ignore it
+			= (expr_heap,class_infos,as)
+
+		check_kinds_of_opt_dynamic_type :: {#CommonDefs} (Optional DynamicType) *ClassDefInfos *AnalyseState -> (!*ClassDefInfos,!*AnalyseState)
+		check_kinds_of_opt_dynamic_type	common_defs (Yes type) class_infos as
+			= check_kinds_of_dynamic_type common_defs type class_infos as
+		check_kinds_of_opt_dynamic_type	common_defs No class_infos as
+			= (class_infos,as)
+
+		check_kinds_of_dynamic_type :: {#CommonDefs} DynamicType *ClassDefInfos *AnalyseState -> (!*ClassDefInfos,!*AnalyseState)
+		check_kinds_of_dynamic_type	common_defs {dt_type,dt_uni_vars,dt_global_vars,dt_contexts} class_infos as=:{as_type_var_heap,as_kind_heap}
+			# (as_type_var_heap, as_kind_heap) = new_local_kind_variables_for_universal_vars dt_uni_vars as_type_var_heap as_kind_heap
 			  (as_type_var_heap, as_kind_heap) = bindFreshKindVariablesToTypeVars dt_global_vars as_type_var_heap as_kind_heap
-			= determine_kinds_type_list common_defs [dt_type] { as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
+			  as = force_star_kind common_defs dt_type { as & as_type_var_heap = as_type_var_heap, as_kind_heap = as_kind_heap}
+			= determine_kinds_of_type_contexts common_defs dt_contexts class_infos as
 
 instance <<< DynamicType
 where
diff --git a/frontend/check.icl b/frontend/check.icl
index 1e82c61..5c193be 100644
--- a/frontend/check.icl
+++ b/frontend/check.icl
@@ -793,8 +793,8 @@ checkFunction fun_def=:{fun_ident,fun_pos,fun_body,fun_type,fun_kind} mod_index
 	  (fun_body, free_vars, e_state, e_info, cs) = checkFunctionBodies fun_body function_ident_for_errors e_input e_state e_info cs
 
 	# {es_fun_defs,es_calls,es_var_heap,es_expr_heap,es_type_heaps,es_generic_heap,es_dynamics} = e_state
-	  (ef_type_defs, ef_modules, es_type_heaps, es_expr_heap, cs) = 
-	  	checkDynamicTypes mod_index es_dynamics fun_type e_info.ef_type_defs e_info.ef_modules es_type_heaps es_expr_heap cs
+	  (ef_type_defs, ef_class_defs, ef_modules, es_type_heaps, es_expr_heap, cs) = 
+	  	checkDynamicTypes mod_index es_dynamics fun_type e_info.ef_type_defs e_info.ef_class_defs e_info.ef_modules es_type_heaps es_expr_heap cs
 	  (fun_body, cs_error) = checkFunctionBodyIfMacro fun_kind fun_body cs.cs_error
 	  cs = { cs & cs_error = popErrorAdmin cs_error }
 	  fi_properties = (if ef_is_macro_fun FI_IsMacroFun 0) bitor (has_type fun_type)
@@ -804,7 +804,7 @@ checkFunction fun_def=:{fun_ident,fun_pos,fun_body,fun_type,fun_kind} mod_index
 	  fun_def = { fun_def & fun_body = fun_body, fun_info = fun_info, fun_type = fun_type}
 	  (fun_defs,macro_defs,cs_symbol_table) = remove_calls_from_symbol_table fun_index def_level es_calls e_state.es_fun_defs e_info.ef_macro_defs cs.cs_symbol_table
 	= (fun_def,fun_defs,
-			{e_info & ef_type_defs=ef_type_defs, ef_modules=ef_modules, ef_macro_defs=macro_defs},
+			{e_info & ef_type_defs=ef_type_defs, ef_class_defs=ef_class_defs, ef_modules=ef_modules,ef_macro_defs=macro_defs},
 			{heaps & hp_var_heap = es_var_heap, hp_expression_heap = es_expr_heap, hp_type_heaps = es_type_heaps,hp_generic_heap=es_generic_heap},
 			{cs & cs_symbol_table = cs_symbol_table})
 where
diff --git a/frontend/checktypes.dcl b/frontend/checktypes.dcl
index 1cc34b4..07e50f7 100644
--- a/frontend/checktypes.dcl
+++ b/frontend/checktypes.dcl
@@ -19,8 +19,8 @@ checkSuperClasses :: ![TypeVar] ![TypeContext] !Index !u:{# CheckedTypeDef} !v:{
 	-> (![TypeVar], ![TypeContext], !u:{#CheckedTypeDef}, !v:{# ClassDef}, !u:{# DclModule}, !*TypeHeaps, !*CheckState)
 
 checkDynamicTypes :: !Index ![ExprInfoPtr] !(Optional SymbolType)
-		!u:{#CheckedTypeDef} !u:{#DclModule} !*TypeHeaps !*ExpressionHeap !*CheckState
-	-> (!u:{#CheckedTypeDef},!u:{#DclModule},!*TypeHeaps,!*ExpressionHeap,!*CheckState)
+		!u:{#CheckedTypeDef} !v:{#ClassDef} !u:{#DclModule} !*TypeHeaps !*ExpressionHeap !*CheckState
+	-> (!u:{#CheckedTypeDef},!v:{#ClassDef},!u:{#DclModule},!*TypeHeaps,!*ExpressionHeap,!*CheckState)
 
 createClassDictionaries ::		  !Bool !Index !Index !Index !Index !*{#CheckedTypeDef} !*{# SelectorDef} !*{# ConsDef} !*{#ClassDef} !*{#DclModule} !*TypeVarHeap !*VarHeap !*SymbolTable
 	-> (![CheckedTypeDef],![SelectorDef],![ConsDef],!DictionaryInfo,!*{#CheckedTypeDef},!*{# SelectorDef},!*{# ConsDef},!*{#ClassDef},!*{#DclModule},!*TypeVarHeap,!*VarHeap,!*SymbolTable)
diff --git a/frontend/checktypes.icl b/frontend/checktypes.icl
index 722e060..5c88c76 100644
--- a/frontend/checktypes.icl
+++ b/frontend/checktypes.icl
@@ -1226,12 +1226,12 @@ where
 					 cs_error			= checkError av_ident "attribute variable in context undefined" cs_error}
 
 checkDynamicTypes :: !Index ![ExprInfoPtr] !(Optional SymbolType)
-		!u:{#CheckedTypeDef} !u:{#DclModule} !*TypeHeaps !*ExpressionHeap !*CheckState
-	-> (!u:{#CheckedTypeDef},!u:{#DclModule},!*TypeHeaps,!*ExpressionHeap,!*CheckState)
-checkDynamicTypes mod_index dyn_type_ptrs No type_defs modules type_heaps expr_heap cs
-	# (type_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs modules type_heaps expr_heap cs
+		!u:{#CheckedTypeDef} !v:{#ClassDef} !u:{#DclModule} !*TypeHeaps !*ExpressionHeap !*CheckState
+	-> (!u:{#CheckedTypeDef},!v:{#ClassDef},!u:{#DclModule},!*TypeHeaps,!*ExpressionHeap,!*CheckState)
+checkDynamicTypes mod_index dyn_type_ptrs No type_defs class_defs modules type_heaps expr_heap cs
+	# (type_defs, class_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs class_defs modules type_heaps expr_heap cs
 	  (expr_heap, cs_symbol_table) = remove_global_type_variables_in_dynamics dyn_type_ptrs (expr_heap, cs.cs_symbol_table)
-	= (type_defs, modules, heaps, expr_heap, { cs & cs_symbol_table = cs_symbol_table })
+	= (type_defs, class_defs, modules, heaps, expr_heap, { cs & cs_symbol_table = cs_symbol_table })
 where
 	remove_global_type_variables_in_dynamics dyn_info_ptrs expr_heap_and_symbol_table
 		= foldSt remove_global_type_variables_in_dynamic dyn_info_ptrs expr_heap_and_symbol_table
@@ -1254,13 +1254,14 @@ where
 				| entry.ste_kind == STE_Empty
 					= symbol_table
 					= symbol_table <:= (id_info, entry.ste_previous)
-checkDynamicTypes mod_index dyn_type_ptrs (Yes {st_vars}) type_defs modules type_heaps expr_heap cs=:{cs_symbol_table}
+checkDynamicTypes mod_index dyn_type_ptrs (Yes {st_vars}) type_defs class_defs modules type_heaps expr_heap cs=:{cs_symbol_table}
 	# (th_vars, cs_symbol_table) = foldSt add_type_variable_to_symbol_table st_vars (type_heaps.th_vars, cs_symbol_table)
-	  (type_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs modules
+	  (type_defs, class_defs, modules, heaps, expr_heap, cs)
+	  	= checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs class_defs modules
 	  		{ type_heaps & th_vars = th_vars } expr_heap { cs & cs_symbol_table = cs_symbol_table }
 	  cs_symbol_table =	removeVariablesFromSymbolTable cModuleScope st_vars cs.cs_symbol_table
 	  (expr_heap, cs) = check_global_type_variables_in_dynamics dyn_type_ptrs (expr_heap, { cs & cs_symbol_table = cs_symbol_table })
-	= (type_defs, modules, heaps, expr_heap, cs) 
+	= (type_defs, class_defs, modules, heaps, expr_heap, cs) 
 where
 	add_type_variable_to_symbol_table {tv_ident={id_info},tv_info_ptr} (var_heap,symbol_table)
 		# (entry, symbol_table) = readPtr id_info symbol_table
@@ -1291,54 +1292,76 @@ where
 					= { cs & cs_symbol_table = cs_symbol_table <:= (id_info, entry.ste_previous),
 							 cs_error = checkError tv_ident.id_name "global type variable not used in type of the function" cs_error }
 
-checkDynamics mod_index scope dyn_type_ptrs type_defs modules type_heaps expr_heap cs
-	= foldSt (check_dynamic mod_index scope) dyn_type_ptrs (type_defs, modules, type_heaps, expr_heap, cs)
+checkDynamics mod_index scope dyn_type_ptrs type_defs class_defs modules type_heaps expr_heap cs
+	= foldSt (check_dynamic mod_index scope) dyn_type_ptrs (type_defs, class_defs, modules, type_heaps, expr_heap, cs)
 where	
-	check_dynamic mod_index scope dyn_info_ptr (type_defs, modules, type_heaps, expr_heap, cs)
+	check_dynamic mod_index scope dyn_info_ptr (type_defs, class_defs, modules, type_heaps, expr_heap, cs)
 		# (dyn_info, expr_heap) = readPtr dyn_info_ptr expr_heap
 		= case dyn_info of
 			EI_UnmarkedDynamic opt_type loc_dynamics
 				-> case opt_type of
 					Yes dyn_type
-						# (dyn_type, loc_type_vars, type_defs, modules, type_heaps, cs) = check_dynamic_type mod_index scope dyn_type type_defs modules type_heaps cs
+						# (dyn_type, loc_type_vars, type_defs, class_defs, modules, type_heaps, cs)
+							= check_dynamic_type_in_pattern mod_index scope dyn_type type_defs class_defs modules type_heaps cs
 						| isEmpty loc_type_vars
 							# expr_heap =  expr_heap <:= (dyn_info_ptr, EI_UnmarkedDynamic (Yes dyn_type) loc_dynamics)
-				  		  	-> check_local_dynamics mod_index scope loc_dynamics type_defs modules type_heaps expr_heap cs
+				  		  	-> check_local_dynamics mod_index scope loc_dynamics type_defs class_defs modules type_heaps expr_heap cs
 				  			# cs_symbol_table = removeVariablesFromSymbolTable scope loc_type_vars cs.cs_symbol_table
 							  cs_error = checkError loc_type_vars "type variable(s) not defined" cs.cs_error
 							  expr_heap = expr_heap <:= (dyn_info_ptr, EI_UnmarkedDynamic (Yes dyn_type) loc_dynamics)
-							-> (type_defs, modules, type_heaps, expr_heap, {cs & cs_error = cs_error, cs_symbol_table = cs_symbol_table})
+							-> (type_defs, class_defs, modules, type_heaps, expr_heap, {cs & cs_error = cs_error, cs_symbol_table = cs_symbol_table})
 					No
-				  		 -> check_local_dynamics mod_index scope loc_dynamics type_defs modules type_heaps expr_heap cs
+				  		 -> check_local_dynamics mod_index scope loc_dynamics type_defs class_defs modules type_heaps expr_heap cs
 			EI_DynamicType dyn_type loc_dynamics
-				# (dyn_type, loc_type_vars, type_defs, modules, type_heaps, cs) = check_dynamic_type mod_index scope dyn_type type_defs modules type_heaps cs
-				  (type_defs, modules, type_heaps, expr_heap, cs) = check_local_dynamics mod_index scope loc_dynamics type_defs modules type_heaps expr_heap cs
+				# (dyn_type, loc_type_vars, type_defs, class_defs, modules, type_heaps, cs)
+					= check_dynamic_type_in_pattern mod_index scope dyn_type type_defs class_defs modules type_heaps cs
+				  (type_defs, class_defs, modules, type_heaps, expr_heap, cs)
+				  	= check_local_dynamics mod_index scope loc_dynamics type_defs class_defs modules type_heaps expr_heap cs
 				  cs_symbol_table = removeVariablesFromSymbolTable scope loc_type_vars cs.cs_symbol_table
 				  expr_heap = expr_heap <:= (dyn_info_ptr, EI_DynamicTypeWithVars loc_type_vars dyn_type loc_dynamics)
-				-> (type_defs, modules, type_heaps, expr_heap, {cs & cs_symbol_table = cs_symbol_table})
+				-> (type_defs, class_defs, modules, type_heaps, expr_heap, {cs & cs_symbol_table = cs_symbol_table}) 
 
-	check_local_dynamics mod_index scope local_dynamics type_defs modules type_heaps expr_heap cs
-		= foldSt (check_dynamic mod_index (inc scope)) local_dynamics (type_defs, modules, type_heaps, expr_heap, cs)
+	check_local_dynamics mod_index scope local_dynamics type_defs class_defs modules type_heaps expr_heap cs
+		= foldSt (check_dynamic mod_index (inc scope)) local_dynamics (type_defs, class_defs, modules, type_heaps, expr_heap, cs)
 
-	check_dynamic_type mod_index scope dt=:{dt_uni_vars,dt_type} type_defs modules type_heaps=:{th_vars} cs
+	check_dynamic_type_in_expression mod_index scope dt=:{dt_uni_vars,dt_type,dt_contexts} type_defs class_defs modules type_heaps=:{th_vars} cs
 		# (dt_uni_vars, (th_vars, cs)) = add_type_variables_to_symbol_table scope dt_uni_vars th_vars cs
 		  ots = { ots_type_defs = type_defs, ots_modules = modules }
 		  oti = { oti_heaps = { type_heaps & th_vars = th_vars }, oti_all_vars = [], oti_all_attrs = [], oti_global_vars = [] }
-		  (dt_type, ( {ots_type_defs, ots_modules}, {oti_heaps,oti_all_vars,oti_all_attrs, oti_global_vars}, cs))
+
+		  (contexts, type_defs, class_defs, modules, heaps, cs)
+		  	= checkTypeContexts dt_contexts mod_index class_defs ots {oti & oti_all_vars=[],oti_all_attrs=[],oti_global_vars=[]} cs
+		  oti = {oti & oti_heaps=heaps}
+		  ots = {ots_modules = modules, ots_type_defs = type_defs}
+
+		  (dt_type, ({ots_type_defs, ots_modules}, oti, cs))
+		  		= checkOpenAType mod_index scope DAK_None dt_type (ots, oti, { cs & cs_x = {cs.cs_x & x_check_dynamic_types = True} })
+		= check_dynamic_type_uniqueness dt_type dt_uni_vars contexts oti ots_type_defs ots_modules class_defs cs
+
+	check_dynamic_type_in_pattern mod_index scope dt=:{dt_uni_vars,dt_type,dt_contexts} type_defs class_defs modules type_heaps=:{th_vars} cs
+		# (dt_uni_vars, (th_vars, cs)) = add_type_variables_to_symbol_table scope dt_uni_vars th_vars cs
+		  ots = { ots_type_defs = type_defs, ots_modules = modules }
+		  oti = { oti_heaps = { type_heaps & th_vars = th_vars }, oti_all_vars = [], oti_all_attrs = [], oti_global_vars = [] }
+		  (dt_type, (ots, oti, cs))
 		  		= checkOpenAType mod_index scope DAK_None dt_type (ots, oti, { cs & cs_x = {cs.cs_x & x_check_dynamic_types = True} })
-		  cs = check_dynamic_uniqueness dt_type.at_attribute cs
-		  
-		  oti = { oti &  oti_all_vars = [], oti_all_attrs = [], oti_global_vars=oti_global_vars, oti_heaps = oti_heaps }
 
-		# cs = { cs & cs_x = {cs.cs_x & x_check_dynamic_types = False} }
+		  (contexts, type_defs, class_defs, modules, heaps, cs)
+		  	= checkTypeContexts dt_contexts mod_index class_defs ots {oti & oti_all_vars=[],oti_all_attrs=[],oti_global_vars=[]} cs
+		  oti = {oti & oti_heaps=heaps}
+
+		= check_dynamic_type_uniqueness dt_type dt_uni_vars contexts oti type_defs modules class_defs cs
+
+	check_dynamic_type_uniqueness dt_type dt_uni_vars contexts {oti_heaps,oti_all_vars,oti_all_attrs, oti_global_vars} ots_type_defs ots_modules class_defs cs
+		# cs = check_dynamic_uniqueness dt_type.at_attribute cs
+		  cs = { cs & cs_x = {cs.cs_x & x_check_dynamic_types = False} }
 		  th_vars = foldSt (\{tv_info_ptr} -> writePtr tv_info_ptr TVI_Empty) oti_global_vars oti_heaps.th_vars
 	  	  cs_symbol_table = removeAttributedTypeVarsFromSymbolTable scope dt_uni_vars cs.cs_symbol_table
-		  dt = {dt_uni_vars = dt_uni_vars, dt_global_vars = oti_global_vars, dt_type = dt_type}
+		  dt = { dt_uni_vars = dt_uni_vars, dt_global_vars = oti_global_vars, dt_type = dt_type, dt_contexts=contexts }
 		| isEmpty oti_all_attrs
-			= (dt, oti_all_vars, ots_type_defs, ots_modules, {oti_heaps & th_vars = th_vars}, {cs & cs_symbol_table = cs_symbol_table})
+			= (dt, oti_all_vars, ots_type_defs, class_defs, ots_modules, {oti_heaps & th_vars = th_vars}, {cs & cs_symbol_table = cs_symbol_table})
 			# cs_symbol_table = removeAttributesFromSymbolTable oti_all_attrs cs_symbol_table
 			  cs_error = checkError (hd oti_all_attrs).av_ident "type attribute variable not allowed" cs.cs_error
-			= (dt, oti_all_vars, ots_type_defs, ots_modules, {oti_heaps & th_vars = th_vars }, {cs & cs_symbol_table = cs_symbol_table, cs_error = cs_error})
+			= (dt, oti_all_vars, ots_type_defs, class_defs, ots_modules, {oti_heaps & th_vars = th_vars}, {cs & cs_symbol_table = cs_symbol_table, cs_error = cs_error})
 		where
 			check_dynamic_uniqueness TA_None cs
 				=	cs
diff --git a/frontend/overloading.icl b/frontend/overloading.icl
index 753401f..f216b8f 100644
--- a/frontend/overloading.icl
+++ b/frontend/overloading.icl
@@ -74,7 +74,7 @@ abstractTypeInDynamicError td_ident err=:{ea_ok}
 	= { err & ea_file = err.ea_file <<< (" derived abstract type '" +++ toString td_ident +++ "' not permitted in a dynamic") <<< '\n' }
 
 typeCodeInDynamicError err=:{ea_ok}
-	# err = errorHeading "Overloading error (warning for now)" err
+	# err = errorHeading "Warning" err
 	  err = {err & ea_ok=ea_ok}
 	= { err & ea_file = err.ea_file <<< "TC context not allowed in dynamic" <<< '\n' }
 
@@ -1350,7 +1350,7 @@ where
 	update_dynamic dyn_ptr (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
 		# (dyn_info, expr_heap) = readPtr dyn_ptr expr_heap 
 		= case dyn_info of
-			EI_TempDynamicType (Yes {dt_global_vars,dt_uni_vars,dt_type}) loc_dynamics _ _ expr_ptr {symb_ident}
+			EI_TempDynamicType (Yes {dt_global_vars,dt_uni_vars,dt_type,dt_contexts}) loc_dynamics _ _ _ expr_ptr {symb_ident}
 				# (expr_info, expr_heap) = readPtr expr_ptr expr_heap
 				-> case expr_info of
 					EI_TypeCodes type_codes
@@ -1371,11 +1371,12 @@ where
 						# (type_var_heap, var_heap, error)
 								= bind_type_vars_to_type_codes symb_ident dt_global_vars type_codes type_code_info.tci_type_var_heap var_heap error
 						  (uni_vars, (type_var_heap, var_heap)) = newTypeVariables dt_uni_vars (type_var_heap, var_heap)
+						  dt_type = add_types_of_dictionaries dt_contexts dt_type type_code_info.tci_common_defs
 						  (type_code_expr, (type_code_info,var_heap,error)) = toTypeCodeExpression (add_universal_vars_to_type dt_uni_vars dt_type)
 						  				({ type_code_info & tci_type_var_heap = type_var_heap }, var_heap, error)
 						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamicWithContexts type_code_expr univ_contexts)
 						-> convert_local_dynamics loc_dynamics (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
-			EI_TempDynamicType No loc_dynamics _ _ expr_ptr {symb_ident}
+			EI_TempDynamicType No loc_dynamics _ _ _ expr_ptr {symb_ident}
 				# (expr_info, expr_heap) = readPtr expr_ptr expr_heap
 				-> case expr_info of
 					EI_TypeCode type_expr
@@ -1386,7 +1387,8 @@ where
 						# (_, var_info_ptr, var_heap, error) = getClassVariable symb_ident record_var var_heap error
 						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamic (convert_selectors selectors var_info_ptr))
 						-> convert_local_dynamics loc_dynamics (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
-			EI_TempDynamicPattern type_vars {dt_global_vars,dt_uni_vars,dt_type} loc_dynamics temp_local_vars _ _ expr_ptr {symb_ident}
+			EI_TempDynamicPattern type_vars {dt_global_vars,dt_uni_vars,dt_type,dt_contexts} loc_dynamics temp_local_vars _ _ expr_ptr {symb_ident}
+				#! no_contexts = isEmpty dt_contexts
 				# (expr_info, expr_heap) = readPtr expr_ptr expr_heap
 				-> case expr_info of
 					EI_TypeCodes type_codes
@@ -1394,20 +1396,30 @@ where
 								= bind_type_vars_to_type_codes symb_ident dt_global_vars type_codes type_code_info.tci_type_var_heap var_heap error
 						  (var_ptrs, (type_pattern_vars, var_heap)) = mapSt addLocalTCInstance temp_local_vars (type_pattern_vars, var_heap)
 						  type_var_heap = bind_type_vars_to_type_var_codes type_vars var_ptrs type_var_heap
+						  dt_type = add_types_of_dictionaries dt_contexts dt_type type_code_info.tci_common_defs
 						  type_code_info = {type_code_info & tci_type_var_heap = type_var_heap}
 						  (type_code_expr, (type_code_info,var_heap,error))
 								= toTypeCodeExpression (add_universal_vars_to_type dt_uni_vars dt_type) (type_code_info, var_heap, error)
-						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamicPattern var_ptrs type_code_expr)
+						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamicPattern var_ptrs type_code_expr no_contexts)
 						-> convert_local_dynamics loc_dynamics (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
 					EI_Empty
 						# (var_ptrs, (type_pattern_vars, var_heap)) = mapSt addLocalTCInstance temp_local_vars (type_pattern_vars, var_heap)
 						  type_var_heap = bind_type_vars_to_type_var_codes type_vars var_ptrs type_code_info.tci_type_var_heap
+  						  dt_type = add_types_of_dictionaries dt_contexts dt_type type_code_info.tci_common_defs
 						  type_code_info = {type_code_info & tci_type_var_heap = type_var_heap}
 						  (type_code_expr, (type_code_info,var_heap,error))
 								= toTypeCodeExpression (add_universal_vars_to_type dt_uni_vars dt_type) (type_code_info, var_heap, error)
-						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamicPattern var_ptrs type_code_expr)
+						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamicPattern var_ptrs type_code_expr no_contexts)
 						-> convert_local_dynamics loc_dynamics (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
 	where
+		add_types_of_dictionaries [{tc_var,tc_class=TCClass {glob_module,glob_object={ds_ident,ds_index}},tc_types}:dictionaries_and_contexts] atype common_defs
+			# {class_dictionary} = common_defs.[glob_module].com_class_defs.[ds_index]
+			  dict_type_symbol = MakeTypeSymbIdent {glob_module=glob_module,glob_object=class_dictionary.ds_index} class_dictionary.ds_ident class_dictionary.ds_arity
+			  class_type = AttributedType (TA dict_type_symbol [AttributedType type \\ type <- tc_types])
+			= {at_attribute=TA_Multi, at_type=class_type --> add_types_of_dictionaries dictionaries_and_contexts atype common_defs}
+		add_types_of_dictionaries [] atype common_defs
+			= atype
+
 		bind_type_vars_to_type_codes symb_ident type_vars type_codes type_var_heap var_heap error
 			= fold2St (bind_type_var_to_type_code symb_ident) type_vars type_codes (type_var_heap, var_heap, error)
 		where
@@ -2041,10 +2053,15 @@ where
 
 instance updateExpression DynamicPattern
 where
-	updateExpression group_index dp=:{dp_type,dp_rhs} ui
-		# (dp_rhs, ui) = updateExpression group_index dp_rhs ui
-		  (EI_TypeOfDynamicPattern type_pattern_vars type_code, ui_symbol_heap) = readPtr dp_type ui.ui_symbol_heap
-		= ({dp & dp_rhs = dp_rhs, dp_type_code = type_code}, {ui & ui_symbol_heap = ui_symbol_heap})
+	updateExpression group_index dp=:{dp_var,dp_type,dp_rhs} ui
+		# (EI_TypeOfDynamicPattern type_pattern_vars type_code no_contexts, ui_symbol_heap) = readPtr dp_type ui.ui_symbol_heap
+		  ui = {ui & ui_symbol_heap = ui_symbol_heap}
+		| no_contexts
+			# (dp_rhs, ui) = updateExpression group_index dp_rhs ui
+			= ({dp & dp_rhs = dp_rhs, dp_type_code = type_code}, ui)
+			# ui = {ui & ui_var_heap = writePtr dp_var.fv_info_ptr VI_FPC ui.ui_var_heap}
+			  (dp_rhs, ui) = updateExpression group_index dp_rhs ui
+			= ({dp & dp_rhs = dp_rhs, dp_type_code = type_code}, ui)
 
 instance updateExpression (a,b) | updateExpression a & updateExpression b
 where
diff --git a/frontend/parse.icl b/frontend/parse.icl
index 6f6b138..0ad3c60 100644
--- a/frontend/parse.icl
+++ b/frontend/parse.icl
@@ -2722,17 +2722,28 @@ determAttr attr1    TA_None type pState = adjustAttribute attr1 type pState
 determAttr attr1    attr2   type pState
 	= (attr1, parseError "simple type" No ("More type attributes, "+toString attr1+" and "+toString attr2+", than") pState)
 
-wantDynamicType :: !*ParseState -> *(!DynamicType,!*ParseState)
-wantDynamicType pState 
-	# (type, pState) = want pState
-	# (type_vars, type) = split_vars_and_type type
-	= ({ dt_uni_vars = type_vars, dt_type = type, dt_global_vars = [] }, pState)
-where
-	split_vars_and_type :: AType -> ([ATypeVar], AType)
-	split_vars_and_type atype=:{at_type=TFA vars type}
-		=	(vars, {atype & at_type=type})
-	split_vars_and_type atype
-		=	([], atype)
+wantDynamicTypeInExpression :: !*ParseState -> *(!DynamicType,!*ParseState)
+wantDynamicTypeInExpression pState 
+	# (atype, pState) = want pState
+	= case atype.at_type of
+		TFA vars type
+			# atype = {atype & at_type=type}
+			  (contexts, pState) = optionalContext pState
+			-> ({dt_uni_vars=vars, dt_type=atype, dt_global_vars=[], dt_contexts=contexts}, pState)
+		_
+			-> ({dt_uni_vars=[], dt_type=atype, dt_global_vars=[], dt_contexts=[]}, pState)
+
+wantDynamicTypeInPattern :: !*ParseState -> *(!DynamicType,!*ParseState)
+wantDynamicTypeInPattern pState 
+	# (atype, pState) = want pState
+	= case atype.at_type of
+		TFA vars type
+			# atype = {atype & at_type=type}
+			  (contexts, pState) = optionalContext pState
+			-> ({dt_uni_vars=vars, dt_type=atype, dt_global_vars=[], dt_contexts=contexts}, pState)
+		_
+			 # (contexts, pState) = optionalContext pState
+			-> ({dt_uni_vars=[], dt_type=atype, dt_global_vars=[], dt_contexts=contexts}, pState)
 
 optionalExistentialQuantifiedVariables :: !*ParseState -> *(![ATypeVar],!*ParseState)
 optionalExistentialQuantifiedVariables pState
@@ -2860,7 +2871,7 @@ wantExpressionT DynamicToken pState
 	# (dyn_expr, pState) = wantExpression pState
 	  (token, pState) = nextToken FunctionContext pState
 	| token == DoubleColonToken
-		# (dyn_type, pState) = wantDynamicType pState
+		# (dyn_type, pState) = wantDynamicTypeInPattern/*wantDynamicTypeInExpression*/ pState
 		= (PE_Dynamic dyn_expr (Yes dyn_type), pState)
 		= (PE_Dynamic dyn_expr No, tokenBack pState)
 wantExpressionT token pState
@@ -2878,7 +2889,7 @@ wantPatternT token pState
 	# (exp, pState)	= wantPatternT2 token pState
 	# (token, pState)	= nextToken FunctionContext pState
 	| token == DoubleColonToken
-		# (dyn_type, pState) = wantDynamicType pState
+		# (dyn_type, pState) = wantDynamicTypeInPattern pState
 		= (PE_DynamicPattern exp dyn_type, pState)
 		= (exp, tokenBack pState)
 where
@@ -2903,7 +2914,7 @@ where
 						// not succ
 							-> (PE_Empty,  parseError "LHS expression" (Yes token) "<expression>" pState)
 			| token == DoubleColonToken
-				# (dyn_type, pState) = wantDynamicType pState
+				# (dyn_type, pState) = wantDynamicTypeInPattern pState
 				= (PE_DynamicPattern (PE_Ident id) dyn_type, pState)
 			// token <> DefinesColonToken // token back and call to wantPatternT2 would do also.
 			# (exprs, pState) = parseList trySimplePattern (tokenBack pState)
@@ -3803,7 +3814,7 @@ where
 				# list = PE_List [expr,expr2 : exprs]
 				# (token, pState)	= nextToken FunctionContext pState
 				| token == DoubleColonToken
-					# (dyn_type, pState) = wantDynamicType pState
+					# (dyn_type, pState) = wantDynamicTypeInPattern pState
 					= (True, PE_DynamicPattern list dyn_type, pState)
 					= (True, list, tokenBack pState)
 				= (True, expr, pState)
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index 1bca9d6..0f77b44 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -875,11 +875,11 @@ cNotVarNumber :== -1
 
 		/* Auxiliary, used during type checking */
 
-					| EI_TempDynamicType 		!(Optional DynamicType) ![DynamicPtr] !AType ![TypeContext] !ExprInfoPtr !SymbIdent
+					| EI_TempDynamicType 		!(Optional DynamicType) ![DynamicPtr] !AType ![TypeContext] ![TypeContext] !ExprInfoPtr !SymbIdent
 					| EI_TempDynamicPattern 	![TypeVar] !DynamicType ![DynamicPtr] ![TempLocalVar] !AType ![TypeContext] !ExprInfoPtr !SymbIdent
 
 					| EI_TypeOfDynamic 			!TypeCodeExpression						/* Final */
-					| EI_TypeOfDynamicPattern 	![VarInfoPtr] !TypeCodeExpression		/* Final */
+					| EI_TypeOfDynamicPattern 	![VarInfoPtr] !TypeCodeExpression !Bool	/* Final */
 					| EI_TypeOfDynamicWithContexts !TypeCodeExpression !(VarContexts DictionaryAndClassType)
 
 					| EI_TypeCode 		!TypeCodeExpression
@@ -1056,6 +1056,7 @@ cNotVarNumber :== -1
 	{	dt_uni_vars 	:: ![ATypeVar]
 	,	dt_global_vars	:: ![TypeVar]
 	,	dt_type			:: !AType
+	,	dt_contexts		:: ![TypeContext]
 	}
 
 ::	KindHeap	:== Heap KindInfo
diff --git a/frontend/type.icl b/frontend/type.icl
index 12317a0..c7d3ec3 100644
--- a/frontend/type.icl
+++ b/frontend/type.icl
@@ -1871,17 +1871,27 @@ where
 instance requirements DynamicExpr
 where
 	requirements ti {dyn_expr,dyn_info_ptr} (reqs, ts=:{ts_expr_heap})
-		# (EI_TempDynamicType _ _ dyn_type dyn_context dyn_expr_ptr type_code_symbol, ts_expr_heap) = readPtr dyn_info_ptr ts_expr_heap
+		# (EI_TempDynamicType _ _ dyn_type dyn_context univ_contexts dyn_expr_ptr type_code_symbol, ts_expr_heap) = readPtr dyn_info_ptr ts_expr_heap
 		  (dyn_expr_type, opt_expr_ptr, (reqs, ts)) = requirements ti dyn_expr (reqs, { ts & ts_expr_heap = ts_expr_heap })
 		  ts_expr_heap = storeAttribute opt_expr_ptr dyn_expr_type.at_attribute ts.ts_expr_heap
 		  type_coercion = { tc_demanded = dyn_type, tc_offered = dyn_expr_type, tc_position = CP_Expression dyn_expr, tc_coercible = True }
 		  atype = {at_type = TB BT_Dynamic, at_attribute = TA_Multi}
 		  type_coercions = [type_coercion : reqs.req_type_coercions]
 		| isEmpty dyn_context
-			= (atype, No, ({reqs & req_type_coercions = type_coercions}, {ts & ts_expr_heap = ts_expr_heap}))
-			# dyn_expr_info = EI_Overloaded {oc_symbol = type_code_symbol, oc_context = dyn_context, oc_specials = []}
-			= (atype, No, ({reqs & req_type_coercions = type_coercions, req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls]},
-							{ts & ts_expr_heap = ts_expr_heap <:= (dyn_expr_ptr, dyn_expr_info)}))
+			| isEmpty univ_contexts
+				= (atype, No, ({reqs & req_type_coercions = type_coercions}, {ts & ts_expr_heap = ts_expr_heap}))
+				# var_contexts = VarContext 0 univ_contexts dyn_expr_type NoVarContexts
+				# dyn_expr_info = EI_OverloadedWithVarContexts {ocvc_symbol=type_code_symbol, ocvc_context=dyn_context,	ocvc_var_contexts=var_contexts}
+				= (atype, No, ({reqs & req_type_coercions = type_coercions, req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls]},
+								{ts & ts_expr_heap = ts_expr_heap <:= (dyn_expr_ptr, dyn_expr_info)}))
+			| isEmpty univ_contexts
+				# dyn_expr_info = EI_Overloaded {oc_symbol = type_code_symbol, oc_context = dyn_context, oc_specials = []}
+				= (atype, No, ({reqs & req_type_coercions = type_coercions, req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls]},
+								{ts & ts_expr_heap = ts_expr_heap <:= (dyn_expr_ptr, dyn_expr_info)}))
+				# var_contexts = VarContext 0 univ_contexts dyn_expr_type NoVarContexts
+				# dyn_expr_info = EI_OverloadedWithVarContexts {ocvc_symbol=type_code_symbol, ocvc_context=dyn_context,	ocvc_var_contexts=var_contexts}
+				= (atype, No, ({reqs & req_type_coercions = type_coercions, req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls]},
+								{ts & ts_expr_heap = ts_expr_heap <:= (dyn_expr_ptr, dyn_expr_info)}))
 
 instance requirements Expression
 where
@@ -2313,13 +2323,14 @@ where
 		fresh_dynamic dyn_ptr (var_store, type_heaps, var_heap, expr_heap, predef_symbols)
 			# (dyn_info, expr_heap) = readPtr dyn_ptr expr_heap
 			= case dyn_info of
-				EI_Dynamic opt_dyn_type=:(Yes {dt_uni_vars,dt_type,dt_global_vars}) loc_dynamics
+				EI_Dynamic opt_dyn_type=:(Yes {dt_uni_vars,dt_type,dt_global_vars,dt_contexts}) loc_dynamics
 					# (th_vars, var_store)		= fresh_existential_attributed_variables dt_uni_vars (type_heaps.th_vars, var_store)
 					  (th_vars, var_store)		= fresh_type_variables dt_global_vars (th_vars, var_store)
 					  (tdt_type, type_heaps)	= freshCopy dt_type { type_heaps & th_vars = th_vars }
+					  (fresh_univ_contexts, (type_heaps,var_heap)) = freshTypeContexts True dt_contexts (type_heaps,var_heap)
 					  (contexts, expr_ptr, type_code_symbol, (var_heap, expr_heap, type_var_heap, predef_symbols))
 					  		= determine_context_and_expr_ptr dt_global_vars (var_heap, expr_heap, type_heaps.th_vars, predef_symbols)
-					  dyn_info = EI_TempDynamicType opt_dyn_type loc_dynamics tdt_type contexts expr_ptr type_code_symbol
+					  dyn_info = EI_TempDynamicType opt_dyn_type loc_dynamics tdt_type contexts fresh_univ_contexts expr_ptr type_code_symbol
 					-> fresh_local_dynamics loc_dynamics (var_store, { type_heaps & th_vars = type_var_heap }, var_heap,
 							expr_heap <:= (dyn_ptr, dyn_info), predef_symbols)
 				EI_Dynamic No loc_dynamics
@@ -2335,17 +2346,29 @@ where
 			 		  (new_var_ptr, var_heap) = newPtr VI_Empty var_heap
 					  context = {tc_class = TCClass tc_class_symb, tc_types = [fresh_var], tc_var = new_var_ptr}
 			  		  (expr_ptr, expr_heap) = newPtr EI_Empty expr_heap
-					  dyn_info = EI_TempDynamicType No loc_dynamics tdt_type [context] expr_ptr tc_member_symb
+			  		  dyn_info = EI_TempDynamicType No loc_dynamics tdt_type [context] [] expr_ptr tc_member_symb
 					-> fresh_local_dynamics loc_dynamics (inc var_store, type_heaps, var_heap,
 							expr_heap <:= (dyn_ptr, dyn_info), predef_symbols)
-				EI_DynamicTypeWithVars loc_type_vars dt=:{dt_uni_vars,dt_type,dt_global_vars} loc_dynamics
+				EI_DynamicTypeWithVars loc_type_vars dt=:{dt_uni_vars,dt_type,dt_global_vars,dt_contexts} loc_dynamics
 					# (fresh_vars, (th_vars, var_store)) = fresh_existential_dynamic_pattern_variables loc_type_vars (type_heaps.th_vars, var_store)
 					  (th_vars, var_store) = fresh_type_variables dt_global_vars (th_vars, var_store)
-					  (tdt_type, type_heaps) = freshCopy (add_universal_vars_to_type dt_uni_vars dt_type) {type_heaps & th_vars = th_vars}
+					  (tdt_type, type_heaps) = fresh_universal_vars_type_and_contexts dt_uni_vars dt_type dt_contexts {type_heaps & th_vars = th_vars}
 					  (contexts, expr_ptr, type_code_symbol, (var_heap, expr_heap, type_var_heap, predef_symbols))
 					  		= determine_context_and_expr_ptr dt_global_vars (var_heap, expr_heap, type_heaps.th_vars, predef_symbols)
 					  expr_heap = expr_heap <:= (dyn_ptr, EI_TempDynamicPattern loc_type_vars dt loc_dynamics fresh_vars tdt_type contexts expr_ptr type_code_symbol)
 					-> fresh_local_dynamics loc_dynamics (var_store, { type_heaps & th_vars = type_var_heap }, var_heap, expr_heap, predef_symbols)
+					where
+						fresh_universal_vars_type_and_contexts [] at [] type_heaps
+							= freshCopy at type_heaps
+						fresh_universal_vars_type_and_contexts uni_vars at=:{at_attribute,at_type} [] type_heaps
+							# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
+							  (at_type, type_heaps)			= freshCopyOfTFAType uni_vars at_type {type_heaps & th_attrs = th_attrs}
+							= ({at & at_attribute = fresh_attribute, at_type = at_type}, type_heaps)
+						fresh_universal_vars_type_and_contexts uni_vars at=:{at_attribute,at_type} contexts type_heaps
+							# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
+							  (at_type, type_heaps)			= freshCopyOfTFACType uni_vars at_type contexts {type_heaps & th_attrs = th_attrs}
+							= ({at & at_attribute = fresh_attribute, at_type = at_type}, type_heaps)
+
 				EI_UnmarkedDynamic _ _
 					-> (var_store, type_heaps, var_heap, expr_heap, predef_symbols)
 		where
@@ -2408,11 +2431,6 @@ where
 		clear_type_vars type_vars var_heap
 			= foldSt (\{tv_info_ptr} -> writePtr tv_info_ptr TVI_Empty) type_vars var_heap 
 
-	add_universal_vars_to_type [] at
-		= at
-	add_universal_vars_to_type uni_vars at=:{at_type}
-		= { at & at_type = TFA uni_vars at_type }
-
 specification_error type type1 err
 	# err = errorHeading "Type error" err
 	  format = { form_properties = cAttributed, form_attr_position = No}