add type constraints in constructors and function arguments with universal quantifier (from iTask branch)

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

28 files changed, 1283 insertions, 372 deletions

diff --git a/frontend/analunitypes.icl b/frontend/analunitypes.icl
index 2cc104f..3105520 100644
--- a/frontend/analunitypes.icl
+++ b/frontend/analunitypes.icl
@@ -315,6 +315,8 @@ signClassOfType (arg_type --> res_type) sign use_top_sign group_nr ci scs
 
 signClassOfType (TFA vars type) sign use_top_sign group_nr ci scs
 	= signClassOfType type sign use_top_sign group_nr ci scs
+signClassOfType (TFAC vars type _) sign use_top_sign group_nr ci scs
+	= signClassOfType type sign use_top_sign group_nr ci scs
 
 signClassOfType type _ _ _ _ scs
 	= (BottomSignClass, BottomSignClass, scs)
@@ -580,6 +582,8 @@ where
 
 propClassOfType (TFA vars type) group_nr ci pcs
 	= propClassOfType type group_nr ci pcs
+propClassOfType (TFAC vars type _) group_nr ci pcs
+	= propClassOfType type group_nr ci pcs
 
 propClassOfType _ _ _ pcs
 	= (NoPropClass, NoPropClass, pcs)
diff --git a/frontend/check.icl b/frontend/check.icl
index 52fafe3..9aad756 100644
--- a/frontend/check.icl
+++ b/frontend/check.icl
@@ -383,6 +383,10 @@ where
 		# (fresh_type_vars, type_heaps) = foldSt build_avar_subst type_vars ([], type_heaps)
 		  (_, new_at, type_heaps) = substitute {at & at_type = type} type_heaps
 		= ({ new_at & at_type = TFA fresh_type_vars new_at.at_type}, (was_ok, type_heaps))
+	substitue_arg_type at=:{at_type = TFAC type_vars type type_contexts} (was_ok, type_heaps)
+		# (fresh_type_vars, type_heaps) = foldSt build_avar_subst type_vars ([], type_heaps)
+		  (_, new_at, type_heaps) = substitute {at & at_type = type} type_heaps
+		= ({ new_at & at_type = TFAC fresh_type_vars new_at.at_type type_contexts}, (was_ok, type_heaps))
 	substitue_arg_type type (was_ok, type_heaps)
 		# (_, type, type_heaps) = substitute type type_heaps
 		= (type, (was_ok, type_heaps))
@@ -877,7 +881,7 @@ checkDclMacros :: !Index !Level !Index !Index !*ExpressionInfo !*Heaps !*CheckSt
 										  -> (!*ExpressionInfo,!*Heaps,!*CheckState)
 checkDclMacros mod_index level fun_index to_index e_info heaps cs
 	| fun_index == to_index
-		= ( e_info, heaps, cs)
+		= (e_info, heaps, cs)
 		# (macro_def,e_info) = e_info!ef_macro_defs.[mod_index,fun_index]
 		# (macro_def,_, e_info, heaps, cs) = checkFunction macro_def mod_index (DclMacroIndex mod_index fun_index) level 0 {} e_info heaps cs
 		# e_info = { e_info & ef_macro_defs.[mod_index,fun_index] = macro_def }
@@ -997,11 +1001,11 @@ array_plus_list a l = arrayPlusList a l
 checkCommonDefinitions :: !(Optional (CopiedDefinitions, Int)) !Index !*CommonDefs !*{# DclModule} !*Heaps !*CheckState
 												  -> (!DictionaryInfo,!*CommonDefs,!*{# DclModule},!*Heaps, !*CheckState)
 checkCommonDefinitions opt_icl_info module_index common modules heaps cs
-	# (com_type_defs, com_cons_defs, com_selector_defs, modules, heaps, cs)
+	# (com_type_defs, com_cons_defs, com_selector_defs, com_class_defs, modules, heaps, cs)
 			= checkTypeDefs module_index opt_icl_info
-					common.com_type_defs common.com_cons_defs common.com_selector_defs modules heaps cs
+					common.com_type_defs common.com_cons_defs common.com_selector_defs common.com_class_defs modules heaps cs
 	  (com_class_defs, com_member_defs, com_type_defs, modules, heaps, cs)
-	  		= checkTypeClasses module_index opt_icl_info common.com_class_defs common.com_member_defs com_type_defs modules heaps cs
+	  		= checkTypeClasses module_index opt_icl_info com_class_defs common.com_member_defs com_type_defs modules heaps cs
 	  (com_member_defs, com_type_defs, com_class_defs, modules, heaps, cs)
 	  		= checkMemberTypes module_index opt_icl_info com_member_defs com_type_defs com_class_defs modules heaps cs
 	  (com_instance_defs, com_type_defs, com_class_defs, com_member_defs, modules, heaps, cs)
diff --git a/frontend/checkFunctionBodies.icl b/frontend/checkFunctionBodies.icl
index 91f1af8..d0af688 100644
--- a/frontend/checkFunctionBodies.icl
+++ b/frontend/checkFunctionBodies.icl
@@ -1073,6 +1073,7 @@ transform_pattern (AP_Algebraic cons_symbol global_type_index args opt_var) patt
 					# glob_object = {glob_object & ds_index=pds_def,ds_ident=pds_ident}
 					= ({pattern & ap_symbol.glob_object=glob_object},cs)
 					= abort "replace_overloaded_symbol_in_pattern"
+
 transform_pattern (AP_Basic basic_val opt_var) patterns pattern_scheme pattern_variables defaul result_expr _ pos var_store expr_heap opt_dynamics cs
 	# pattern = { bp_value = basic_val, bp_expr = result_expr, bp_position = pos}
 	  pattern_variables = cons_optional opt_var pattern_variables
@@ -1309,6 +1310,10 @@ where
 				SK_Constructor _
 					# app_expr = App {app_symb = symbol, app_args = [], app_info_ptr = nilPtr}
 					-> (app_expr, free_vars, e_state, e_info, cs)
+				SK_OverloadedConstructor cons_index
+					# (new_info_ptr, es_expr_heap) = newPtr EI_Empty e_state.es_expr_heap
+					  app_expr = App {app_symb = {symbol & symb_kind=SK_Constructor cons_index}, app_args = [], app_info_ptr = new_info_ptr}
+					-> (app_expr, free_vars, {e_state & es_expr_heap = es_expr_heap}, e_info, cs)
 				SK_NewTypeConstructor _
 					# cs = { cs & cs_error = checkError id "argument missing (for newtype constructor)" cs.cs_error}
 					# app_expr = App { app_symb = symbol , app_args = [], app_info_ptr = nilPtr }
@@ -1372,18 +1377,22 @@ where
 			# {me_type={st_arity},me_priority} = com_member_defs.[def_index]
 			= (SK_OverloadedFunction { glob_object = def_index, glob_module = mod_index }, st_arity, me_priority)
 		ste_kind_to_symbol_kind STE_Constructor def_index mod_index {dcl_common={com_cons_defs}}
-			# {cons_type={st_arity},cons_priority,cons_number} = com_cons_defs.[def_index]
+			# {cons_type={st_arity,st_args,st_context},cons_priority,cons_number} = com_cons_defs.[def_index]
 			| cons_number <> -2
-				= (SK_Constructor {glob_object = def_index, glob_module = mod_index}, st_arity, cons_priority)
+				| isEmpty st_context && no_TFAC_argument st_args
+					= (SK_Constructor {glob_object = def_index, glob_module = mod_index}, st_arity, cons_priority)
+					= (SK_OverloadedConstructor {glob_object = def_index, glob_module = mod_index}, st_arity, cons_priority)
 				= (SK_NewTypeConstructor {gi_index = def_index, gi_module = mod_index}, st_arity, cons_priority)
 	determine_info_of_symbol {ste_kind=STE_Member, ste_index} _ e_input=:{ei_mod_index} e_state e_info=:{ef_member_defs} cs
 		# ({me_type={st_arity},me_priority}, ef_member_defs) = ef_member_defs![ste_index]
 		= (SK_OverloadedFunction { glob_object = ste_index, glob_module = ei_mod_index}, st_arity, me_priority,
 				e_state, { e_info & ef_member_defs = ef_member_defs }, cs)
 	determine_info_of_symbol {ste_kind=STE_Constructor, ste_index} _ e_input=:{ei_mod_index} e_state e_info cs
-		# ({cons_type={st_arity},cons_priority,cons_number}, e_info) = e_info!ef_cons_defs.[ste_index]
+		# ({cons_type={st_arity,st_args,st_context},cons_priority,cons_number}, e_info) = e_info!ef_cons_defs.[ste_index]
 		| cons_number <> -2
-			= (SK_Constructor {glob_object = ste_index, glob_module =  ei_mod_index}, st_arity, cons_priority, e_state, e_info, cs)
+			| isEmpty st_context && no_TFAC_argument st_args
+				= (SK_Constructor {glob_object = ste_index, glob_module = ei_mod_index}, st_arity, cons_priority, e_state, e_info, cs)
+				= (SK_OverloadedConstructor {glob_object = ste_index, glob_module = ei_mod_index}, st_arity, cons_priority, e_state, e_info, cs)
 			= (SK_NewTypeConstructor {gi_index = ste_index, gi_module = ei_mod_index}, st_arity, cons_priority, e_state, e_info, cs)
 	determine_info_of_symbol {ste_kind=STE_DclFunction, ste_index} _ e_input=:{ei_mod_index} e_state=:{es_calls} e_info=:{ef_is_macro_fun} cs
 		# ({ft_type={st_arity},ft_priority}, e_info) = e_info!ef_modules.[ei_mod_index].dcl_functions.[ste_index]
@@ -1402,6 +1411,10 @@ where
 			= SK_LocalMacroFunction index.glob_object
 			= SK_Function index
 
+	no_TFAC_argument [{at_type=TFAC _ _ _}:_] = False
+	no_TFAC_argument [_:args] = no_TFAC_argument args
+	no_TFAC_argument [] = True
+
 checkQualifiedIdentExpression free_vars module_id ident_name is_expr_list e_input=:{ei_fun_index,ei_mod_index} e_state e_info cs
 	# (found,{decl_kind,decl_ident,decl_index},cs) = search_qualified_ident module_id ident_name ExpressionNameSpaceN cs
 	| not found
@@ -1417,12 +1430,15 @@ checkQualifiedIdentExpression free_vars module_id ident_name is_expr_list e_inpu
 					# e_state = { e_state & es_calls = [DclFunCall mod_index decl_index : e_state.es_calls ]}
 					-> (app_expr, free_vars, e_state, e_info, cs)
 			STE_Imported STE_Constructor mod_index
-				# ({cons_type={st_arity},cons_priority,cons_number}, e_info) = e_info!ef_modules.[mod_index].dcl_common.com_cons_defs.[decl_index]
+				# ({cons_type={st_arity,st_context},cons_priority,cons_number}, e_info) = e_info!ef_modules.[mod_index].dcl_common.com_cons_defs.[decl_index]
 				| cons_number <> -2
 					# kind = SK_Constructor { glob_object = decl_index, glob_module = mod_index }
 					  symbol = { symb_ident = decl_ident, symb_kind = kind }
-					# app_expr = build_application_or_constant_for_constructor symbol st_arity cons_priority
-					-> (app_expr, free_vars, e_state, e_info, cs)
+					| isEmpty st_context
+						# (app_expr,e_state) = build_application_or_constant_for_function symbol st_arity cons_priority e_state
+						-> (app_expr, free_vars, e_state, e_info, cs)
+						# app_expr = build_application_or_constant_for_constructor symbol st_arity cons_priority
+						-> (app_expr, free_vars, e_state, e_info, cs)
 					# kind = SK_NewTypeConstructor { gi_index = decl_index, gi_module = mod_index }
 					# symbol = { symb_ident = decl_ident, symb_kind = kind }
 					# app_expr = build_application_or_constant_for_constructor symbol st_arity cons_priority
@@ -2663,6 +2679,13 @@ buildApplication symbol=:{symb_kind=SK_Constructor _} form_arity act_arity args
 	| act_arity > form_arity
 		= (app, e_state, checkError symbol.symb_ident "used with too many arguments" error)
 		= (app, e_state, error)
+buildApplication symbol=:{symb_kind=SK_OverloadedConstructor cons_index} form_arity act_arity args e_state error
+	# (new_info_ptr, es_expr_heap) = newPtr EI_Empty e_state.es_expr_heap
+	  e_state = {e_state & es_expr_heap=es_expr_heap}
+	  app = App {app_symb = {symbol & symb_kind=SK_Constructor cons_index}, app_args = args, app_info_ptr = new_info_ptr}
+	| act_arity > form_arity
+		= (app, e_state, checkError symbol.symb_ident "used with too many arguments" error)
+		= (app, e_state, error)
 buildApplication symbol=:{symb_kind=SK_NewTypeConstructor _} form_arity act_arity args e_state error
 	# app = App { app_symb = symbol , app_args = args, app_info_ptr = nilPtr }
 	| act_arity == form_arity
@@ -2682,6 +2705,10 @@ buildApplicationWithoutArguments :: !SymbIdent !*ExpressionState !*ErrorAdmin ->
 buildApplicationWithoutArguments symbol=:{symb_kind=SK_Constructor _} e_state error
 	# app = App { app_symb = symbol , app_args = [], app_info_ptr = nilPtr }
 	= (app, e_state, error)
+buildApplicationWithoutArguments symbol=:{symb_kind=SK_OverloadedConstructor cons_index} e_state error
+	# (new_info_ptr, es_expr_heap) = newPtr EI_Empty e_state.es_expr_heap
+	  app = App {app_symb = {symbol & symb_kind=SK_Constructor cons_index}, app_args = [], app_info_ptr = new_info_ptr}
+	= (app, {e_state & es_expr_heap = es_expr_heap}, error)
 buildApplicationWithoutArguments symbol=:{symb_kind=SK_NewTypeConstructor _} e_state error
 	# app = App { app_symb = symbol , app_args = [], app_info_ptr = nilPtr }
 	= (app, e_state, checkError symbol.symb_ident "argument missing (for newtype constructor)" error)
diff --git a/frontend/checktypes.dcl b/frontend/checktypes.dcl
index bb7f26c..1cc34b4 100644
--- a/frontend/checktypes.dcl
+++ b/frontend/checktypes.dcl
@@ -3,8 +3,8 @@ definition module checktypes
 import checksupport
 
 checkTypeDefs :: !Index !(Optional (CopiedDefinitions, Int))
-		!*{#CheckedTypeDef} !*{#ConsDef} !*{#SelectorDef} !*{#DclModule} !*Heaps !*CheckState
-	-> (!*{#CheckedTypeDef},!*{#ConsDef},!*{#SelectorDef},!*{#DclModule},!*Heaps,!*CheckState)
+		!*{#CheckedTypeDef} !*{#ConsDef} !*{#SelectorDef} !v:{#ClassDef} !*{#DclModule} !*Heaps !*CheckState
+	-> (!*{#CheckedTypeDef},!*{#ConsDef},!*{#SelectorDef},!v:{#ClassDef},!*{#DclModule},!*Heaps,!*CheckState)
 
 checkFunctionType :: !Index !SymbolType !FunSpecials !u:{#CheckedTypeDef} !v:{#ClassDef} !u:{#DclModule} !*TypeHeaps !*CheckState
 						-> (!SymbolType,!FunSpecials,!u:{#CheckedTypeDef},!v:{#ClassDef},!u:{#DclModule},!*TypeHeaps,!*CheckState)
diff --git a/frontend/checktypes.icl b/frontend/checktypes.icl
index 8179002..722e060 100644
--- a/frontend/checktypes.icl
+++ b/frontend/checktypes.icl
@@ -24,17 +24,69 @@ from explicitimports import search_qualified_ident,::NameSpaceN,TypeNameSpaceN,C
 	,	cti_lhs_attribute	:: !TypeAttribute
 	}
 
-bindArgAType :: !CurrentTypeInfo !AType !(!*TypeSymbols, !*TypeInfo, !*CheckState)
-			-> (!AType, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
-bindArgAType cti {at_attribute,at_type=TFA vars type} (ts, ti=:{ti_type_heaps}, cs)
+bindArgAType :: !CurrentTypeInfo !AType !v:{#ClassDef}  !(!*TypeSymbols, !*TypeInfo, !*CheckState)
+			-> (!AType, !TypeAttribute, !v:{#ClassDef}, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
+bindArgAType cti {at_attribute,at_type=TFA vars type} class_defs (ts, ti=:{ti_type_heaps}, cs)
 	# (type_vars, (_, ti_type_heaps, cs)) = addTypeVariablesToSymbolTable cRankTwoScope vars [] ti_type_heaps cs
 	  (type, _, (ts, ti, cs)) = bindTypes cti type (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
 	  cs & cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
 	  at_type = TFA type_vars type
-	= bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
-bindArgAType cti {at_attribute,at_type} ts_ti_cs
+	  (attype,combined_attribute,ts_ti_cs) = bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
+	= (attype,combined_attribute,class_defs,ts_ti_cs)
+bindArgAType cti {at_attribute,at_type=TFAC vars type contexts} class_defs (ts, ti=:{ti_type_heaps}, cs)
+	# (type_vars, (_, ti_type_heaps, cs)) = addTypeVariablesToSymbolTable cRankTwoScope vars [] ti_type_heaps cs
+	  (type, _, (ts, ti, cs)) = bindTypes cti type (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
+	  (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
+	  cs & cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
+	  at_type = TFAC type_vars type contexts
+	  (attype,combined_attribute,ts_ti_cs) = bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
+	= (attype,combined_attribute,class_defs,ts_ti_cs)
+bindArgAType cti {at_attribute,at_type} class_defs ts_ti_cs
 	# (at_type, type_attr, ts_ti_cs) = bindTypes cti at_type ts_ti_cs
-	= bindAttributes type_attr cti at_attribute at_type ts_ti_cs
+	  (attype,combined_attribute,ts_ti_cs) = bindAttributes type_attr cti at_attribute at_type ts_ti_cs
+	= (attype,combined_attribute,class_defs,ts_ti_cs)
+
+bind_rank2_context_of_cons [context=:{tc_class,tc_types}:contexts] cti class_defs ts ti cs
+	# (tc_class, class_defs, modules, cs=:{cs_error}) = check_context_class tc_class tc_types cti.cti_module_index class_defs ts.ts_modules cs
+	  ts = {ts & ts_modules=modules}
+	| cs_error.ea_ok
+	 	# (tc_types, _, (ts,ti,cs)) = bindTypes cti tc_types (ts,ti,cs)
+		  cs = check_context_types tc_class tc_types cs
+		  (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
+		#! contexts = [{context & tc_class=tc_class, tc_types=tc_types}:contexts]
+		| cs_error.ea_ok
+			# cs = foldSt check_rank2_vars_in_type tc_types cs
+			= (contexts,class_defs,ts,ti,cs)
+			= (contexts,class_defs,ts,ti,cs)
+		# (contexts,class_defs,ts,ti,cs) = bind_rank2_context_of_cons contexts cti class_defs ts ti cs
+		= ([{context & tc_types = []}:contexts],class_defs,ts,ti,cs)
+where
+	check_rank2_vars_in_atypes [{at_type}:tc_types] cs
+		= check_rank2_vars_in_atypes tc_types (check_rank2_vars_in_type at_type cs)
+	check_rank2_vars_in_atypes [] cs
+		= cs
+	
+	check_rank2_vars_in_type (TV {tv_ident}) cs=:{cs_symbol_table}
+		| (sreadPtr tv_ident.id_info cs_symbol_table).ste_def_level==cRankTwoScope
+			= cs
+			= {cs & cs_error = checkError tv_ident "universally quantified type variable expected" cs.cs_error}
+	check_rank2_vars_in_type (TA _ atypes) cs
+		= check_rank2_vars_in_atypes atypes cs
+	check_rank2_vars_in_type (TAS _ atypes _) cs
+		= check_rank2_vars_in_atypes atypes cs
+	check_rank2_vars_in_type (arg_type --> res_type) cs
+		= check_rank2_vars_in_type res_type.at_type (check_rank2_vars_in_type arg_type.at_type cs)
+	check_rank2_vars_in_type (TArrow1 {at_type}) cs
+		= check_rank2_vars_in_type at_type cs
+	check_rank2_vars_in_type (CV {tv_ident} :@: types) cs=:{cs_symbol_table}
+		| (sreadPtr tv_ident.id_info cs_symbol_table).ste_def_level==cRankTwoScope
+			= check_rank2_vars_in_atypes types cs
+			# cs & cs_error = checkError tv_ident "universally quantified type variable expected" cs.cs_error
+			= check_rank2_vars_in_atypes types cs
+	check_rank2_vars_in_type _ cs
+		= cs
+bind_rank2_context_of_cons [] cti class_defs ts ti cs
+	= ([],class_defs,ts,ti,cs)
 
 class bindTypes type :: !CurrentTypeInfo !type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
 					-> (!type, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
@@ -199,11 +251,6 @@ where
 		# (tv, type_attr, ts_ti_cs) = bindTypes cti tv ts_ti_cs
 		  (types, _, ts_ti_cs) = bindTypes cti types ts_ti_cs
 		= (CV tv :@: types, type_attr, ts_ti_cs)
-	bindTypes cti (TFA vars type) (ts, ti=:{ti_type_heaps}, cs)
-		# (type_vars, (_, ti_type_heaps, cs)) = addTypeVariablesToSymbolTable cRankTwoScope vars [] ti_type_heaps cs
-		  (type, _, (ts, ti, cs)) = bindTypes cti type (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
-		  cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
-		= (TFA type_vars type, TA_Multi, (ts, ti, {cs & cs_symbol_table = cs_symbol_table}))
 	bindTypes cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} type=:(TQualifiedIdent module_id type_name types)
 					(ts=:{ts_type_defs,ts_modules}, ti, cs)
 		# (found,{decl_kind,decl_ident=type_ident,decl_index=type_index},cs) = search_qualified_ident module_id type_name TypeNameSpaceN cs
@@ -325,7 +372,11 @@ check_context_class (TCGeneric gtc=:{gtc_generic, gtc_kind}) tc_types mod_index
 				}
 			  ({pds_module,pds_def},cs) = cs!cs_predef_symbols.[PD_TypeGenericDict]
 			  generic_dict = {gi_module=pds_module, gi_index=pds_def}
-			= (TCGeneric {gtc & gtc_generic = checked_gen, gtc_class=clazz, gtc_generic_dict=generic_dict}, class_defs, modules, cs)
+			#! tc_class = TCGeneric {gtc & gtc_generic = checked_gen, gtc_class=clazz, gtc_generic_dict=generic_dict}
+			| not cs.cs_x.x_check_dynamic_types
+				= (tc_class, class_defs, modules, cs)
+				# cs = {cs & cs_error = checkError gen_ident "a generic context is not allowed in a dynamic type" cs.cs_error}
+				= (tc_class, class_defs, modules, cs)
 			# cs_error = checkError gen_ident "generic used with wrong arity: generic has always has one class argument" cs.cs_error  
 			= (TCGeneric {gtc & gtc_class=clazz}, class_defs, modules, {cs & cs_error = cs_error})
 		# cs_error = checkError gen_ident "generic undefined" cs.cs_error
@@ -343,8 +394,8 @@ check_context_types tc_class [type : types] cs
 
 emptyIdent name :== { id_name = name, id_info = nilPtr }
 
-checkTypeDef :: !Index !Index !*TypeSymbols !*TypeInfo !*CheckState -> (!*TypeSymbols, !*TypeInfo, !*CheckState);
-checkTypeDef type_index module_index ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:{cs_error}
+checkTypeDef :: !Index !Index !v:{#ClassDef} !*TypeSymbols !*TypeInfo !*CheckState -> (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState);
+checkTypeDef type_index module_index class_defs ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:{cs_error}
 	# (type_def, ts_type_defs) = ts_type_defs![type_index]
 	# {td_ident,td_pos,td_args,td_attribute,td_index} = type_def
 	| td_index == NoIndex
@@ -354,14 +405,14 @@ checkTypeDef type_index module_index ts=:{ts_type_defs} ti=:{ti_type_heaps} cs=:
 		  (type_vars, (attr_vars, ti_type_heaps, cs))
 		  		= addTypeVariablesToSymbolTable cGlobalScope td_args attr_vars { ti_type_heaps & th_attrs = th_attrs } { cs & cs_error = cs_error }
 		  type_def = { type_def & td_args = type_vars, td_index = type_index, td_attrs = attr_vars, td_attribute = td_attribute }
-		  (td_rhs, (ts,ti,cs)) = check_rhs_of_TypeDef type_def attr_vars
+		  (td_rhs, (class_defs,ts,ti,cs)) = check_rhs_of_TypeDef type_def attr_vars
 				{ cti_module_index = module_index, cti_type_index = type_index, cti_lhs_attribute = td_attribute }
-					({ts & ts_type_defs = ts_type_defs}, {ti & ti_type_heaps = ti_type_heaps}, cs)
+					(class_defs, {ts & ts_type_defs = ts_type_defs}, {ti & ti_type_heaps = ti_type_heaps}, cs)
 		  (td_used_types, cs_symbol_table) = retrieve_used_types ti.ti_used_types cs.cs_symbol_table
 		  cs = {cs &	cs_error = popErrorAdmin cs.cs_error,
 						cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope type_vars cs_symbol_table}
-		= ({ts & ts_type_defs = {ts.ts_type_defs & [type_index] = {type_def & td_rhs = td_rhs, td_used_types = td_used_types}}}, {ti & ti_used_types = []}, cs)
-		= ({ts & ts_type_defs = ts_type_defs}, ti, cs)
+		= (class_defs, {ts & ts_type_defs = {ts.ts_type_defs & [type_index] = {type_def & td_rhs = td_rhs, td_used_types = td_used_types}}}, {ti & ti_used_types = []},cs)
+		= (class_defs, {ts & ts_type_defs = ts_type_defs}, ti, cs)
 where
 	determine_root_attribute TA_None name attr_var_heap
 		# (attr_info_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
@@ -370,28 +421,29 @@ where
 	determine_root_attribute TA_Unique name attr_var_heap
 		= (TA_Unique, [], attr_var_heap)
 
-	check_rhs_of_TypeDef :: !CheckedTypeDef ![AttributeVar] !CurrentTypeInfo !(!*TypeSymbols, !*TypeInfo, !*CheckState)
-		-> (!TypeRhs, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
-	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:AlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} ts_ti_cs
+	check_rhs_of_TypeDef :: !CheckedTypeDef ![AttributeVar] !CurrentTypeInfo
+					  !(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+		-> (!TypeRhs, !(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState))
+	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:AlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
 		# type_lhs = { at_attribute = cti_lhs_attribute,
 				  	   at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
 									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
-		  ts_ti_cs = bind_types_of_constructors cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs conses ts_ti_cs
-		= (td_rhs, ts_ti_cs)
+		  class_defs_ts_ti_cs = bind_types_of_constructors cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
+		= (td_rhs, class_defs_ts_ti_cs)
 	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:RecordType {rt_constructor={ds_index,ds_arity}, rt_fields}}
-			attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} (ts,ti,cs)
+			attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} (class_defs,ts,ti,cs)
 		# type_lhs = {	at_attribute = cti_lhs_attribute,
 						at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
 									[{ at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
 		  cs = if (ds_arity>32)
 				{ cs & cs_error = checkError ("Record has too many fields ("+++toString ds_arity+++",") "32 are allowed)" cs.cs_error }
 				cs;
-		  (ts, ti, cs) = bind_types_of_constructor cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs ds_index (ts,ti,cs)
+		  (class_defs,ts,ti,cs) = bind_types_of_constructor cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs ds_index (class_defs,ts,ti,cs)
 		# (rec_cons_def, ts) = ts!ts_cons_defs.[ds_index]
 		# {cons_type = { st_vars,st_args,st_result,st_attr_vars }, cons_exi_vars} = rec_cons_def
 		# (ts_selector_defs, ti_var_heap, cs_error) = check_selectors 0 rt_fields cti_type_index st_args st_result st_vars st_attr_vars cons_exi_vars
 					ts.ts_selector_defs ti.ti_var_heap cs.cs_error
-		= (td_rhs, ({ts & ts_selector_defs = ts_selector_defs}, {ti & ti_var_heap = ti_var_heap}, {cs & cs_error = cs_error}))
+		= (td_rhs, (class_defs,{ts & ts_selector_defs = ts_selector_defs},{ti & ti_var_heap = ti_var_heap},{cs & cs_error = cs_error}))
 	where
 		check_selectors :: !Index !{# FieldSymbol} !Index ![AType] !AType ![TypeVar] ![AttributeVar] ![ATypeVar] !*{#SelectorDef} !*VarHeap !*ErrorAdmin
 			-> (!*{#SelectorDef}, !*VarHeap, !*ErrorAdmin)
@@ -422,64 +474,65 @@ where
 				= [av : attr_vars]
 			add_attr_var attr attr_vars
 				= attr_vars
-	check_rhs_of_TypeDef {td_rhs = SynType type} _ cti ts_ti_cs
-		# (type, type_attr, ts_ti_cs) = bindTypes cti type ts_ti_cs
-		= (SynType type, ts_ti_cs)
-	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:NewType cons} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} ts_ti_cs
+	check_rhs_of_TypeDef {td_rhs = SynType type} _ cti (class_defs,ts,ti,cs)
+		# (type, type_attr, (ts,ti,cs)) = bindTypes cti type (ts,ti,cs)
+		= (SynType type, (class_defs,ts,ti,cs))
+	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:NewType {ds_index}} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
 		# type_lhs = { at_attribute = cti_lhs_attribute,
 				  	   at_type = TA (MakeTypeSymbIdent { glob_object = cti_type_index, glob_module = cti_module_index } td_ident td_arity)
 									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
-		  ts_ti_cs = bind_types_of_constructor cti -2 (atype_vars_to_type_vars td_args) attr_vars type_lhs cons.ds_index ts_ti_cs
-		= (td_rhs, ts_ti_cs)
-	check_rhs_of_TypeDef {td_rhs = AbstractSynType properties type} _ cti ts_ti_cs
-		# (type, type_attr, ts_ti_cs) = bindTypes cti type ts_ti_cs
-		= (AbstractSynType properties type, ts_ti_cs)
+		  class_defs_ts_ti_cs = bind_types_of_constructor cti -2 (atype_vars_to_type_vars td_args) attr_vars type_lhs ds_index class_defs_ts_ti_cs
+		= (td_rhs, class_defs_ts_ti_cs)
+	check_rhs_of_TypeDef {td_rhs = AbstractSynType properties type} _ cti (class_defs,ts,ti,cs)
+		# (type, type_attr, (ts,ti,cs)) = bindTypes cti type (ts,ti,cs)
+		= (AbstractSynType properties type, (class_defs,ts,ti,cs))
 	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:ExtensibleAlgType conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
 		# type_lhs = { at_attribute = cti_lhs_attribute,
 				  	   at_type = TA (MakeTypeSymbIdent {glob_object = cti_type_index, glob_module = cti_module_index} td_ident td_arity)
 									[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
 		  class_defs_ts_ti_cs = bind_types_of_constructors cti 0 (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
 		= (td_rhs, class_defs_ts_ti_cs)
-	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:UncheckedAlgConses type_ext_ident conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} ts_ti_cs
-		# (ts,ti,cs) = ts_ti_cs
+	check_rhs_of_TypeDef {td_ident,td_arity,td_args,td_rhs = td_rhs=:UncheckedAlgConses type_ext_ident conses} attr_vars cti=:{cti_module_index,cti_type_index,cti_lhs_attribute} class_defs_ts_ti_cs
+		# (class_defs,ts,ti,cs) = class_defs_ts_ti_cs
 		  (type_index, type_module, cs_symbol_table, ti_used_types) = retrieveTypeDefinition td_ident.id_info cti_module_index cs.cs_symbol_table ti.ti_used_types
 		  ti & ti_used_types = ti_used_types
 		  cs & cs_symbol_table = cs_symbol_table
 		| type_index <> NotFound
-		 	# ts_ti_cs = (ts,ti,cs)
+		 	# class_defs_ts_ti_cs = (class_defs,ts,ti,cs)
 			// to do check if ExtensibleAlgType
 			# type_lhs = { at_attribute = cti_lhs_attribute,
 					  	   at_type = TA (MakeTypeSymbIdent { glob_object = type_index, glob_module = type_module } td_ident td_arity)
 										[{at_attribute = atv_attribute,at_type = TV atv_variable} \\ {atv_variable, atv_attribute} <- td_args]}
-			  ts_ti_cs = bind_types_of_added_constructors cti (atype_vars_to_type_vars td_args) attr_vars type_lhs conses ts_ti_cs
-			= (AlgConses conses {gi_module=type_module,gi_index=type_index}, ts_ti_cs)
+			  class_defs_ts_ti_cs = bind_types_of_added_constructors cti (atype_vars_to_type_vars td_args) attr_vars type_lhs conses class_defs_ts_ti_cs
+			= (AlgConses conses {gi_module=type_module,gi_index=type_index}, class_defs_ts_ti_cs)
 			# cs & cs_error = checkError td_ident "undefined" cs.cs_error
-			= (td_rhs, (ts,ti,cs))
-	check_rhs_of_TypeDef {td_rhs} _ _ ts_ti_cs
-		= (td_rhs, ts_ti_cs)
+			= (td_rhs, (class_defs,ts,ti,cs))
+	check_rhs_of_TypeDef {td_rhs} _ _ class_defs_ts_ti_cs
+		= (td_rhs, class_defs_ts_ti_cs)
 
 	atype_vars_to_type_vars atype_vars
 		= [atv_variable \\ {atv_variable} <- atype_vars]
 
-	bind_types_of_constructors :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol] !(!*TypeSymbols,!*TypeInfo,!*CheckState)
-							-> (!*TypeSymbols, !*TypeInfo, !*CheckState)
-	bind_types_of_constructors cti cons_index free_vars free_attrs type_lhs [cons=:{ds_arity,ds_ident,ds_index}:conses] (ts,ti,cs)
+	bind_types_of_constructors :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol]
+								!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+							->   (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+	bind_types_of_constructors cti cons_number free_vars free_attrs type_lhs [{ds_arity,ds_ident,ds_index}:conses] (class_defs,ts,ti,cs)
 		# (ts,cs) = if (ds_arity>32)
 						(constructor_has_too_many_arguments ds_index ds_ident ds_arity ts cs)
 						(ts,cs);
-		# ts_ti_cs = bind_types_of_constructor cti cons_index free_vars free_attrs type_lhs ds_index (ts,ti,cs)
-		= bind_types_of_constructors cti (inc cons_index) free_vars free_attrs type_lhs conses ts_ti_cs
-	bind_types_of_constructors _ _ _ _ _ [] ts_ti_cs
-		= ts_ti_cs
+		# class_defs_ts_ti_cs = bind_types_of_constructor cti cons_number free_vars free_attrs type_lhs ds_index (class_defs,ts,ti,cs)
+		= bind_types_of_constructors cti (inc cons_number) free_vars free_attrs type_lhs conses class_defs_ts_ti_cs
+	bind_types_of_constructors _ _ _ _ _ [] class_defs_ts_ti_cs
+		= class_defs_ts_ti_cs
 
 	bind_types_of_added_constructors :: !CurrentTypeInfo ![TypeVar] ![AttributeVar] !AType ![DefinedSymbol]
-								!(!*TypeSymbols,!*TypeInfo,!*CheckState)
-							->   (!*TypeSymbols,!*TypeInfo,!*CheckState)
-	bind_types_of_added_constructors cti free_vars free_attrs type_lhs [{ds_arity,ds_ident,ds_index}:conses] (ts,ti,cs)
+								!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+							->   (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+	bind_types_of_added_constructors cti free_vars free_attrs type_lhs [{ds_arity,ds_ident,ds_index}:conses] (class_defs,ts,ti,cs)
 		# (ts,cs) = if (ds_arity>32)
 						(constructor_has_too_many_arguments ds_index ds_ident ds_arity ts cs)
 						(ts,cs);
-		# class_defs_ts_ti_cs = bind_types_of_constructor cti -3 free_vars free_attrs type_lhs ds_index (ts,ti,cs)
+		# class_defs_ts_ti_cs = bind_types_of_constructor cti -3 free_vars free_attrs type_lhs ds_index (class_defs,ts,ti,cs)
 		= bind_types_of_added_constructors cti free_vars free_attrs type_lhs conses class_defs_ts_ti_cs
 	bind_types_of_added_constructors _ _ _ _ [] class_defs_ts_ti_cs
 		= class_defs_ts_ti_cs
@@ -488,37 +541,55 @@ where
 		# (cons_pos,ts2) = ts!ts_cons_defs.[ds_index].cons_pos
 		= (ts2, {cs & cs_error = checkErrorWithPosition ds_ident cons_pos ("Constructor has too many arguments ("+++toString ds_arity+++", 32 are allowed)") cs.cs_error})
 
-	bind_types_of_constructor :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType !Index !(!*TypeSymbols,!*TypeInfo,!*CheckState)
-								-> (!*TypeSymbols, !*TypeInfo, !*CheckState)
-	bind_types_of_constructor cti=:{cti_lhs_attribute} cons_number free_vars free_attrs type_lhs cons_index (ts, ti=:{ti_type_heaps}, cs)
+	bind_types_of_constructor :: !CurrentTypeInfo !Index ![TypeVar] ![AttributeVar] !AType !Index
+					!(!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+				->	 (!v:{#ClassDef},!*TypeSymbols,!*TypeInfo,!*CheckState)
+	bind_types_of_constructor cti=:{cti_lhs_attribute} cons_number free_vars free_attrs type_lhs cons_index (class_defs, ts, ti=:{ti_type_heaps}, cs)
 		# (cons_def, ts) = ts!ts_cons_defs.[cons_index]
 		# (exi_vars, (ti_type_heaps, cs))
 		  		= addExistentionalTypeVariablesToSymbolTable cti_lhs_attribute cons_def.cons_exi_vars ti_type_heaps cs
-		  (st_args, st_attr_env, (ts, ti, cs))
-		  		= bind_types_of_cons cons_def.cons_type.st_args cti free_vars [] (ts, { ti & ti_type_heaps = ti_type_heaps }, cs)
+		  (st_args, st_attr_env,class_defs,(ts, ti, cs))
+		  		= bind_types_of_cons cons_def.cons_type.st_args cti free_vars [] class_defs (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
+		  (st_context,class_defs,ts,ti,cs)
+		  		= bind_context_of_cons cons_def.cons_type.st_context cti class_defs ts ti cs
 		  symbol_table = removeAttributedTypeVarsFromSymbolTable cGlobalScope /* cOuterMostLevel */ exi_vars cs.cs_symbol_table
 		  attr_vars = add_universal_attr_vars st_args free_attrs
-		  cons_type = {cons_def.cons_type & st_vars = free_vars, st_args = st_args, st_result = type_lhs, st_attr_vars = attr_vars, st_attr_env = st_attr_env}
+		  cons_type = {cons_def.cons_type & st_vars = free_vars, st_args = st_args, st_result = type_lhs, st_context = st_context, st_attr_vars = attr_vars, st_attr_env = st_attr_env}
 		  (new_type_ptr, ti_var_heap) = newPtr VI_Empty ti.ti_var_heap
 		  cons_def = { cons_def & cons_type = cons_type, cons_number = cons_number, cons_type_index = cti.cti_type_index, cons_exi_vars = exi_vars,
 		  						  cons_type_ptr = new_type_ptr }
-		= ({ts & ts_cons_defs.[cons_index] = cons_def}, { ti & ti_var_heap = ti_var_heap }, { cs & cs_symbol_table=symbol_table})
+		= (class_defs, {ts & ts_cons_defs.[cons_index] = cons_def}, {ti & ti_var_heap = ti_var_heap}, {cs & cs_symbol_table=symbol_table})
 	where
-		bind_types_of_cons :: ![AType] !CurrentTypeInfo ![TypeVar] ![AttrInequality] !(!*TypeSymbols, !*TypeInfo, !*CheckState)
-									  -> (![AType], ![AttrInequality],!(!*TypeSymbols, !*TypeInfo, !*CheckState))
-		bind_types_of_cons [] cti free_vars attr_env ts_ti_cs
-			= ([], attr_env, ts_ti_cs)
-		bind_types_of_cons [type : types] cti free_vars attr_env ts_ti_cs
-			# (types, attr_env, ts_ti_cs)
-					= bind_types_of_cons types cti free_vars attr_env ts_ti_cs
-			  (type, type_attr, (ts, ti, cs)) = bindArgAType cti type ts_ti_cs
+		bind_types_of_cons :: ![AType] !CurrentTypeInfo ![TypeVar] ![AttrInequality] !v:{#ClassDef} !(!*TypeSymbols, !*TypeInfo, !*CheckState)
+													 -> (![AType], ![AttrInequality],!v:{#ClassDef},!(!*TypeSymbols, !*TypeInfo, !*CheckState))
+		bind_types_of_cons [] cti free_vars attr_env class_defs ts_ti_cs
+			= ([], attr_env, class_defs, ts_ti_cs)
+		bind_types_of_cons [type : types] cti free_vars attr_env class_defs ts_ti_cs
+			# (types, attr_env, class_defs, ts_ti_cs)
+					= bind_types_of_cons types cti free_vars attr_env class_defs ts_ti_cs
+			  (type, type_attr, class_defs, (ts, ti, cs)) = bindArgAType cti type class_defs ts_ti_cs
 			  (attr_env, cs_error) = addToAttributeEnviron type_attr cti.cti_lhs_attribute attr_env cs.cs_error
-			= ([type : types], attr_env, (ts, ti, {cs & cs_error = cs_error}))
+			= ([type : types], attr_env, class_defs, (ts, ti, {cs & cs_error = cs_error}))
+
+		bind_context_of_cons [context=:{tc_class,tc_types,tc_var}:contexts] cti class_defs ts ti cs
+			# (tc_class, class_defs, modules, cs=:{cs_error}) = check_context_class tc_class tc_types cti.cti_module_index class_defs ts.ts_modules cs
+			  ts = {ts & ts_modules=modules}
+			| cs_error.ea_ok
+			 	# (tc_types, _, (ts,ti,cs)) = bindTypes cti tc_types (ts,ti,cs)
+				  cs = check_context_types tc_class tc_types cs
+				  (contexts,class_defs,ts,ti,cs) = bind_context_of_cons contexts cti class_defs ts ti cs
+				= ([{context & tc_class=tc_class, tc_types=tc_types}:contexts],class_defs,ts,ti,cs)
+				# (contexts,class_defs,ts,ti,cs) = bind_context_of_cons contexts cti class_defs ts ti cs
+				= ([{context & tc_types = []}:contexts],class_defs,ts,ti,cs)
+		bind_context_of_cons [] cti class_defs ts ti cs
+			= ([],class_defs,ts,ti,cs)
 
 		add_universal_attr_vars [] attr_vars
 			= attr_vars
 		add_universal_attr_vars [{at_type=TFA vars type}:types] attr_vars
 			= add_universal_attr_vars types (add_attr_vars vars attr_vars)
+		add_universal_attr_vars [{at_type=TFAC vars type contexts}:types] attr_vars
+			= add_universal_attr_vars types (add_attr_vars vars attr_vars)
 		add_universal_attr_vars [type:types] attr_vars
 			= add_universal_attr_vars types attr_vars
 
@@ -550,20 +621,21 @@ where
 CS_Checked	:== 1
 CS_Checking	:== 0
 
-checkTypeDefs :: !Index !(Optional (CopiedDefinitions, Int)) !*{# CheckedTypeDef} !*{# ConsDef} !*{# SelectorDef} !*{# DclModule} !*Heaps !*CheckState
-	-> (!*{# CheckedTypeDef}, !*{# ConsDef}, !*{# SelectorDef}, !*{# DclModule}, !*Heaps, !*CheckState)
-checkTypeDefs module_index opt_icl_info type_defs cons_defs selector_defs modules heaps=:{hp_type_heaps,hp_var_heap} cs
+checkTypeDefs :: !Index !(Optional (CopiedDefinitions, Int))
+		!*{#CheckedTypeDef} !*{#ConsDef} !*{#SelectorDef} !v:{#ClassDef} !*{#DclModule} !*Heaps !*CheckState
+	-> (!*{#CheckedTypeDef},!*{#ConsDef},!*{#SelectorDef},!v:{#ClassDef},!*{#DclModule},!*Heaps,!*CheckState)
+checkTypeDefs module_index opt_icl_info type_defs cons_defs selector_defs class_defs modules heaps=:{hp_type_heaps,hp_var_heap} cs
 	#! nr_of_types = size type_defs
 	#  ts = { ts_type_defs = type_defs, ts_cons_defs = cons_defs, ts_selector_defs = selector_defs, ts_modules = modules }
 	   ti = { ti_type_heaps = hp_type_heaps, ti_var_heap = hp_var_heap, ti_used_types = [] }
-	   ({ts_type_defs,ts_cons_defs, ts_selector_defs, ts_modules}, {ti_var_heap,ti_type_heaps}, cs)
-	  		= iFoldSt (check_type_def module_index opt_icl_info) 0 nr_of_types (ts, ti, cs)
-	= (ts_type_defs, ts_cons_defs, ts_selector_defs, ts_modules, {heaps& hp_var_heap=ti_var_heap, hp_type_heaps=ti_type_heaps}, cs)
+	   (class_defs, {ts_type_defs,ts_cons_defs, ts_selector_defs, ts_modules}, {ti_var_heap,ti_type_heaps}, cs)
+	  		= iFoldSt (check_type_def module_index opt_icl_info) 0 nr_of_types (class_defs, ts, ti, cs)
+	= (ts_type_defs, ts_cons_defs, ts_selector_defs, class_defs, ts_modules, {heaps& hp_var_heap=ti_var_heap, hp_type_heaps=ti_type_heaps}, cs)
 where
-	check_type_def module_index opt_icl_info type_index (ts, ti, cs)
+	check_type_def module_index opt_icl_info type_index (class_defs, ts, ti, cs)
 		| has_to_be_checked module_index opt_icl_info type_index
-			= checkTypeDef  type_index module_index ts ti cs
-			= (ts, ti, cs)
+			= checkTypeDef type_index module_index class_defs ts ti cs
+			= (class_defs, ts, ti, cs)
 
 	has_to_be_checked module_index No type_index
 		= True
@@ -755,6 +827,11 @@ checkOpenArgAType mod_index scope dem_attr atype=:{at_type = TFA vars type, at_a
 	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr { atype & at_type = type } (ots, oti, cs)
 	  cs = {cs & cs_symbol_table = remove_universal_vars vars cs.cs_symbol_table}
 	= ({checked_type & at_type = TFA vars checked_type.at_type }, (ots, oti, cs))
+checkOpenArgAType mod_index scope dem_attr atype=:{at_type = TFAC vars type contexts, at_attribute} (ots, oti, cs)
+	# cs = add_universal_vars_again vars cs
+	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr {atype & at_type = type} (ots, oti, cs)
+	  cs = {cs & cs_symbol_table = remove_universal_vars vars cs.cs_symbol_table}
+	= ({checked_type & at_type = TFAC vars checked_type.at_type contexts}, (ots, oti, cs))
 checkOpenArgAType mod_index scope dem_attr type ots_oti_cs
 	= checkOpenAType mod_index scope dem_attr type ots_oti_cs
 
@@ -864,6 +941,9 @@ checkOpenAType mod_index scope dem_attr_kind type=:{ at_type=TQualifiedIdent mod
 checkOpenAType mod_index scope dem_attr atype=:{at_type = TFA vars type} (ots, oti, cs)
 	# cs = universal_quantifier_error vars cs
 	= (atype, (ots, oti, cs))
+checkOpenAType mod_index scope dem_attr atype=:{at_type = TFAC vars type contexts} (ots, oti, cs)
+	# cs = universal_quantifier_error vars cs
+	= (atype, (ots, oti, cs))
 checkOpenAType mod_index scope dem_attr type=:{at_attribute} (ots, oti, cs)
 	# (new_attr, oti, cs) = newAttribute dem_attr "." at_attribute oti cs
 	= ({ type & at_attribute = new_attr}, (ots, oti, cs))
@@ -892,6 +972,27 @@ add_universal_vars vars oti cs
 					({oti & oti_heaps = {oti_heaps & th_vars = th_vars}}, cs))
 			= (atv, (oti, {cs & cs_error = checkError id_name "type variable already defined" cs_error, cs_symbol_table = cs_symbol_table}))
 
+add_universal_vars_again vars cs
+	= foldSt add_universal_var_and_attribute_again vars cs
+  where
+	add_universal_var_and_attribute_again {atv_variable,atv_attribute=TA_Var {av_ident=attr_name=:{id_info},av_info_ptr}} cs=:{cs_symbol_table}
+		# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
+		| ste_kind == STE_Empty || ste_def_level == cModuleScope
+			# cs_symbol_table = cs_symbol_table <:= (id_info,
+				{ste_index = NoIndex, ste_kind = STE_TypeAttribute av_info_ptr, ste_def_level = cGlobalScope, ste_previous = entry})
+			= add_universal_var_again atv_variable {cs & cs_symbol_table=cs_symbol_table}
+			= add_universal_var_again atv_variable {cs & cs_symbol_table=cs_symbol_table}
+	add_universal_var_and_attribute_again {atv_variable} cs
+		= add_universal_var_again atv_variable cs
+
+	add_universal_var_again {tv_ident={id_name,id_info},tv_info_ptr} cs=:{cs_symbol_table}
+		# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
+		| ste_kind == STE_Empty || ste_def_level < cRankTwoScope
+			= {cs & cs_symbol_table = cs_symbol_table <:= (id_info,
+						{ste_index = NoIndex, ste_kind = STE_TypeVariable tv_info_ptr, ste_def_level = cRankTwoScope, ste_previous = entry})}
+			# cs_error = checkError id_name "type variable already defined" cs.cs_error
+			= {cs & cs_symbol_table = cs_symbol_table,cs_error=cs_error}
+
 remove_universal_vars vars symbol_table
 	= foldSt remove_universal_var vars symbol_table
   where
@@ -988,6 +1089,7 @@ checkSymbolType :: !Bool !Index !SymbolType !FunSpecials !u:{#CheckedTypeDef} !v
 checkSymbolType is_function mod_index st=:{st_args,st_result,st_context,st_attr_env} specials type_defs class_defs modules heaps cs
 	# ots = {ots_type_defs = type_defs, ots_modules = modules}
 	  oti = {oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars= []}
+	  (st_args,class_defs,ots,oti,cs) = check_argument_type_contexts st_args mod_index class_defs ots oti cs
 	  (st_args, cot_state) = checkOpenArgATypes mod_index cGlobalScope st_args (ots, oti, cs)
 	  (st_result, (ots, oti=:{oti_all_vars = st_vars,oti_all_attrs = st_attr_vars,oti_global_vars}, cs))
 	  	= checkOpenAType mod_index cGlobalScope DAK_None st_result cot_state	  
@@ -1002,6 +1104,22 @@ checkSymbolType is_function mod_index st=:{st_args,st_result,st_context,st_attr_
 	    					st_attr_vars = st_attr_vars, st_attr_env = st_attr_env }
 	= (checked_st, specials, type_defs, class_defs, modules, heaps, cs)
 where
+	check_argument_type_contexts [arg=:{at_type=TFAC vars type contexts}:args] mod_index class_defs ots oti cs
+		# (vars, (oti, cs)) = add_universal_vars vars oti cs
+		  (contexts, type_defs, class_defs, modules, heaps, cs)
+		  	= checkTypeContexts 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}
+		  cs = {cs & cs_symbol_table = remove_universal_vars vars cs.cs_symbol_table}
+		  arg = {arg & at_type = TFAC vars type contexts}
+	 	  (args,class_defs,ots,oti,cs) = check_argument_type_contexts args mod_index class_defs ots oti cs
+		= ([arg:args],class_defs,ots,oti,cs)
+	check_argument_type_contexts [arg:args] mod_index class_defs ots oti cs
+	 	# (args,class_defs,ots,oti,cs) = check_argument_type_contexts args mod_index class_defs ots oti cs
+		= ([arg:args],class_defs,ots,oti,cs)
+	check_argument_type_contexts [] mod_index class_defs ots oti cs
+		= ([],class_defs,ots,oti,cs)
+
 	check_attr_inequality ineq=:{ai_demanded=ai_demanded=:{av_ident=dem_name},ai_offered=ai_offered=:{av_ident=off_name}} cs=:{cs_symbol_table,cs_error}
 		# (dem_entry, cs_symbol_table) = readPtr dem_name.id_info cs_symbol_table
 		# (found_dem_attr, dem_attr_ptr) = retrieve_attribute dem_entry
diff --git a/frontend/classify.icl b/frontend/classify.icl
index 0e5725f..15b67e5 100644
--- a/frontend/classify.icl
+++ b/frontend/classify.icl
@@ -483,6 +483,16 @@ instance consumerRequirements Expression where
 		= (CPassive, False, ai)
 	consumerRequirements (FailExpr _) _ ai
 		= (CPassive, False, ai)
+	consumerRequirements (DictionariesFunction dictionaries expr expr_type) common_defs ai
+		# (new_next_var,new_next_var_of_fun,ai_var_heap) = init_variables dictionaries ai.ai_next_var ai.ai_next_var_of_fun ai.ai_var_heap
+		# ai = {ai & ai_next_var=new_next_var,ai_next_var_of_fun=new_next_var_of_fun,ai_var_heap=ai_var_heap}
+		= consumerRequirements expr common_defs ai
+		where
+			init_variables [({fv_info_ptr},_):dictionaries] ai_next_var ai_next_var_of_fun ai_var_heap
+				# ai_var_heap = writePtr fv_info_ptr (VI_AccVar ai_next_var ai_next_var_of_fun) ai_var_heap
+				= init_variables dictionaries (inc ai_next_var) (inc ai_next_var_of_fun) ai_var_heap
+			init_variables [] ai_next_var ai_next_var_of_fun ai_var_heap
+				= (ai_next_var,ai_next_var_of_fun,ai_var_heap)
 	consumerRequirements expr _ ai
 		= abort ("consumerRequirements [Expression]" ---> expr)
 
@@ -685,7 +695,7 @@ instance consumerRequirements Case where
 										  		_ -> False
 
 		inspect_patterns :: !{#CommonDefs} !Bool !CasePatterns ![(Int,Bool)] -> (!Bool,!Bool)
-		inspect_patterns common_defs has_default (AlgebraicPatterns {gi_index,gi_module} algebraic_patterns) constructors_and_unsafe_bits
+		inspect_patterns common_defs has_default (AlgebraicPatterns {gi_index,gi_module} _) constructors_and_unsafe_bits
 			# type_def						= common_defs.[gi_module].com_type_defs.[gi_index]
 			  defined_symbols				= case type_def.td_rhs of
 													AlgType defined_symbols		-> defined_symbols
@@ -1473,6 +1483,13 @@ count_locals EE n
 count_locals (FailExpr _) n = n
 count_locals (NoBind _) n
 	= n
+count_locals (DictionariesFunction dictionaries expr expr_type) n
+	= count_locals expr (foldSt count_local_dictionary dictionaries n)
+	where
+		count_local_dictionary ({fv_count},_) n
+			| fv_count > 0
+				= n+1
+				= n
 
 count_optional_locals (Yes e) n
 	= count_locals e n
@@ -1781,6 +1798,8 @@ instance producerRequirements Expression where
 		= (True,prs)
 	producerRequirements (FailExpr _) prs
 		= (True,prs)
+	producerRequirements (DictionariesFunction dictionaries expr expr_type) prs
+		= producerRequirements expr prs
 	producerRequirements expr prs
 		= abort ("producerRequirements " ---> expr)
 
diff --git a/frontend/comparedefimp.icl b/frontend/comparedefimp.icl
index 26c1a4f..a016b40 100644
--- a/frontend/comparedefimp.icl
+++ b/frontend/comparedefimp.icl
@@ -110,9 +110,14 @@ where
 		  comp_type_var_heap = initialyseATypeVars dcl_cons_def.cons_exi_vars icl_cons_def.cons_exi_vars comp_type_var_heap
 		  comp_st = { comp_st & comp_type_var_heap = comp_type_var_heap }
 		  (ok, comp_st) = compare (dcl_cons_type.st_args,dcl_cons_type.st_args_strictness) (icl_cons_type.st_args,icl_cons_type.st_args_strictness) comp_st
-		| ok && do_compare_result_types
-			= compare dcl_cons_type.st_result icl_cons_type.st_result comp_st
-			= (ok, comp_st)
+		| not ok
+			= (False,comp_st)
+		| do_compare_result_types
+			# (ok,comp_st) = compare dcl_cons_type.st_result icl_cons_type.st_result comp_st
+			| ok
+				= compare dcl_cons_type.st_context icl_cons_type.st_context comp_st
+				= (False,comp_st)
+			= compare dcl_cons_type.st_context icl_cons_type.st_context comp_st
 
 compareClassDefs :: !{#Int} {#Bool} !{# ClassDef} !{# MemberDef} !u:{# ClassDef} !v:{# MemberDef} !*CompareState
 	-> (!u:{# ClassDef}, !v:{# MemberDef}, !*CompareState)
@@ -298,6 +303,12 @@ where
 		  type_heaps = clear_type_vars dclvars (comp_st.comp_type_var_heap, comp_st.comp_attr_var_heap)
 		  (comp_type_var_heap, comp_attr_var_heap) = clear_type_vars iclvars type_heaps
 		= (ok, {comp_st & comp_type_var_heap = comp_type_var_heap, comp_attr_var_heap = comp_attr_var_heap})
+	compare (TFAC dclvars dcltype dcl_contexts) (TFAC iclvars icltype icl_contexts) comp_st=:{comp_type_var_heap}
+		# comp_type_var_heap = initialyseATypeVars dclvars iclvars comp_type_var_heap
+		  (ok, comp_st) = compare (dcltype,dcl_contexts) (icltype,icl_contexts) {comp_st & comp_type_var_heap = comp_type_var_heap}
+		  type_heaps = clear_type_vars dclvars (comp_st.comp_type_var_heap, comp_st.comp_attr_var_heap)
+		  (comp_type_var_heap, comp_attr_var_heap) = clear_type_vars iclvars type_heaps
+		= (ok, {comp_st & comp_type_var_heap = comp_type_var_heap, comp_attr_var_heap = comp_attr_var_heap})
 	compare _ _ comp_st
 		= (False, comp_st)
 
@@ -940,6 +951,10 @@ instance t_corresponds Type where
 	t_corresponds (TFA dclVars dclType) (TFA iclVars iclType)
 		=	do (init_atype_vars dclVars iclVars)
 		&&&	t_corresponds dclType iclType
+	t_corresponds (TFAC dclVars dclType dclContexts) (TFAC iclVars iclType iclContexts)
+		=	do (init_atype_vars dclVars iclVars)
+		&&&	t_corresponds dclType iclType
+		&&&	t_corresponds dclContexts iclContexts
 	t_corresponds _ _
 		= return False
 		
@@ -1084,9 +1099,9 @@ instance e_corresponds FunctionBody where
 	// both bodies are either CheckedBodies or TransformedBodies
 	e_corresponds dclDef iclDef
 		=	e_corresponds (from_body dclDef) (from_body iclDef)
-	  where
-		from_body (TransformedBody {tb_args, tb_rhs}) = (tb_args, [tb_rhs])
-		from_body (CheckedBody {cb_args, cb_rhs}) = (cb_args, [ca_rhs \\ {ca_rhs} <- cb_rhs])
+
+from_body (TransformedBody {tb_args, tb_rhs}) = (tb_args, [tb_rhs])
+from_body (CheckedBody {cb_args, cb_rhs}) = (cb_args, [ca_rhs \\ {ca_rhs} <- cb_rhs])
 		
 instance e_corresponds FreeVar where
 	e_corresponds dclVar iclVar
@@ -1387,31 +1402,3 @@ do_nothing ec_state
 give_error s ec_state
 	= { ec_state & ec_error_admin = checkError s ErrorMessage ec_state.ec_error_admin }
 
-/*
-instance <<< Priority
-	where
-		(<<<) file NoPrio = file <<< "NoPrio"		
-		(<<<) file (Prio LeftAssoc i) = file <<< "Prio LeftAssoc " <<< i
-		(<<<) file (Prio RightAssoc i) = file <<< "Prio RightAssoc " <<< i
-		(<<<) file (Prio NoAssoc i) = file <<< "Prio NoAssoc " <<< i
-
-Trace_array a
-	= trace_array 0
-	where
-		trace_array i
-			| i<size a
-				= Trace_tn i && Trace_tn a.[i] && trace_array (i+1)
-				= True;
-
-Trace_tn d
-	= file_to_true (stderr <<< d <<< '\n')
-
-file_to_true :: !File -> Bool;
-file_to_true file = code {
-  .inline file_to_true
-          pop_b 2
-          pushB TRUE
-  .end
- };
-
-*/
\ No newline at end of file
diff --git a/frontend/convertDynamics.icl b/frontend/convertDynamics.icl
index 2780825..26ab7fc 100644
--- a/frontend/convertDynamics.icl
+++ b/frontend/convertDynamics.icl
@@ -301,6 +301,9 @@ instance convertDynamics Expression where
 		= (EE, ci)
 	convertDynamics cinp expr=:(NoBind _) ci
 		= (expr,ci)
+	convertDynamics cinp (DictionariesFunction dictionaries expr expr_type) ci
+		# (expr,ci) = convertDynamics cinp expr ci
+		= (DictionariesFunction dictionaries expr expr_type,ci)
 
 instance convertDynamics App where
 	convertDynamics cinp app=:{app_args} ci
@@ -561,6 +564,7 @@ where
 		# type_fun
 			=	App {app_symb = fun_ident, app_args = [], app_info_ptr = nilPtr}
 		= (App {app_symb = cinp_dynamic_representation.dr_type_code_constructor_symb_ident, app_args = [type_fun], app_info_ptr = nilPtr}, ci)
+
 	typeConstructor (GTT_Basic basic_type) ci
 		#! predefined_TC_basic_type
 			= case basic_type of
@@ -737,7 +741,6 @@ create_dynamic_and_selector_idents common_defs predefined_symbols
 	// otherwise
 		# ({pds_module=pds_module1, pds_def=pds_def1} , predefined_symbols) = predefined_symbols![PD_Dyn_DynamicTemp]
 		# {td_rhs=RecordType {rt_constructor}} = common_defs.[pds_module1].com_type_defs.[pds_def1]
-	
 		# dynamic_defined_symbol
 			= {glob_module = pds_module1, glob_object = rt_constructor}
 		# dynamic_type = {gi_module = pds_module1, gi_index = pds_def1}
diff --git a/frontend/convertcases.icl b/frontend/convertcases.icl
index cb0120e..9f9bd10 100644
--- a/frontend/convertcases.icl
+++ b/frontend/convertcases.icl
@@ -259,6 +259,8 @@ where
 		= rs
 	weightedRefCount rci (NoBind ptr) rs
 		= rs
+	weightedRefCount rci (DictionariesFunction _ expr _) rs
+		= weightedRefCount rci expr rs
 	weightedRefCount rci (FailExpr _) rs
 		= rs
 	weightedRefCount rci expr rs
@@ -582,6 +584,9 @@ where
 		= (NoBind ptr, ds)
 	distributeLets _ (FailExpr id) ds
 		= (FailExpr id, ds)
+	distributeLets di (DictionariesFunction dictionaries expr expr_type) ds
+		# (expr,ds) = distributeLets di expr ds
+		= (DictionariesFunction dictionaries expr expr_type,ds)
 
 instance distributeLets Case
 where
@@ -1641,6 +1646,33 @@ where
 		# (failExpr, cs)
 			=	convertNonRootFail ci ident cs
 		= (failExpr, cs)
+	convertCases ci (DictionariesFunction dictionaries expr expr_type) cs
+		# (expr,cs) = convertRootCases {ci & ci_case_level=CaseLevelRoot,ci_bound_vars=dictionaries++ci.ci_bound_vars} expr cs
+	      (old_fv_info_ptr_values,var_heap) = store_VI_FreeVar_in_dictionary_vars_and_save_old_values dictionaries [] cs.cs_var_heap
+	      (old_fv_info_ptr_values,var_heap) = store_VI_BoundVar_in_bound_vars_and_save_old_values ci.ci_bound_vars old_fv_info_ptr_values var_heap
+		  (expr, {cp_free_vars,cp_var_heap,cp_local_vars}) = copy expr {cp_free_vars=[], cp_var_heap=var_heap, cp_local_vars=[]}
+		  (bound_vars, free_typed_vars, var_heap) = retrieve_variables cp_free_vars cp_var_heap
+		  (free_typed_dictinary_vars, var_heap) = retrieve_dictionary_variables dictionaries var_heap
+		  cs = {cs & cs_var_heap = var_heap}
+		  (fun_ident,cs) = new_case_function No expr_type expr (free_typed_vars++free_typed_dictinary_vars) cp_local_vars ci.ci_group_index cs
+		  cs_var_heap = restore_old_fv_info_ptr_values old_fv_info_ptr_values (dictionaries++ci.ci_bound_vars) cs.cs_var_heap
+		= (App {app_symb=fun_ident, app_args=bound_vars, app_info_ptr=nilPtr}, {cs & cs_var_heap=cs_var_heap})
+	where
+		store_VI_FreeVar_in_dictionary_vars_and_save_old_values [({fv_info_ptr,fv_ident},type):bound_vars] old_fv_info_ptr_values var_heap
+			# (old_fv_info_ptr_value,var_heap) = readPtr fv_info_ptr var_heap
+			  (new_info_ptr,var_heap) = newPtr (VI_Labelled_Empty "convertCases [FreeVar]") var_heap
+			  var_heap = writePtr fv_info_ptr (VI_FreeVar fv_ident new_info_ptr 0 type) var_heap
+			  (old_fv_info_ptr_values,var_heap) = store_VI_FreeVar_in_dictionary_vars_and_save_old_values bound_vars old_fv_info_ptr_values var_heap
+			= ([old_fv_info_ptr_value:old_fv_info_ptr_values],var_heap)
+		store_VI_FreeVar_in_dictionary_vars_and_save_old_values [] old_fv_info_ptr_values var_heap
+			= (old_fv_info_ptr_values,var_heap)
+
+		retrieve_dictionary_variables cp_free_vars cp_var_heap
+			= foldSt retrieve_dictionary_variable cp_free_vars ([], cp_var_heap)
+		where
+			retrieve_dictionary_variable ({fv_info_ptr}, type) (free_typed_vars, var_heap)
+				# (VI_FreeVar name new_ptr count type, var_heap) = readPtr fv_info_ptr var_heap
+				= ([({fv_def_level = NotALevel, fv_ident = name, fv_info_ptr = new_ptr, fv_count = count}, type) : free_typed_vars], var_heap)
 	convertCases ci expr cs
 		= (expr, cs)
 
diff --git a/frontend/expand_types.icl b/frontend/expand_types.icl
index f9591ec..609f6a7 100644
--- a/frontend/expand_types.icl
+++ b/frontend/expand_types.icl
@@ -158,6 +158,11 @@ where
 		| changed

 			= (True,TFA vars type, ets)

 			= (False,tfa_type, ets)

+	expandSynTypes rem_annots common_defs tfac_type=:(TFAC vars type type_context) ets

+		# (changed,type, ets) = expandSynTypes rem_annots common_defs type ets

+		| changed

+			= (True,TFAC vars type type_context, ets)

+			= (False,tfac_type, ets)

 	expandSynTypes rem_annots common_defs type ets

 		= (False,type, ets)

 

diff --git a/frontend/frontend.icl b/frontend/frontend.icl
index 8bac21b..e22dfdd 100644
--- a/frontend/frontend.icl
+++ b/frontend/frontend.icl
@@ -1,6 +1,3 @@
-		/*
-	module owner: Ronny Wichers Schreur
-*/
 implementation module frontend
 
 import scanner, parse, postparse, check, type, trans, partition, convertcases, overloading, utilities, convertDynamics,
@@ -347,17 +344,42 @@ showMacrosInModule dcl_index (macro_defs,file)
 			# (macro,macro_defs) = macro_defs![dcl_index,macro_index]
 			= (macro_defs, file <<< macro_index <<< macro <<< '\n')
 
-showComponents :: !u:{! Group} !Int !Bool !*{# FunDef} !*File  -> (!u:{! Group}, !*{# FunDef},!*File)
+showGroups :: !u:{! Group} !Int !Bool !*{# FunDef} !*File  -> (!u:{! Group}, !*{# FunDef},!*File)
+showGroups comps comp_index show_types fun_defs file
+	| comp_index >= size comps
+		= (comps, fun_defs, file)
+		# (comp, comps) = comps![comp_index]
+		# (fun_defs, file) = show_group comp.group_members show_types fun_defs (file <<< "component " <<< comp_index <<< '\n')
+		= showGroups comps (inc comp_index) show_types fun_defs file
+
+show_group [] show_types fun_defs file
+	= (fun_defs, file <<< '\n')
+show_group [fun:funs] show_types fun_defs file
+	# (fun_def, fun_defs) = fun_defs![fun]
+	# file=file<<<fun<<<'\n'
+	| show_types
+		= show_group funs show_types fun_defs (file <<< fun_def.fun_type <<< '\n' <<< fun_def)
+		= show_group funs show_types fun_defs (file <<< fun_def)
+//		= show_group funs show_types fun_defs (file <<< fun_def.fun_ident)
+
+showComponents :: !u:{!Component} !Int !Bool !*{# FunDef} !*File  -> (!u:{!Component}, !*{# FunDef},!*File)
 showComponents comps comp_index show_types fun_defs file
 	| comp_index >= size comps
 		= (comps, fun_defs, file)
 		# (comp, comps) = comps![comp_index]
-		# (fun_defs, file) = show_component comp.group_members show_types fun_defs (file <<< "component " <<< comp_index <<< '\n')
+		# (fun_defs, file) = show_component comp.component_members show_types fun_defs (file <<< "component " <<< comp_index <<< '\n')
 		= showComponents comps (inc comp_index) show_types fun_defs file
 
-show_component [] show_types fun_defs file
+show_component NoComponentMembers show_types fun_defs file
 	= (fun_defs, file <<< '\n')
-show_component [fun:funs] show_types fun_defs file
+show_component (ComponentMember fun funs) show_types fun_defs file
+	# (fun_def, fun_defs) = fun_defs![fun]
+	# file=file<<<fun<<<'\n'
+	| show_types
+		= show_component funs show_types fun_defs (file <<< fun_def.fun_type <<< '\n' <<< fun_def)
+		= show_component funs show_types fun_defs (file <<< fun_def)
+//		= show_component funs show_types fun_defs (file <<< fun_def.fun_ident)
+show_component (GeneratedComponentMember fun _ funs) show_types fun_defs file
 	# (fun_def, fun_defs) = fun_defs![fun]
 	# file=file<<<fun<<<'\n'
 	| show_types
diff --git a/frontend/mergecases.icl b/frontend/mergecases.icl
index 40f2579..c40bd95 100644
--- a/frontend/mergecases.icl
+++ b/frontend/mergecases.icl
@@ -1,6 +1,3 @@
-/*
-	module owner: Ronny Wichers Schreur
-*/
 implementation module mergecases
 
 import syntax, transform, compare_types, utilities
@@ -147,7 +144,7 @@ where
 	
 	has_no_default No 		= True
 	has_no_default (Yes _) 	= False
-	
+
 	skip_alias var_info_ptr var_heap
 		= case sreadPtr var_info_ptr var_heap of
 			VI_Alias bv
@@ -209,7 +206,7 @@ where
 	new_variable fv=:{fv_ident, fv_info_ptr} var_heap
 		# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
 		= ({fv & fv_info_ptr = new_info_ptr}, var_heap <:= (fv_info_ptr, VI_Variable fv_ident new_info_ptr))
-		
+
 	rebuild_let_expression lad expr var_heap expr_heap
 		# (rev_let_lazy_binds, var_heap) = foldSt renew_let_var lad.let_lazy_binds ([], var_heap)
 		  (let_info_ptr, expr_heap) = newPtr EI_Empty expr_heap
@@ -373,14 +370,14 @@ where
 				= ([ pattern : patterns ], var_heap, symbol_heap, error)
 		merge_basic_pattern_with_patterns new_pattern [] var_heap symbol_heap error
 			= ([new_pattern], var_heap, symbol_heap, error)
-	
+
 	replace_variables vars expr ap_vars var_heap symbol_heap
 		# var_heap = build_aliases vars ap_vars var_heap
 		# us = { us_var_heap = var_heap, us_symbol_heap = symbol_heap, us_local_macro_functions = No }
 		  (expr, us) = unfold expr us
 		= (expr, us.us_var_heap, us.us_symbol_heap)
 	where
-		build_aliases [var1 : vars1] [ {fv_ident,fv_info_ptr} : vars2 ] var_heap
+		build_aliases [var1 : vars1] [{fv_ident,fv_info_ptr} : vars2] var_heap
 			= build_aliases vars1 vars2 (writePtr var1.fv_info_ptr (VI_Variable fv_ident fv_info_ptr) var_heap)
 		build_aliases [] [] var_heap
 			= var_heap
diff --git a/frontend/overloading.icl b/frontend/overloading.icl
index 57d2848..753401f 100644
--- a/frontend/overloading.icl
+++ b/frontend/overloading.icl
@@ -1,6 +1,6 @@
 implementation module overloading
 
-import StdEnv, compare_types
+import StdEnv,StdOverloadedList,compare_types
 
 import syntax, type, expand_types, utilities, unitype, predef, checktypes
 import genericsupport, type_io_common
@@ -60,6 +60,15 @@ overloadingError op_symb err
 	  				-> str+++" [line "+++toString line_nr+++"]"
 	= { err & ea_file = err.ea_file <<< " internal overloading of \"" <<< str <<< "\" could not be solved\n" }
 
+sub_class_error op_symb err
+	# err = errorHeading "Overloading error" err
+	  str = case optBeautifulizeIdent op_symb.id_name of
+	  			No
+	  				-> op_symb.id_name
+	  			Yes (str, line_nr)
+	  				-> str+++" [line "+++toString line_nr+++"]"
+	= {err & ea_file = err.ea_file <<< " internal overloading could not be solved, because subclass of \"" <<< str <<< "\" used\n"}
+
 abstractTypeInDynamicError td_ident err=:{ea_ok}
 	# err = errorHeading "Implementation restriction" err
 	= { err & ea_file = err.ea_file <<< (" derived abstract type '" +++ toString td_ident +++ "' not permitted in a dynamic") <<< '\n' }
@@ -540,6 +549,10 @@ types_are_reducible [type : types] first_type tc_class predef_symbols
 			->	is_lazy_or_strict_array_or_list_context
 		_ :@: _
 			->	is_lazy_or_strict_array_or_list_context
+		TempQV _
+			->	is_lazy_or_strict_array_or_list_context
+		TempQDV _
+			->	is_lazy_or_strict_array_or_list_context
 		_
 			-> is_reducible types tc_class predef_symbols
 where
@@ -820,6 +833,83 @@ where
 					  os = {os & os_type_heaps=os_type_heaps, os_symbol_heap=os_symbol_heap, os_var_heap=os_var_heap,
 								 os_special_instances=os_special_instances, os_error=os_error, os_predef_symbols=os_predef_symbols}
 					-> ([(oc_symbol,fun_index,over_info_ptr,class_applications):reduced_calls],new_contexts,coercion_env,type_pattern_vars,os)
+			(EI_OverloadedWithVarContexts {ocvc_symbol,ocvc_context,ocvc_var_contexts},os_symbol_heap)
+				# rs_state 	= { rs_new_contexts=new_contexts, rs_special_instances = os_special_instances,
+								rs_type_pattern_vars=type_pattern_vars,rs_var_heap=os_var_heap, 
+								rs_type_heaps=os_type_heaps, rs_coercions=coercion_env,
+								rs_predef_symbols=os_predef_symbols, rs_error=os_error}
+				  info = {ri_main_dcl_module_n=main_dcl_module_n, ri_defs=defs, ri_instance_info=instance_info}
+				  (class_applications, rs_state) = reduceContexts info ocvc_context rs_state
+				  {rs_new_contexts=new_contexts, rs_special_instances = os_special_instances,
+				   rs_type_pattern_vars=type_pattern_vars, rs_var_heap=os_var_heap, rs_type_heaps=os_type_heaps,
+				   rs_coercions=coercion_env, rs_predef_symbols=os_predef_symbols, rs_error=os_error}
+						= rs_state
+				  (new_contexts,os_var_heap) = add_var_contexts ocvc_var_contexts new_contexts os_var_heap
+				  os = {os & os_type_heaps=os_type_heaps, os_symbol_heap=os_symbol_heap, os_var_heap=os_var_heap,
+							 os_special_instances=os_special_instances, os_error=os_error, os_predef_symbols=os_predef_symbols}
+				  ocvc_symbol = {ocvc_symbol & symb_kind = case ocvc_symbol.symb_kind of
+															SK_TypeCode
+																-> SK_TypeCodeAndContexts ocvc_var_contexts
+				  											_
+					  											-> SK_VarContexts ocvc_var_contexts
+					  			 }
+				-> ([(ocvc_symbol,fun_index,over_info_ptr,class_applications):reduced_calls],new_contexts,coercion_env,type_pattern_vars,os)
+			(EI_CaseTypeWithContexts case_type constructor_contexts,os_symbol_heap)
+				# (new_contexts,constructor_contexts,os_predef_symbols,os_var_heap) = add_constructor_contexts constructor_contexts new_contexts os_predef_symbols os_var_heap
+				  os_symbol_heap = writePtr over_info_ptr (EI_CaseTypeWithContexts case_type constructor_contexts) os_symbol_heap
+				  os = {os & os_symbol_heap=os_symbol_heap,os_var_heap=os_var_heap,os_predef_symbols=os_predef_symbols}
+				-> (reduced_calls,new_contexts,coercion_env,type_pattern_vars,os)
+	where
+		add_var_contexts NoVarContexts new_contexts var_heap
+			= (new_contexts,var_heap)
+		add_var_contexts (VarContext arg_n contexts arg_atype var_contexts) new_contexts var_heap
+			# (new_contexts,var_heap) = add_contexts contexts new_contexts var_heap
+			= add_var_contexts var_contexts new_contexts var_heap
+
+		add_constructor_contexts [(constructor_symbol,constructor_context):constructor_contexts] new_contexts predef_symbols var_heap
+			# (new_contexts,constructor_context,predef_symbols,var_heap) = add_contexts_of_constructor constructor_context new_contexts predef_symbols var_heap
+			# (new_contexts,constructor_contexts,predef_symbols,var_heap) = add_constructor_contexts constructor_contexts new_contexts predef_symbols var_heap
+			= (new_contexts,[(constructor_symbol,constructor_context):constructor_contexts],predef_symbols,var_heap)
+		add_constructor_contexts [] new_contexts predef_symbols var_heap
+			= (new_contexts,[],predef_symbols,var_heap)
+
+		add_contexts_of_constructor [constructor_context:constructor_contexts] new_contexts predef_symbols var_heap
+			| context_is_reducible constructor_context predef_symbols
+				# (new_contexts,constructor_contexts,predef_symbols,var_heap)
+					= add_contexts_of_constructor constructor_contexts new_contexts predef_symbols var_heap
+				= (new_contexts,[constructor_context:constructor_contexts],predef_symbols,var_heap)
+			# (found,found_context=:{tc_var}) = lookup_context constructor_context new_contexts
+			| found
+				# var_heap
+					= case readPtr tc_var var_heap of
+						(VI_Empty,var_heap)
+							-> writePtr tc_var VI_EmptyConstructorClassVar var_heap
+						(VI_EmptyConstructorClassVar,var_heap)
+							-> var_heap
+				  (new_contexts,constructor_contexts,predef_symbols,var_heap)
+					= add_contexts_of_constructor constructor_contexts new_contexts predef_symbols var_heap
+				  constructor_context = {constructor_context & tc_var=tc_var}
+				= (new_contexts,[constructor_context:constructor_contexts],predef_symbols,var_heap)
+				# var_heap
+					= case readPtr constructor_context.tc_var var_heap of
+						(VI_Empty,var_heap)
+							-> writePtr constructor_context.tc_var VI_EmptyConstructorClassVar var_heap
+						(VI_EmptyConstructorClassVar,var_heap)
+							-> var_heap
+				  new_contexts = [constructor_context : new_contexts]
+				  (new_contexts,constructor_contexts,predef_symbols,var_heap)
+					= add_contexts_of_constructor constructor_contexts new_contexts predef_symbols var_heap
+				= (new_contexts,[constructor_context:constructor_contexts],predef_symbols,var_heap)
+			where
+				lookup_context :: !TypeContext ![TypeContext] -> (!Bool,!TypeContext)
+				lookup_context new_tc [tc : tcs]
+					| new_tc==tc
+						= (True,tc)
+						= lookup_context new_tc tcs
+				lookup_context new_tc []
+					= (False,new_tc)
+		add_contexts_of_constructor [] new_contexts predef_symbols var_heap
+			= (new_contexts,[],predef_symbols,var_heap)
 
 	add_specified_contexts (Yes spec_context, expr_ptrs, pos, index) (contexts,var_heap)
 		= add_contexts spec_context contexts var_heap
@@ -939,6 +1029,19 @@ convertOverloadedCall defs contexts symbol=:{symb_ident, symb_kind = SK_Generic
 convertOverloadedCall defs contexts {symb_ident,symb_kind = SK_TypeCode} expr_info_ptr class_appls (heaps, ptrs, error)
 	# (class_expressions, (heaps, ptrs)) = convertClassApplsToExpressions defs contexts class_appls (heaps, ptrs)
 	= ({heaps & hp_expression_heap = heaps.hp_expression_heap <:= (expr_info_ptr, EI_TypeCodes (map expressionToTypeCodeExpression class_expressions))}, ptrs, error)
+convertOverloadedCall defs contexts {symb_kind=SK_TFACVar var_expr_ptr,symb_ident} expr_info_ptr appls (heaps,ptrs, error)
+	# (class_expressions, (heaps, ptrs)) = convertClassApplsToExpressions defs contexts appls (heaps,ptrs)
+	= ({heaps & hp_expression_heap = heaps.hp_expression_heap <:= (expr_info_ptr, EI_FPContext class_expressions var_expr_ptr)}, ptrs, error)
+convertOverloadedCall defs contexts {symb_kind=SK_VarContexts var_contexts} expr_info_ptr appls (heaps,ptrs, error)
+	# (var_contexts,error) = get_var_contexts var_contexts defs contexts error
+	  (class_expressions, (heaps, ptrs)) = convertClassApplsToExpressions defs contexts appls (heaps,ptrs)
+	  expr_info = EI_ContextWithVarContexts class_expressions var_contexts
+	= ({heaps & hp_expression_heap = writePtr expr_info_ptr expr_info heaps.hp_expression_heap}, [expr_info_ptr:ptrs], error)
+convertOverloadedCall defs contexts {symb_ident,symb_kind = SK_TypeCodeAndContexts univ_contexts} expr_info_ptr class_appls (heaps, ptrs, error)
+	# (univ_contexts,error) = get_var_contexts univ_contexts defs contexts error
+	  (class_expressions, (heaps, ptrs)) = convertClassApplsToExpressions defs contexts class_appls (heaps, ptrs)
+	  expr_info = EI_TypeCodesWithContexts (expressionsToTypeCodeExpressions class_expressions) univ_contexts
+	= ({heaps & hp_expression_heap = writePtr expr_info_ptr expr_info heaps.hp_expression_heap}, ptrs, error)
 convertOverloadedCall defs contexts symbol expr_info_ptr appls (heaps,ptrs, error)
 	# (class_expressions, (heaps, ptrs)) = convertClassApplsToExpressions defs contexts appls (heaps,ptrs)
 	= ({heaps & hp_expression_heap = heaps.hp_expression_heap <:= (expr_info_ptr, EI_Context class_expressions)}, ptrs, error)
@@ -946,6 +1049,34 @@ convertOverloadedCall defs contexts symbol expr_info_ptr appls (heaps,ptrs, erro
 expressionsToTypeCodeExpressions class_expressions
 	= map expressionToTypeCodeExpression class_expressions
 
+get_var_contexts (VarContext arg_n context arg_atype var_contexts) defs contexts error
+	# (cs,error) = get_var_context context contexts error 
+	  cs = [convert_TypeContext_to_DictionaryAndClassType c defs \\ c <- cs]
+	  (var_contexts,error) = get_var_contexts var_contexts defs contexts error
+ 	= (VarContext arg_n cs arg_atype var_contexts,error)
+where
+	get_var_context [] contexts error
+		= ([],error)
+	get_var_context [var_context:var_contexts] contexts error
+		# (var_contexts,error) = get_var_context var_contexts contexts error
+		= get_context var_context var_contexts contexts error
+
+	get_context context var_contexts [c:cs] error
+		| context==c
+			= ([c:var_contexts],error)
+			= get_context context var_contexts cs error
+	get_context {tc_class=TCClass {glob_object={ds_ident}}} var_contexts [] error
+		# error = sub_class_error ds_ident error
+		= (var_contexts,error)
+
+	convert_TypeContext_to_DictionaryAndClassType {tc_var,tc_class=TCClass {glob_module,glob_object={ds_ident,ds_index}},tc_types} defs
+		# {class_dictionary} = 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 = TA dict_type_symbol [AttributedType type \\ type <- tc_types]
+		= {dc_var=tc_var,dc_class_type=AttributedType class_type}
+get_var_contexts NoVarContexts defs contexts error
+	= (NoVarContexts,error)
+
 expressionToTypeCodeExpression (TypeCodeExpression texpr)
 	= texpr
 expressionToTypeCodeExpression (ClassVariable var_info_ptr)
@@ -1128,8 +1259,11 @@ where
 	remove_overloaded_function type_pattern_vars fun_index (ok, fun_defs, fun_env, symbol_heap, type_code_info, var_heap, error, predef_symbols)
 		| ok
 			# (fun_def, fun_defs) = fun_defs![fun_index]  
-			  (CheckedType st=:{st_context}, fun_env) = fun_env![fun_index]
+			  (CheckedType st=:{st_context,st_args}, fun_env) = fun_env![fun_index]
 			  {fun_body = TransformedBody {tb_args,tb_rhs},fun_info,fun_arity,fun_ident,fun_pos} = fun_def
+			  
+			  var_heap = mark_FPC_arguments st_args tb_args var_heap
+			  
 			  error = setErrorAdmin (newPosition fun_ident fun_pos) error
 			  (rev_variables,var_heap,error) = foldSt determine_class_argument st_context ([],var_heap,error)
 			  (type_code_info, symbol_heap, type_pattern_vars, var_heap, error)
@@ -1158,6 +1292,12 @@ where
 				mark_type_codes _ info
 					=	info
 
+	mark_FPC_arguments :: ![AType] ![FreeVar] !*VarHeap -> *VarHeap
+	mark_FPC_arguments st_args tb_args var_heap
+		| has_TFAC st_args
+			= mark_FPC_vars st_args tb_args var_heap
+			= var_heap
+
 	determine_class_argument {tc_class, tc_var} (variables,var_heap,error)
 		# (var_info, var_heap) = readPtr tc_var var_heap
 		= case var_info of
@@ -1166,12 +1306,16 @@ where
 				-> case var_info of
 					VI_Empty
 						-> add_class_var var_info_ptr tc_class var_heap error
+					VI_EmptyConstructorClassVar
+						-> add_class_var var_info_ptr tc_class var_heap error
 					VI_ClassVar _ _ _
 						# error = errorHeading "Overloading error" error
 						  error = {error & ea_file = error.ea_file <<< " a type context occurs multiple times in the specified type\n" }
 						-> ([var_info_ptr : variables],var_heap,error)
 			VI_Empty
 				-> add_class_var tc_var tc_class var_heap error
+			VI_EmptyConstructorClassVar
+				-> add_class_var tc_var tc_class var_heap error
 	where
 		add_class_var var tc_class var_heap error
 			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
@@ -1185,6 +1329,18 @@ where
 		# (VI_ClassVar var_ident new_info_ptr count, var_heap) = readPtr var_info_ptr var_heap
 		= ([{fv_ident = var_ident, fv_info_ptr = new_info_ptr, fv_def_level = NotALevel, fv_count = count } : args], var_heap <:= (var_info_ptr, VI_Empty))
 
+has_TFAC [{at_type=TFAC _ _ _}:_] = True
+has_TFAC [_:atypes] = has_TFAC atypes
+has_TFAC [] = False
+
+mark_FPC_vars [{at_type=TFAC _ _ _}:atypes] [{fv_info_ptr}:args] var_heap
+	# var_heap = writePtr fv_info_ptr VI_FPC var_heap
+	= mark_FPC_vars atypes args var_heap
+mark_FPC_vars [_:atypes] [_:args] var_heap
+	= mark_FPC_vars atypes args var_heap
+mark_FPC_vars [] [] var_heap
+	= var_heap
+
 convertDynamicTypes :: [ExprInfoPtr]
 	   *(*TypeCodeInfo,*ExpressionHeap,[LocalTypePatternVariable],*VarHeap,*ErrorAdmin)
 	-> *(*TypeCodeInfo,*ExpressionHeap,[LocalTypePatternVariable],*VarHeap,*ErrorAdmin)
@@ -1211,6 +1367,14 @@ where
 						  			({ type_code_info & tci_type_var_heap = type_var_heap }, var_heap, error)
 						  expr_heap = expr_heap <:= (dyn_ptr, EI_TypeOfDynamic type_code_expr)
 						-> convert_local_dynamics loc_dynamics (type_code_info, expr_heap, type_pattern_vars, var_heap, error)
+					EI_TypeCodesWithContexts type_codes univ_contexts=:(VarContext _ dictionaries_and_contexts _ _)
+						# (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)
+						  (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}
 				# (expr_info, expr_heap) = readPtr expr_ptr expr_heap
 				-> case expr_info of
@@ -1439,6 +1603,19 @@ where
 						-> (select_expr, { ui & ui_var_heap = ui_var_heap, ui_error = ui_error })
 						-> (select_expr @ all_args, examine_calls context_args
 								{ ui & ui_var_heap = ui_var_heap, ui_error = ui_error })
+				EI_ContextWithVarContexts context_args var_contexts
+					# (app_args,ui) = add_class_vars_for_var_contexts_and_update_expressions var_contexts app_args 0 group_index ui				
+					# (app_args, ui) = adjustClassExpressions symb_ident context_args app_args ui
+					#! main_dcl_module_n = ui.ui_x.UpdateInfoX.x_main_dcl_module_n
+					#! fun_index = get_recursive_fun_index group_index symb_kind main_dcl_module_n ui.ui_fun_defs
+					| fun_index == NoIndex
+						# app = {app & app_args = app_args}
+						-> (App app, examine_calls context_args ui)
+						# (CheckedType {st_context}, ui) = ui!ui_fun_env.[fun_index]
+						  nr_of_context_args = length context_args
+						  nr_of_lifted_contexts = length st_context - nr_of_context_args
+						  (app_args, (ui_var_heap, ui_error)) = mapAppendSt (build_context_arg symb_ident) (take nr_of_lifted_contexts st_context) app_args (ui.ui_var_heap,ui.ui_error)
+						-> (App {app & app_args = app_args}, examine_calls context_args {ui & ui_var_heap = ui_var_heap, ui_error = ui_error })
 	where
 		build_context_arg symb tc=:{tc_var} (var_heap, error)
 			# (var_info, var_heap) = readPtr tc_var var_heap
@@ -1454,6 +1631,37 @@ where
 					-> (Var { var_ident = symb, var_info_ptr = new_info_ptr, var_expr_ptr = nilPtr },
 								(var_heap <:= (tc_var, VI_ClassVar symb new_info_ptr 1), overloadingError symb error))
 
+		add_class_vars_for_var_contexts_and_update_expressions var_contexts=:(VarContext arg_n context arg_atype var_contexts_t) [app_arg:app_args] app_arg_n group_index ui
+			| app_arg_n<arg_n
+				# (app_arg,ui) = updateExpression group_index app_arg ui
+				  (app_args,ui) = add_class_vars_for_var_contexts_and_update_expressions var_contexts app_args (app_arg_n+1) group_index ui
+				= ([app_arg:app_args],ui)
+			| app_arg_n==arg_n
+				# (old_var_infos,var_heap) = add_class_vars_for_var_context context ui.ui_var_heap
+				  (app_arg,ui) = updateExpression group_index app_arg {ui & ui_var_heap=var_heap}
+				  (free_vars_and_types,local_vars,var_heap)
+					= restore_old_var_infos_and_retrieve_class_vars context old_var_infos ui.ui_local_vars ui.ui_var_heap
+				  ui = {ui & ui_local_vars=local_vars,ui_var_heap=var_heap}
+				= case app_arg of
+					expr @ args
+						| same_args args free_vars_and_types
+							# app_arg = expr
+							  (app_args,ui) = add_class_vars_for_var_contexts_and_update_expressions var_contexts_t app_args (app_arg_n+1) group_index ui
+							-> ([app_arg:app_args],ui)
+					_
+						# app_arg = DictionariesFunction free_vars_and_types app_arg arg_atype
+						  (app_args,ui) = add_class_vars_for_var_contexts_and_update_expressions var_contexts_t app_args (app_arg_n+1) group_index ui
+						-> ([app_arg:app_args],ui)
+		add_class_vars_for_var_contexts_and_update_expressions NoVarContexts app_args app_arg_n group_index ui
+			= updateExpression group_index app_args ui
+
+		same_args [] []
+			= True
+		same_args [Var {var_info_ptr}:args] [({fv_info_ptr},_):free_vars_and_types]
+			= var_info_ptr==fv_info_ptr && same_args args free_vars_and_types
+		same_args _ _
+			= False
+
 		get_recursive_fun_index :: !Index !SymbKind Int !{# FunDef} -> Index
 		get_recursive_fun_index group_index (SK_Function {glob_module,glob_object}) main_dcl_module_n fun_defs
 			| glob_module == main_dcl_module_n
@@ -1484,6 +1692,30 @@ where
 		# (let_strict_binds, ui)	= updateExpression group_index let_strict_binds ui
 		# (let_expr, ui)			= updateExpression group_index let_expr ui
 		= (Let {lad & let_lazy_binds = let_lazy_binds, let_strict_binds = let_strict_binds, let_expr = let_expr}, ui)
+
+	updateExpression group_index (Case kees=:{case_guards=case_guards=:AlgebraicPatterns type patterns,case_expr,case_default,case_info_ptr}) ui
+		# (case_info, ui_symbol_heap) = readPtr case_info_ptr ui.ui_symbol_heap
+		  ui = {ui & ui_symbol_heap = ui_symbol_heap}
+		= case case_info of
+			EI_CaseTypeWithContexts case_type=:{ct_cons_types} constructorcontexts
+				# (case_expr,ui) = updateExpression group_index case_expr ui
+				  (patterns,ct_cons_types,ui) = update_constructors_with_contexts_patterns constructorcontexts patterns ct_cons_types group_index ui
+				  case_guards = AlgebraicPatterns type patterns
+				  (case_default,ui) = updateExpression group_index case_default ui
+				  ui_symbol_heap = writePtr case_info_ptr (EI_CaseType {case_type & ct_cons_types=ct_cons_types}) ui.ui_symbol_heap
+				  ui = {ui & ui_symbol_heap = ui_symbol_heap}
+				-> (Case {kees & case_expr = case_expr, case_guards = case_guards, case_default = case_default}, ui)
+			EI_CaseType {ct_cons_types}
+				| Any has_TFAC ct_cons_types
+					# (case_expr,ui) = updateExpression group_index case_expr ui
+					  (patterns, ui) = update_algebraic_patterns patterns ct_cons_types group_index ui
+					  case_guards = AlgebraicPatterns type patterns
+					  (case_default, ui) = updateExpression group_index case_default ui
+					-> (Case {kees & case_expr = case_expr, case_guards = case_guards, case_default = case_default}, ui)
+			_
+				# ((case_expr,(case_guards,case_default)), ui) = updateExpression group_index (case_expr,(case_guards,case_default)) ui
+				-> (Case {kees & case_expr = case_expr, case_guards = case_guards, case_default = case_default}, ui)
+
 	updateExpression group_index case_expr=:(Case {case_guards=NewTypePatterns _ _}) ui
 		= remove_NewTypePatterns_case_and_update_expression case_expr group_index ui
 	updateExpression group_index (Case kees=:{case_expr,case_guards,case_default}) ui
@@ -1503,7 +1735,21 @@ where
 		  (expressions, ui) = updateExpression group_index expressions ui
 		= (RecordUpdate cons_symbol expression expressions, ui)
 	updateExpression group_index (DynamicExpr dyn=:{dyn_expr,dyn_info_ptr}) ui=:{ui_has_type_codes}
-		# (dyn_expr, ui) = updateExpression group_index dyn_expr {ui & ui_has_type_codes = False}
+		# (dyn_info, ui_symbol_heap) = readPtr dyn_info_ptr ui.ui_symbol_heap
+		  ui = {ui & ui_has_type_codes = False, ui_symbol_heap = ui_symbol_heap}
+		  (dyn_expr,type_code,ui)
+			= case dyn_info of
+				EI_TypeOfDynamic type_code
+					# (dyn_expr, ui) = updateExpression group_index dyn_expr ui
+					-> (dyn_expr,type_code,ui)
+				EI_TypeOfDynamicWithContexts type_code (VarContext _ context dynamic_expr_type NoVarContexts)
+					# (old_var_infos,var_heap) = add_class_vars_for_var_context context ui.ui_var_heap
+					  (dyn_expr,ui) = updateExpression group_index dyn_expr {ui & ui_var_heap=var_heap}
+					  (free_vars_and_types,local_vars,var_heap)
+						= restore_old_var_infos_and_retrieve_class_vars context old_var_infos ui.ui_local_vars ui.ui_var_heap
+					  ui = {ui & ui_local_vars=local_vars,ui_var_heap=var_heap}
+					  dyn_expr = DictionariesFunction free_vars_and_types dyn_expr dynamic_expr_type
+					-> (dyn_expr,type_code,ui)
 		  ui = check_type_codes_in_dynamic ui
 			with
 				check_type_codes_in_dynamic ui=:{ui_has_type_codes, ui_error}
@@ -1512,8 +1758,6 @@ where
 						= {ui & ui_error = ui_error}
 						= ui
 		  ui = {ui & ui_has_type_codes=ui_has_type_codes}
-		  (EI_TypeOfDynamic type_code, ui_symbol_heap) = readPtr dyn_info_ptr ui.ui_symbol_heap
-		  ui = { ui & ui_symbol_heap = ui_symbol_heap }
 		= (DynamicExpr { dyn & dyn_expr = dyn_expr, dyn_type_code = type_code }, ui)
 	updateExpression group_index (TupleSelect symbol argn_nr expr) ui
 		# (expr, ui) = updateExpression group_index expr ui
@@ -1529,7 +1773,7 @@ where
 		= (IsConstructor expr cons_symbol cons_arity global_type_index case_ident position, ui)
 	updateExpression group_index (TypeSignature _ expr) ui
 		= updateExpression group_index expr ui
-	updateExpression group_index expr=:(Var {var_info_ptr}) ui
+	updateExpression group_index expr=:(Var {var_info_ptr,var_expr_ptr,var_ident}) ui
 		# (var_info,var_heap) = readPtr var_info_ptr ui.ui_var_heap
 		# ui = {ui & ui_var_heap = var_heap}
 		= case var_info of
@@ -1537,6 +1781,14 @@ where
 				# (var_info2,var_heap) = readPtr var2.var_info_ptr ui.ui_var_heap
 				# ui = { ui & ui_var_heap = var_heap }
 				-> skip_aliases var_info2 var2 var_info_ptr ui
+			VI_FPC
+				# (expr_info,ui_symbol_heap) = readPtr var_expr_ptr ui.ui_symbol_heap
+				# ui = {ui & ui_symbol_heap=ui_symbol_heap}
+				-> case expr_info of
+					EI_FPContext context_args var_expr_ptr
+						# (app_args, ui) = adjustClassExpressions var_ident context_args [] ui
+						# ui = examine_calls context_args ui
+						-> (expr @ app_args,ui)
 			_
 				-> (expr,ui)
 	where
@@ -1552,6 +1804,83 @@ where
 	updateExpression group_index expr ui
 		= (expr, ui)
 
+update_constructors_with_contexts_patterns [constructor_context:constructor_contexts] patterns cons_types group_index ui
+	= update_constructor_with_contexts_patterns constructor_context constructor_contexts patterns cons_types group_index ui
+where
+	update_constructor_with_contexts_patterns constructor_context=:(constructor_symbol,context) constructor_contexts [pattern:patterns] [cons_type:cons_types] group_index ui
+		| constructor_symbol==pattern.ap_symbol.glob_object
+			# (old_var_infos,var_heap) = make_class_vars context ui.ui_var_heap
+			  ui = {ui & ui_var_heap=var_heap}					  
+
+			  (expr,ui) = updateExpression group_index pattern.ap_expr ui
+
+			  vars = pattern.ap_vars
+			  arity = pattern.ap_symbol.glob_object.ds_arity
+			  (vars,arity,local_vars,var_heap) = add_class_vars_to_pattern_and_restore_old_var_infos context old_var_infos vars arity ui.ui_local_vars ui.ui_var_heap
+			  ui = {ui & ui_local_vars=local_vars,ui_var_heap=var_heap}
+			  pattern = {pattern & ap_vars=vars,ap_expr=expr,ap_symbol.glob_object.ds_arity=arity}
+			  (patterns,cons_types,ui) = update_constructors_with_contexts_patterns constructor_contexts patterns cons_types group_index ui
+
+			  (common_defs,ui) = ui!ui_x.x_type_code_info.tci_common_defs
+			  cons_type = addTypesOfDictionaries common_defs context cons_type
+
+			= ([pattern:patterns],[cons_type:cons_types],ui)
+
+			# (pattern,ui) = updateExpression group_index pattern ui
+			  (patterns,cons_types,ui) = update_constructor_with_contexts_patterns constructor_context constructor_contexts patterns cons_types group_index ui
+			= ([pattern:patterns],[cons_type:cons_types],ui)
+
+	make_class_vars [tc=:{tc_class,tc_var}:contexts] var_heap
+		# (old_var_infos,var_heap) = make_class_vars contexts var_heap
+		  (old_var_info,var_heap) = readPtr tc_var var_heap
+	  	  (var_info_ptr, var_heap) = newPtr VI_Empty var_heap
+		  ident = {id_name = "_v" +++ toString tc_class, id_info = nilPtr}
+		  (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
+		  var_heap = writePtr tc_var (VI_ClassVar ident new_info_ptr 0) var_heap
+		= ([old_var_info:old_var_infos],var_heap)
+	make_class_vars [] var_heap
+		= ([],var_heap)
+
+	add_class_vars_to_pattern_and_restore_old_var_infos [{tc_var}:contexts] [old_var_info:old_var_infos] vars arity local_vars var_heap
+		# (vars,arity,local_vars,var_heap) = add_class_vars_to_pattern_and_restore_old_var_infos contexts old_var_infos vars arity local_vars var_heap
+		  (VI_ClassVar var_ident new_info_ptr count, var_heap) = readPtr tc_var var_heap
+		  free_var = {fv_ident=var_ident, fv_info_ptr=new_info_ptr, fv_def_level=NotALevel, fv_count=count}
+		  var_heap = writePtr tc_var old_var_info var_heap
+		= ([free_var:vars],arity+1,[free_var:local_vars],var_heap)
+	add_class_vars_to_pattern_and_restore_old_var_infos [] [] vars arity local_vars var_heap
+		= (vars,arity,local_vars,var_heap)
+update_constructors_with_contexts_patterns [] patterns cons_types group_index ui
+	# (patters,ui) = updateExpression group_index patterns ui
+	= (patters,cons_types,ui)
+
+update_algebraic_patterns [pattern=:{ap_expr,ap_vars}:patterns] [cons_arg_types:conses_args_types] group_index ui
+	# ui & ui_var_heap = mark_FPC_vars cons_arg_types ap_vars ui.ui_var_heap
+	# (ap_expr,ui) = updateExpression group_index ap_expr ui
+	# (patterns,ui) = update_algebraic_patterns patterns conses_args_types group_index ui
+	= ([{pattern & ap_expr=ap_expr}:patterns],ui)
+update_algebraic_patterns [] [] group_index ui
+	= ([],ui)
+
+add_class_vars_for_var_context [{dc_var}:contexts] var_heap
+	# (var_info,var_heap) = readPtr dc_var var_heap
+	  symb = {id_name = "_d", id_info = nilPtr}
+	  (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
+	  var_heap = writePtr dc_var (VI_ClassVar symb new_info_ptr 0) var_heap
+	  (old_var_infos,var_heap) = add_class_vars_for_var_context contexts var_heap
+	= ([var_info:old_var_infos],var_heap)
+add_class_vars_for_var_context [] var_heap
+	= ([],var_heap)
+
+restore_old_var_infos_and_retrieve_class_vars [{dc_var,dc_class_type}:contexts] [old_var_info:old_var_infos] local_vars var_heap		
+	# (VI_ClassVar var_ident new_info_ptr count, var_heap) = readPtr dc_var var_heap
+	  free_var = {fv_ident=var_ident, fv_info_ptr=new_info_ptr, fv_def_level=NotALevel, fv_count=count}
+	  var_heap = writePtr dc_var old_var_info var_heap
+	  (free_vars_and_types,local_vars,var_heap)
+	  	= restore_old_var_infos_and_retrieve_class_vars contexts old_var_infos local_vars var_heap
+	= ([(free_var,dc_class_type):free_vars_and_types],[free_var:local_vars],var_heap)
+restore_old_var_infos_and_retrieve_class_vars [] [] local_vars var_heap
+	= ([],local_vars,var_heap)
+
 examine_calls [expr : exprs] ui
 	= examine_calls exprs (examine_calls_in_expr expr ui)
 where
diff --git a/frontend/parse.icl b/frontend/parse.icl
index b1b16f5..6f6b138 100644
--- a/frontend/parse.icl
+++ b/frontend/parse.icl
@@ -425,7 +425,7 @@ where
 		| ~(isGlobalContext parseContext)
 			= (False,abort "no def(3)",parseError "definition" No "imports only at the global level" pState)
 			# (imp, pState) = wantFromImports pState
-	   		= (True, PD_Import [imp], pState) -->> imp
+	   		= (True, PD_Import [imp], pState)
 	try_definition parseContext ClassToken pos pState
 		| ~(isGlobalContext parseContext)
 			= (False,abort "no def(2)",parseError "definition" No "class definitions are only at the global level" pState)
@@ -1131,7 +1131,7 @@ where
 			  (file_name, line_nr, pState)
 			  					= getFileAndLineNr pState
 			  (rhs_exp, pState) = wantExpression pState
-			  pState			= wantEndRootExpression pState -->> ("#",lhs_exp,"=",rhs_exp)
+			  pState			= wantEndRootExpression pState // -->> ("#",lhs_exp,"=",rhs_exp)
 	  	  	  (locals , pState) = optionalLocals WithToken localsExpected pState
 			=	( True
 				, {	ndwl_strict	= strict
@@ -1536,6 +1536,13 @@ optionalContext pState
 		= want_contexts pState
 		= ([], tokenBack pState)
 
+optional_constructor_context :: !ParseState -> ([TypeContext],ParseState)
+optional_constructor_context pState
+	# (token, pState) = nextToken TypeContext pState
+	| token == AndToken
+		= want_contexts pState
+		= ([], tokenBack pState)
+
 want_contexts :: ParseState -> ([TypeContext],ParseState)
 want_contexts pState
 	# (contexts, pState) = want_context pState
@@ -1926,8 +1933,9 @@ where
 		# token = basic_type_to_constructor token
 		# (pc_cons_ident,  pc_cons_prio, pc_cons_pos, pState) = want_cons_name_and_prio token pState
 		  (pc_arg_types, pState) = parseList tryBrackSAType pState
+		  (pc_context,pState) = optional_constructor_context pState
 		  cons = {	pc_cons_ident = pc_cons_ident, pc_arg_types = atypes_from_satypes pc_arg_types, pc_args_strictness=strictness_from_satypes pc_arg_types,
-		  			pc_cons_arity = length pc_arg_types, pc_cons_prio = pc_cons_prio, pc_exi_vars = exi_vars, pc_cons_pos = pc_cons_pos}
+		  			pc_context = pc_context, pc_cons_arity = length pc_arg_types, pc_cons_prio = pc_cons_prio, pc_exi_vars = exi_vars, pc_cons_pos = pc_cons_pos}
 		= (cons,pState)
 
 	want_newtype_constructor :: ![ATypeVar] !Token !ParseState -> (.ParsedConstructor,!ParseState)
@@ -1936,7 +1944,7 @@ where
 		  (pc_cons_ident,  pc_cons_prio, pc_cons_pos, pState) = want_cons_name_and_prio token pState
 		  (succ, pc_arg_type, pState) = trySimpleType TA_Anonymous pState
 		  cons = {	pc_cons_ident = pc_cons_ident, pc_arg_types = [pc_arg_type], pc_args_strictness = NotStrict,
-		  			pc_cons_arity = 1, pc_cons_prio = pc_cons_prio, pc_exi_vars = exi_vars, pc_cons_pos = pc_cons_pos}
+		  			pc_context = [], pc_cons_arity = 1, pc_cons_prio = pc_cons_prio, pc_exi_vars = exi_vars, pc_cons_pos = pc_cons_pos}
 		| succ
 			= (cons,pState)
 			= (cons,parseError "newtype definition" No "type" pState)
@@ -2271,50 +2279,53 @@ where
 
 :: AnnotationWithPosition = NoAnnot | StrictAnnotWithPosition !FilePosition;
 
-wantAnnotatedATypeWithPosition :: !ParseState -> (!AnnotationWithPosition,!AType,!ParseState)
-wantAnnotatedATypeWithPosition pState
-	# (vars , pState)		= optionalUniversalQuantifiedVariables pState	
+wantAnnotatedATypeWithPositionT :: !Token !ParseState -> (!AnnotationWithPosition,!AType,!ParseState)
+wantAnnotatedATypeWithPositionT ForAllToken pState
+	# (vars, pState)		= wantUniversalQuantifiedVariables pState
 	# (_,annotation,pState) = optionalAnnotWithPosition pState
-	# (succ, atype, pState)	= tryAnnotatedAType True TA_None vars pState
+	# (succ, atype, pState)	= tryAnnotatedAType TA_None pState
+	# atype = {atype & at_type = TFA vars atype.at_type}
 	| succ
 		= (annotation, atype, pState)
-	// otherwise //~ succ
-		# (token, pState) = nextToken TypeContext pState
-		= (annotation, atype, parseError "atype" (Yes token) "attributed and annotated type" pState)
+		= (annotation, atype, attributed_and_annotated_type_error pState)
+wantAnnotatedATypeWithPositionT noForAllToken pState
+	= wantAnnotatedATypeWithPosition_noUniversalQuantifiedVariables (tokenBack pState)
+
+wantAnnotatedATypeWithPosition_noUniversalQuantifiedVariables pState
+	# (_,annotation,pState) = optionalAnnotWithPosition pState
+	# (succ, atype, pState)	= tryAnnotatedAType TA_None pState
+	| succ
+		= (annotation, atype, pState)
+		= (annotation, atype, attributed_and_annotated_type_error pState)
 
 wantAnnotatedAType :: !ParseState -> (!Annotation,!AType,!ParseState)
 wantAnnotatedAType pState
 	# (vars , pState)		= optionalUniversalQuantifiedVariables pState	
 	# (_,annotation,pState) = optionalAnnot pState
-	# (succ, atype, pState)	= tryAnnotatedAType True TA_None vars pState
-	| succ
-		= (annotation, atype, pState)
-	// otherwise //~ succ
-		# (token, pState) = nextToken TypeContext pState
-		= (annotation, atype, parseError "atype" (Yes token) "attributed and annotated type" pState)
+	| isEmpty vars
+		# (succ, atype, pState)	= tryAnnotatedAType TA_None pState
+		| succ
+			= (annotation, atype, pState)
+			= (annotation, atype, attributed_and_annotated_type_error pState)
+		# (succ, atype, pState)	= tryAnnotatedAType TA_None pState
+		# atype = {atype & at_type = TFA vars atype.at_type}
+		| succ
+			= (annotation, atype, pState)
+			= (annotation, atype, attributed_and_annotated_type_error pState)
 
-tryAnnotatedAType :: !Bool !TypeAttribute ![ATypeVar] !ParseState -> (!Bool, !AType,!ParseState)
-tryAnnotatedAType tryAA attr vars pState
+tryAnnotatedAType :: !TypeAttribute !ParseState -> (!Bool, !AType,!ParseState)
+tryAnnotatedAType attr pState
 	# (types, pState)		= parseList tryBrackAType pState
 	| isEmpty types
-		| isEmpty vars
-			= (False, {at_attribute = attr, at_type = TE}, pState)
-		// otherwise // PK
-			# (token, pState) = nextToken TypeContext pState
-			= (False, {at_attribute = attr, at_type = TFA vars TE}
-			  , parseError "annotated type" (Yes token) "type" (tokenBack pState))
+		= (False, {at_attribute = attr, at_type = TE}, pState)
 	# (token, pState)		= nextToken TypeContext pState
 	| token == ArrowToken
 		# (rtype, pState)	= wantAType pState
 		  atype = make_curry_type attr types rtype
-		| isEmpty vars
-			= ( True, atype, pState)
-			= ( True, { atype & at_type = TFA vars atype.at_type }, pState)
+		= ( True, atype, pState)
 	// otherwise (note that types is non-empty)
 	# (atype, pState) = convertAAType types attr (tokenBack pState)
-	| isEmpty vars
-		= (True, atype, pState)
-		= (True, { atype & at_type = TFA vars atype.at_type }, pState)
+	= (True, atype, pState)
 where
 	make_curry_type attr [t1] res_type
 		= {at_attribute = attr, at_type = t1 --> res_type}
@@ -2322,37 +2333,81 @@ where
 		= {at_attribute = attr, at_type = t1 --> make_curry_type TA_None tr res_type}
 	make_curry_type _ _ _ = abort "make_curry_type: wrong assumption"
 
-tryBrackSAType :: !ParseState -> (!Bool, SAType, !ParseState)
-tryBrackSAType pState
-	// type of constructor argument
-	# (succ, annot, attr, pState) = optionalAnnotAndAttr pState
-	| succ
-		# (token, pState) = nextToken TypeContext pState
-		# (result, atype, pState) = trySimpleTypeT token attr pState
-		# sa_type = {s_annotation=annot,s_type=atype}
-		| result==ParseOk
-			= (True, sa_type, pState)
-		| result==ParseFailWithError
-			= (False, sa_type, pState)
-			= (False, sa_type, parseError "constructor type" (Yes token) "type" pState)
-		# (succ, atype, pState) = trySimpleType attr pState
-		= (succ, {s_annotation=annot,s_type=atype}, pState)
+:: ParseResult :== Int
+ParseOk:==0
+ParseFailWithError:==1
+ParseFailWithoutError:==2
+
+tryBrackAType_allow_universal_quantifier :: !TypeAttribute !ParseState -> (!Bool, AType, !ParseState)
+tryBrackAType_allow_universal_quantifier attr pState
+	# (token, pState) = nextToken TypeContext pState
+	# (result,atype,pState) = tryBrackATypeT_allow_universal_quantifier token attr pState
+	= (result==ParseOk,atype,pState)
+
+tryBrackATypeT_allow_universal_quantifier :: !Token !TypeAttribute !ParseState -> (!ParseResult, AType, !ParseState)
+tryBrackATypeT_allow_universal_quantifier OpenToken attr pState
+	// type of function or constructor argument
+	# (token, pState) = nextToken TypeContext pState
+	= case token of
+		ForAllToken
+			# (vars,pState) = wantUniversalQuantifiedVariables pState 
+			  (annot_with_pos, atype, pState) = wantAnnotatedATypeWithPosition_noUniversalQuantifiedVariables pState
+			  (token, pState) = nextToken TypeContext pState
+			-> case token of
+				BarToken
+					# (contexts, pState) = want_contexts pState
+					  (token, pState) = nextToken TypeContext pState
+					  (succ,atype,pState)
+						= case token of
+							CloseToken
+								# type = atype.at_type
+								  (attr, pState) = determAttr attr atype.at_attribute type pState
+								  pState = warnIfStrictAnnot annot_with_pos pState
+								-> (ParseOk, {at_attribute = attr, at_type = type}, pState)
+							_
+								-> (ParseFailWithError, atype, parseError "Simple type" (Yes token) "')' or ','" pState)
+					  atype = {atype & at_type = TFAC vars atype.at_type contexts}
+					-> (succ, atype, pState)
+				_
+					# atype = {atype & at_type = TFA vars atype.at_type}
+					-> trySimpleTypeT_after_OpenToken_and_type token annot_with_pos atype attr pState
+		_
+			-> trySimpleTypeT_after_OpenToken token attr pState
+tryBrackATypeT_allow_universal_quantifier token attr pState
+	= trySimpleTypeT token attr pState
 
 tryBrackSATypeWithPosition :: !ParseState -> (!Bool, SATypeWithPosition, !ParseState)
 tryBrackSATypeWithPosition pState
+	// type of function argument
 	# (succ, annot, attr, pState) = optionalAnnotAndAttrWithPosition pState
 	| succ
 		# (token, pState) = nextToken TypeContext pState
-		# (result, atype, pState) = trySimpleTypeT token attr pState
+		# (result, atype, pState) = tryBrackATypeT_allow_universal_quantifier token attr pState
 		# sa_type_wp = {sp_annotation=annot,sp_type=atype}
 		| result==ParseOk
 			= (True, sa_type_wp, pState)
 		| result==ParseFailWithError
 			= (False, sa_type_wp, pState)
 			= (False, sa_type_wp, parseError "symbol type" (Yes token) "type" pState)
-		# (succ, atype, pState) = trySimpleType attr pState
+		# (succ, atype, pState) = tryBrackAType_allow_universal_quantifier attr pState
 		= (succ, {sp_annotation=annot,sp_type=atype}, pState)
 
+tryBrackSAType :: !ParseState -> (!Bool, SAType, !ParseState)
+tryBrackSAType pState
+	// type of constructor argument
+	# (succ, annot, attr, pState) = optionalAnnotAndAttr pState
+	| succ
+		# (token, pState) = nextToken TypeContext pState
+		# (result, atype, pState) = tryBrackATypeT_allow_universal_quantifier token attr pState
+		# sa_type = {s_annotation=annot,s_type=atype}
+		| result==ParseOk
+			= (True, sa_type, pState)
+		| result==ParseFailWithError
+			= (False, sa_type, pState)
+			= (False, sa_type, parseError "constructor type" (Yes token) "type" pState)
+		# (succ, atype, pState) = tryBrackAType_allow_universal_quantifier attr pState
+		= (succ, {s_annotation=annot,s_type=atype}, pState)
+
 instance want AType
 where
 	want pState = wantAType pState
@@ -2482,11 +2537,6 @@ tryBrackAType pState
 	# (_, attr, pState)	= warnAnnotAndOptionalAttr pState
 	= trySimpleType attr pState
 
-:: ParseResult :== Int
-ParseOk:==0
-ParseFailWithError:==1
-ParseFailWithoutError:==2
-
 trySimpleType :: !TypeAttribute !ParseState -> (!Bool, !AType, !ParseState)
 trySimpleType attr pState
 	# (token, pState)		= nextToken TypeContext pState
@@ -2629,7 +2679,7 @@ trySimpleTypeT_after_OpenToken ArrowToken attr pState
 		= (ParseFailWithError,{at_attribute = attr, at_type = TE},
 			parseError "arrow type" (Yes token) ")" pState)
 trySimpleTypeT_after_OpenToken token attr pState
-	# (annot_with_pos,atype, pState) = wantAnnotatedATypeWithPosition (tokenBack pState)
+	# (annot_with_pos,atype, pState) = wantAnnotatedATypeWithPositionT token pState
 	  (token, pState)	= nextToken TypeContext pState
 	= trySimpleTypeT_after_OpenToken_and_type token annot_with_pos atype attr pState
 
@@ -4283,7 +4333,7 @@ skipToEndOfDefinition pState
 		EndGroupToken		-> (token, pState)
 		EndOfFileToken		-> (token, pState)
 //		SemicolonToken		-> (token, pState) // might be useful in non layout mode.
-		_					-> skipToEndOfDefinition pState -->> (token,"skipped")
+		_					-> skipToEndOfDefinition pState // -->> (token,"skipped")
 
 wantEndCodeRhs :: !ParseState -> ParseState
 wantEndCodeRhs pState
diff --git a/frontend/partition.icl b/frontend/partition.icl
index 74bada3..56701d4 100644
--- a/frontend/partition.icl
+++ b/frontend/partition.icl
@@ -437,6 +437,8 @@ where
 		= fc_state
 	find_calls fc_info (FailExpr _) fc_state
 		= fc_state
+	find_calls fc_info (DictionariesFunction dictionaries expr expr_type) fc_state
+		= find_calls fc_info expr fc_state
 
 instance find_calls App
 where
diff --git a/frontend/postparse.icl b/frontend/postparse.icl
index b1e3b7c..d47b3d0 100644
--- a/frontend/postparse.icl
+++ b/frontend/postparse.icl
@@ -1300,7 +1300,7 @@ reorganiseDefinitions icl_module [PD_Type type_def=:{td_ident, td_rhs = Selector
 	  cons_arity = new_count - sel_count
 	  pc_arg_types = [ ps_field_type \\ {ps_field_type} <- sel_defs ]
 	  cons_def = {	pc_cons_ident = rec_cons_id, pc_cons_prio = NoPrio, pc_cons_arity = cons_arity, pc_cons_pos = td_pos,
-	  				pc_arg_types = pc_arg_types, pc_args_strictness=strictness_from_fields sel_defs,pc_exi_vars = exivars }
+	  				pc_arg_types = pc_arg_types, pc_args_strictness=strictness_from_fields sel_defs,pc_context=[], pc_exi_vars = exivars }
 	  type_def = { type_def & td_rhs = RecordType {rt_constructor = { ds_ident = rec_cons_id, ds_arity = cons_arity, ds_index = cons_count },
 	  							rt_fields =  { sel \\ sel <- sel_syms }, rt_is_boxed_record = is_boxed_record}}
 	  c_defs = { c_defs & def_types = [type_def : c_defs.def_types], def_constructors = [ParsedConstructorToConsDef cons_def : c_defs.def_constructors],
diff --git a/frontend/predef.icl b/frontend/predef.icl
index 75e372f..8157dfd 100644
--- a/frontend/predef.icl
+++ b/frontend/predef.icl
@@ -415,9 +415,9 @@ make_list_definition list_type_pre_def_symbol_index cons_pre_def_symbol_index ni
 	  nil_symb = { ds_ident = nil_ident, ds_arity=0 ,ds_index = nil_pre_def_symbol_index-FirstConstructorPredefinedSymbolIndex }
 	  (list_def, pre_def_symbols) = make_type_def list_type_pre_def_symbol_index [type_var] (AlgType [cons_ds,nil_symb]) pre_def_symbols	
 	  list_type = MakeAttributedType (TA (MakeNewTypeSymbIdent list_ident 1) [type_var_with_attr])
-	  cons_def = {	pc_cons_ident = cons_ident, pc_cons_arity = 2, pc_arg_types = [type_var_with_attr, list_type],
+	  cons_def = {	pc_cons_ident = cons_ident, pc_cons_arity = 2, pc_arg_types = [type_var_with_attr, list_type], pc_context = [],
 				 	pc_args_strictness=cons_strictness,	pc_cons_prio =  NoPrio, pc_exi_vars = [], pc_cons_pos = PreDefPos pre_mod_id}
-	  nil_def = {	pc_cons_ident = nil_ident, pc_cons_arity = 0, pc_arg_types = [], pc_args_strictness=NotStrict,
+	  nil_def = {	pc_cons_ident = nil_ident, pc_cons_arity = 0, pc_arg_types = [], pc_args_strictness=NotStrict, pc_context = [],
 	  				pc_cons_prio =  NoPrio, pc_exi_vars = [], pc_cons_pos = PreDefPos pre_mod_id}
 	= (list_def,ParsedConstructorToConsDef cons_def,ParsedConstructorToConsDef nil_def,pre_def_symbols);
 
@@ -476,7 +476,7 @@ where
 			  (tuple_type_def, pre_def_symbols)	= make_type_def (GetTupleTypeIndex tup_arity) type_vars (AlgType [tuple_cons_symb]) pre_def_symbols
 			  tuple_cons_def	= { pc_cons_ident = tuple_ident, pc_cons_arity = tup_arity, pc_cons_pos = PreDefPos pre_mod_id,
 			  						pc_arg_types = [ MakeAttributedType (TV tv) \\ tv <- type_vars],
-			  						pc_args_strictness = NotStrict,
+			  						pc_args_strictness = NotStrict, pc_context = [],
 			  						pc_cons_prio =  NoPrio, pc_exi_vars = []}
 			= add_tuple_defs pre_mod_id (dec tup_arity) [tuple_type_def : type_defs] [ParsedConstructorToConsDef tuple_cons_def : cons_defs] pre_def_symbols
 			= (type_defs, cons_defs, pre_def_symbols)
diff --git a/frontend/refmark.icl b/frontend/refmark.icl
index 0680d7c..c509dc7 100644
--- a/frontend/refmark.icl
+++ b/frontend/refmark.icl
@@ -748,8 +748,9 @@ where
 			empty_occurrence {fv_info_ptr} var_heap 
 				= var_heap <:= (fv_info_ptr, VI_Empty)
 
-		get_type (VI_Type atype _)		= atype
-		get_type (VI_FAType _ atype _)	= atype
+		get_type (VI_Type atype _)			= atype
+		get_type (VI_FAType _ atype _)		= atype
+		get_type (VI_FATypeC _ atype _ _)	= atype
 
 		make_shared_vars_non_unique vars fun_body coercion_env var_heap expr_heap error
 			= foldl make_shared_var_non_unique (coercion_env, var_heap, expr_heap, error) vars
@@ -779,6 +780,8 @@ where
 									 ===> ("make_shared_occurrence_non_unique", free_var, var_expr_ptr, sa_attr_nr)
 								-> (coercion_env, expr_heap, error)
 								-> (coercion_env, expr_heap, uniquenessErrorVar free_var fun_body " demanded attribute cannot be offered by shared object" error)
+						EI_FPContext _ var_expr_ptr
+							-> make_shared_occurrence_non_unique free_var var_expr_ptr (coercion_env, expr_heap, error)
 						_
 							-> abort ("make_shared_occurrence_non_unique" ===> ((free_var, var_expr_ptr) )) // <<- expr_info))
 	
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index fce13e6..1bca9d6 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -292,6 +292,7 @@ cNameLocationDependent :== True
 	,	pc_exi_vars		:: ![ATypeVar]
 	,	pc_arg_types	:: ![AType]
 	,	pc_args_strictness	:: !StrictnessList
+	,	pc_context		:: ![TypeContext]
 	,	pc_cons_prio	:: !Priority
 	,	pc_cons_pos		:: !Position
 	}
@@ -725,6 +726,7 @@ pIsSafe			:== True
 //::	VarInfo  =	VI_Empty | VI_Type !AType !(Optional CoercionPosition) | VI_FAType ![ATypeVar] !AType !(Optional CoercionPosition) |
 ::	VarInfo  =	VI_Empty | VI_Type !AType !VI_TypeInfo |
 				VI_FAType ![ATypeVar] !AType !VI_TypeInfo |
+				VI_FATypeC ![ATypeVar] !AType ![TypeContext] !VI_TypeInfo | VI_FPC |
 				VI_Occurrence !Occurrence | VI_UsedVar !Ident |
 				VI_Expression !Expression | VI_Variable !Ident !VarInfoPtr | VI_LiftedVariable !VarInfoPtr |
 				VI_Count !Int /* the reference count of a variable */ !Bool /* true if the variable is global, false otherwise */ |
@@ -737,6 +739,7 @@ pIsSafe			:== True
 				VI_RefFromArrayUpdateOfTupleElem2 !Int ![Selection] |
 				VI_FreeVar !Ident !VarInfoPtr !Int !AType | VI_BoundVar !AType | VI_LocalVar |
 				VI_ClassVar !Ident !VarInfoPtr !Int | /* to hold dictionary variables during overloading */
+				VI_EmptyConstructorClassVar |
 				VI_ForwardClassVar !VarInfoPtr | /* to hold the dictionary variable generated during overloading */
 				VI_Forward !BoundVar | VI_LetVar !LetVarInfo | VI_LetExpression !LetExpressionInfo |
 				VI_CaseOrStrictLetVar !VarInfoPtr | VI_StrictLetVar |
@@ -804,6 +807,10 @@ cNotVarNumber :== -1
 				| SK_NewTypeConstructor !GlobalIndex
 				| SK_Generic !(Global Index) !TypeKind
 				| SK_TypeCode
+				| SK_OverloadedConstructor !(Global Index)
+				| SK_TFACVar !ExprInfoPtr
+				| SK_VarContexts !(VarContexts TypeContext)
+				| SK_TypeCodeAndContexts !(VarContexts TypeContext)
 
 /*	Some auxiliary type definitions used during fusion. Actually, these definitions
 	should have been given in seperate module. Unfortunately, Clean's module system
@@ -849,9 +856,12 @@ cNotVarNumber :== -1
 		/* For handling overloading */
 
 					| EI_Overloaded !OverloadedCall 						/* initial, set by the type checker */
+					| EI_OverloadedWithVarContexts !OverloadedCallWithVarContexts /* initial, set by the type checker */
 					| EI_Instance 	!(Global DefinedSymbol) ![Expression]	/* intermedediate, used during resolving of overloading */ 
 					| EI_Selection 	![Selection] !VarInfoPtr ![Expression]	/* intermedediate, used during resolving of overloading */
 					| EI_Context 	![Expression]							/* intermedediate, used during resolving of overloading */
+					| EI_ContextWithVarContexts ![Expression] !(VarContexts DictionaryAndClassType) /* intermedediate, used during resolving of overloading */
+					| EI_FPContext	![Expression] !ExprInfoPtr				/* intermedediate, used during resolving of overloading */
 
 		/* For handling dynamics */
 
@@ -870,9 +880,11 @@ cNotVarNumber :== -1
 
 					| EI_TypeOfDynamic 			!TypeCodeExpression						/* Final */
 					| EI_TypeOfDynamicPattern 	![VarInfoPtr] !TypeCodeExpression		/* Final */
+					| EI_TypeOfDynamicWithContexts !TypeCodeExpression !(VarContexts DictionaryAndClassType)
 
 					| EI_TypeCode 		!TypeCodeExpression
 					| EI_TypeCodes 		![TypeCodeExpression]
+					| EI_TypeCodesWithContexts ![TypeCodeExpression] !(VarContexts DictionaryAndClassType)
 
 					| EI_Attribute !Int
 
@@ -882,6 +894,7 @@ cNotVarNumber :== -1
 					| EI_DictionaryType !Type
 					| EI_CaseType !CaseType
 					| EI_LetType ![AType]
+					| EI_CaseTypeWithContexts !CaseType ![(DefinedSymbol,[TypeContext])]
 					| EI_CaseTypeAndRefCounts !CaseType !RefCountsInCase
 					| EI_CaseTypeAndSplits !CaseType !SplitsInCase
 					| EI_LetTypeAndRefCounts ![AType] ![Int]
@@ -915,6 +928,21 @@ cNotVarNumber :== -1
 	,	oc_specials	:: ![Special]
 	}
 
+::	OverloadedCallWithVarContexts = 
+	{	ocvc_symbol       :: !SymbIdent
+	,	ocvc_context      :: ![TypeContext]
+	,	ocvc_var_contexts :: !VarContexts TypeContext
+	}
+
+::	DictionaryAndClassType =
+	{	dc_var			:: !VarInfoPtr
+	,	dc_class_type	:: !AType
+	}
+
+::	VarContexts type_contexts
+	= VarContext !Int /*arg_n*/ ![type_contexts] !AType !(VarContexts type_contexts)
+	| NoVarContexts
+
 /*
 	CaseType contains the type information needed to type the corresponding case construct:
 		ct_pattern_type : the type of the pattern
@@ -991,7 +1019,6 @@ cNotVarNumber :== -1
 ::	TempAttrId		:== Int
 ::	TempVarId		:== Int
 
-
 ::	Type	=	TA !TypeSymbIdent ![AType]
 			|	TAS !TypeSymbIdent ![AType] !StrictnessList
 			|	(-->) infixr 9 !AType !AType
@@ -1004,6 +1031,9 @@ cNotVarNumber :== -1
 
 			| 	GTV !TypeVar
 			| 	TV !TypeVar
+
+			|	TFAC ![ATypeVar] !Type ![TypeContext]	// Universally quantified function argument type with contexts
+
 			|	TempV !TempVarId				/* Auxiliary, used during type checking */
 			
 			|	TQV	TypeVar
@@ -1101,7 +1131,7 @@ cNotVarNumber :== -1
 					| TA_Anonymous | TA_None
 					| TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
 					| TA_MultiOfPropagatingConsVar // only filled in after type checking, semantically equal to TA_Multi
-							
+
 ::	AttributeVar =
 	{	av_ident			:: !Ident
 	,	av_info_ptr		:: !AttrVarInfoPtr
@@ -1312,6 +1342,8 @@ cIsNotStrict	:== False
 				| MatchExpr !(Global DefinedSymbol) !Expression
 				| IsConstructor !Expression !(Global DefinedSymbol) /*arity*/!Int !GlobalIndex !Ident !Position
 				| FreeVar FreeVar 
+				| DictionariesFunction ![(FreeVar,AType)] !Expression !AType
+
 				| Constant !SymbIdent !Int !Priority		/* auxiliary clause used during checking */
 				| ClassVariable !VarInfoPtr					/* auxiliary clause used during overloading */
 
@@ -1522,7 +1554,7 @@ ParsedSelectorToSelectorDef sd_type_index ps :==
 ParsedConstructorToConsDef pc :==
 	{	cons_ident = pc.pc_cons_ident, cons_pos = pc.pc_cons_pos, cons_priority = pc.pc_cons_prio, cons_number = NoIndex, cons_type_index = NoIndex,
 		cons_type = { st_vars = [], st_args = pc.pc_arg_types, st_args_strictness=pc.pc_args_strictness, st_result = MakeAttributedType TE, 
-				  st_arity = pc.pc_cons_arity, st_context = [], st_attr_env = [], st_attr_vars = []},
+				  st_arity = pc.pc_cons_arity, st_context = pc.pc_context, st_attr_env = [], st_attr_vars = []},
 		cons_exi_vars = pc.pc_exi_vars, cons_type_ptr = nilPtr }
 
 ParsedInstanceToClassInstance pi members member_types :==
diff --git a/frontend/syntax.icl b/frontend/syntax.icl
index 1f7c5c6..fa89199 100644
--- a/frontend/syntax.icl
+++ b/frontend/syntax.icl
@@ -196,6 +196,8 @@ where
 		= file <<< "(->) " <<< t	
 	(<<<) file (TFA vars types)
 		= file <<< "A." <<< vars <<< ':' <<< types
+	(<<<) file (TFAC vars types contexts)
+		= file <<< "A." <<< vars <<< ':' <<< types <<< " | " <<< contexts
 	(<<<) file (TQV varid)
 		= file <<< "E." <<< varid
 	(<<<) file (TempQV tv_number)
@@ -403,6 +405,8 @@ where
 
 	(<<<) file (FailExpr _) = file <<< "** FAIL **"
 	(<<<) file (TypeSignature array_kind expr) = file <<< "TypeSignature " <<< '(' <<< expr <<< ')'
+	(<<<) file (DictionariesFunction dictionaries expr expr_type)
+		= file <<< "DictionariesFunction " <<< dictionaries <<< expr <<< expr_type
 	(<<<) file expr         				= abort ("<<< (Expression)" )
 	
 instance <<< LetBind
@@ -573,11 +577,13 @@ where
 instance <<< FunCall
 where
 	(<<<) file (FunCall fc_index fc_level)
-			= file <<< fc_index <<< '.' <<< fc_level
+		= file <<< fc_index <<< '.' <<< fc_level
 	(<<<) file (MacroCall module_index fc_index fc_level)
-			= file <<< "MacroCall "<<< module_index <<<" "<<<fc_index <<< '.' <<< fc_level
+		= file <<< "MacroCall "<<< module_index <<<" "<<<fc_index <<< '.' <<< fc_level
 	(<<<) file (DclFunCall module_index fc_index)
-			= file <<< "DclFunCall "<<< module_index <<<" "<<<fc_index
+		= file <<< "DclFunCall "<<< module_index <<<" "<<<fc_index
+	(<<<) file (GeneratedFunCall fc_index _)
+		= file <<< "GeneratedFunCall "<<< fc_index
 
 instance <<< FreeVar
 where
diff --git a/frontend/trans.icl b/frontend/trans.icl
index 1e7b97d..3774926 100644
--- a/frontend/trans.icl
+++ b/frontend/trans.icl
@@ -211,7 +211,6 @@ where
 		  (let_lazy_binds, ti) = transform let_lazy_binds ro ti
 		  (let_expr, ti) = transform let_expr ro ti
 		  lad = { lad & let_lazy_binds = let_lazy_binds, let_strict_binds = let_strict_binds, let_expr = let_expr}
-//		  ti = check_type_info lad ti
 		= (Let lad, ti)
 	  where
 		store_type_info_of_bindings_in_heap {let_strict_binds, let_lazy_binds,let_info_ptr} ti
@@ -221,12 +220,7 @@ where
 			= {ti & ti_symbol_heap = ti_symbol_heap, ti_var_heap = ti_var_heap}
 		store_type_info_let_bind (var_type, {lb_dst={fv_info_ptr}}) var_heap
 			= setExtendedVarInfo fv_info_ptr (EVI_VarType var_type) var_heap
-/*
-		check_type_info {let_strict_binds,let_lazy_binds,let_info_ptr} ti
-			# (EI_LetType var_types, ti_symbol_heap) = readExprInfo let_info_ptr ti.ti_symbol_heap
-			= { ti & ti_symbol_heap = ti_symbol_heap }
-				//  ---> ("check_type_info_of_bindings_in_heap",let_strict_binds,let_lazy_binds,var_types)
-*/
+
 	transform (Case kees) ro ti
 		# ti = store_type_info_of_patterns_in_heap kees ti
 		= transformCase kees ro ti
@@ -292,6 +286,9 @@ where
 	transform (DynamicExpr dynamic_expr) ro ti
 		# (dynamic_expr, ti) = transform dynamic_expr ro ti
 		= (DynamicExpr dynamic_expr, ti)
+	transform (DictionariesFunction dictionaries expr expr_type) ro ti
+		# (expr,ti) = transform expr ro ti
+		= (DictionariesFunction dictionaries expr expr_type,ti)
 	transform expr ro ti
 		= (expr, ti)
 
@@ -1671,7 +1668,6 @@ generateFunction app_symb fd=:{fun_body = TransformedBody {tb_args,tb_rhs},fun_i
 										f2b { fv_ident, fv_info_ptr }
 											= Var { var_ident = fv_ident, var_info_ptr = fv_info_ptr, var_expr_ptr = nilPtr }
 								-> add_args_to_fun_body act_args fresh_result_type tb_rhs ro ti
-
 	  (new_fun_rhs, ti)
 			= transform tb_rhs ro ti
 	  new_fd
@@ -3514,8 +3510,6 @@ foldrExprSt f expr st :== foldr_expr_st expr st
 		= f lad st
 	foldr_expr_st sel=:(Selection a expr b) st
 		= f sel (foldr_expr_st expr st)
-		
-	// AA:	
 	foldr_expr_st expr=:(BasicExpr _) st 
 		= f expr st
 
@@ -4341,6 +4335,8 @@ where
 	strip :: AType [TypeVar] -> (AType,[TypeVar])
 	strip atype=:{at_type = TFA vars type} tvs
 		= ({atype & at_type = type}, map (\{atv_variable}->atv_variable) vars ++ tvs)
+	strip atype=:{at_type = TFAC vars type contexts} tvs
+		= ({atype & at_type = type}, map (\{atv_variable}->atv_variable) vars ++ tvs)
 	strip atype tvs
 		= (atype,tvs)
 
diff --git a/frontend/transform.icl b/frontend/transform.icl
index c076ecc..5dc725e 100644
--- a/frontend/transform.icl
+++ b/frontend/transform.icl
@@ -1722,6 +1722,11 @@ where
 	clearCount {fv_info_ptr} locality var_heap
 		= var_heap <:= (fv_info_ptr, VI_Count 0 locality)
 
+instance clearCount (FreeVar,a)
+where
+	clearCount ({fv_info_ptr},_) locality var_heap
+		= var_heap <:= (fv_info_ptr, VI_Count 0 locality)
+
 /*
 	In 'collectVariables' all local variables are collected. Moreover the reference counts
 	of the local as well as of the global variables are determined. Aliases and unreachable 
@@ -2007,6 +2012,16 @@ where
 	collectVariables (TypeSignature type_function expr) free_vars dynamics cos
 		# (expr, free_vars, dynamics, cos) = collectVariables expr free_vars dynamics cos
 		= (TypeSignature type_function expr, free_vars, dynamics, cos);
+	collectVariables (DictionariesFunction dictionaries expr expr_type) free_vars dynamics cos
+		# cos = {cos & cos_var_heap = clearCount dictionaries cIsALocalVar cos.cos_var_heap}
+		  (expr, free_vars, dynamics, cos) = collectVariables expr free_vars dynamics cos
+		  (dictionaries, var_heap) = mapSt retrieve_ref_count dictionaries cos.cos_var_heap
+		  cos = {cos & cos_var_heap = var_heap}
+		= (DictionariesFunction dictionaries expr expr_type, free_vars, dynamics, cos)
+	where
+		retrieve_ref_count (fv,a_type) var_heap
+			# (fv,var_heap) = retrieveRefCount fv var_heap
+			= ((fv,a_type),var_heap)
 	collectVariables expr free_vars dynamics cos
 		= (expr, free_vars, dynamics, cos)
 
diff --git a/frontend/type.icl b/frontend/type.icl
index 1cc292b..12317a0 100644
--- a/frontend/type.icl
+++ b/frontend/type.icl
@@ -1,6 +1,6 @@
 implementation module type
 
-import StdEnv, compare_types
+import StdEnv,StdOverloadedList,compare_types
 import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor
 import genericsupport
 
@@ -119,6 +119,17 @@ where
 		| changed
 			= (changed, TFA vars type, subst)
 			= (False, tfa_type, subst)
+	arraySubst tfac_type=:(TFAC vars type contexts) subst
+		# (changed, new_type, subst) = arraySubst type subst
+		| changed
+			# (changed,new_contexts,subst) = arraySubst contexts subst
+			| changed
+				= (True, TFAC vars new_type new_contexts, subst)
+				= (True, TFAC vars new_type contexts, subst)
+			# (changed,new_contexts,subst) = arraySubst contexts subst
+			| changed
+				= (True, TFAC vars type new_contexts, subst)
+				= (False, tfac_type, subst)
 
 	arraySubst type subst
 		= (False, type, subst)
@@ -156,6 +167,34 @@ where
 			= (True,{ tc & tc_types = tc_types}, subst)
 			= (False, tc, subst)
 
+instance arraySubst (VarContexts TypeContext)
+where
+	arraySubst var_context=:(VarContext arg_n context arg_atype var_contexts) subst
+		# (changed,new_context,subst) = arraySubst context subst
+		| changed
+			# (changed,new_arg_atype,subst) = arraySubst arg_atype subst
+			| changed
+				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
+				| changed
+					= (True,VarContext arg_n new_context new_arg_atype new_var_contexts,subst)
+					= (True,VarContext arg_n new_context new_arg_atype var_contexts,subst)
+				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
+				| changed
+					= (True,VarContext arg_n new_context arg_atype new_var_contexts,subst)
+					= (True,VarContext arg_n new_context arg_atype var_contexts,subst)
+			# (changed,new_arg_atype,subst) = arraySubst arg_atype subst
+			| changed			
+				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
+				| changed
+					= (True,VarContext arg_n context new_arg_atype new_var_contexts,subst)
+					= (True,VarContext arg_n context new_arg_atype var_contexts,subst)
+				# (changed,new_var_contexts,subst) = arraySubst var_contexts subst
+				| changed
+					= (True,VarContext arg_n context arg_atype new_var_contexts,subst)
+					= (False,var_context,subst)
+	arraySubst NoVarContexts subst
+		= (False,NoVarContexts,subst)
+
 instance arraySubst CaseType
 where
 	arraySubst ct=:{ct_pattern_type, ct_result_type, ct_cons_types} subst
@@ -673,6 +712,8 @@ where
 		= (TArrow1 arg_type, type_heaps)
 	freshCopy (TFA vars type) type_heaps
 		= freshCopyOfTFAType vars type type_heaps
+	freshCopy (TFAC vars type context) type_heaps
+		= freshCopyOfTFACType vars type context type_heaps
 	freshCopy type type_heaps
 		= (type, type_heaps)
 
@@ -682,6 +723,13 @@ freshCopyOfTFAType vars type type_heaps
 	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
 	= (TFA fresh_vars type, type_heaps)
 
+freshCopyOfTFACType vars type contexts type_heaps
+	# (fresh_vars, type_heaps) = bind_TFA_vars_and_attrs vars type_heaps
+	  (type, type_heaps) = freshCopy type type_heaps
+	  (contexts, type_heaps) = freshTypeContexts_no_fresh_context_vars contexts type_heaps
+	  type_heaps = clear_binding_of_TFA_vars_and_attrs fresh_vars type_heaps
+	= (TFAC fresh_vars type contexts, type_heaps)
+
 bind_TFA_vars_and_attrs vars type_heaps
 	= foldSt bind_var_and_attr vars ([], type_heaps)
 	where
@@ -719,7 +767,7 @@ where
 		# (exi_attr_vars, attr_store, th_attrs) = fresh_existential_attribute atv_attribute (exi_attr_vars, attr_store, th_attrs)
 		= (exi_attr_vars, var_store, attr_store, { type_heaps & th_vars = th_vars, th_attrs = th_attrs })
 
-	fresh_existential_attribute (TA_Var {av_ident,av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
+	fresh_existential_attribute (TA_Var {av_info_ptr}) (exi_attr_vars, attr_store, attr_heap)
 		= ([ attr_store : exi_attr_vars ], inc attr_store, attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
 	fresh_existential_attribute attr state
 		= state
@@ -758,7 +806,8 @@ fresh_environment inequalities attr_env attr_heap
 		is_new_ineqality dem_attr_var off_attr_var []
 			= True
 
-freshAlgebraicType :: !GlobalIndex ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!TypeRhs,!*TypeState)
+freshAlgebraicType :: !GlobalIndex ![AlgebraicPattern] !{#CommonDefs} !*TypeState
+					-> (![[AType]],!AType,![AttrCoercion],[(DefinedSymbol,[TypeContext])],!TypeRhs,!*TypeState)
 freshAlgebraicType {gi_module,gi_index} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_exis_variables}
 	# {td_rhs,td_args,td_attrs}		= common_defs.[gi_module].com_type_defs.[gi_index]
 	# (th_vars, ts_var_store)		= fresh_type_variables td_args (ts_type_heaps.th_vars, ts_var_store)
@@ -766,7 +815,7 @@ freshAlgebraicType {gi_module,gi_index} patterns common_defs ts=:{ts_var_store,t
 	  ts_type_heaps					= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
 	  (cons_types, alg_type, attr_env, constructor_contexts, ts_var_store, ts_attr_store, ts_type_heaps, ts_exis_variables)
 	  		= fresh_symbol_types patterns common_defs td_attrs td_args ts_var_store ts_attr_store ts_type_heaps ts_exis_variables
-	= (cons_types, alg_type, attr_env, td_rhs,
+	= (cons_types, alg_type, attr_env, constructor_contexts, td_rhs,
 			{ ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = ts_type_heaps, ts_exis_variables = ts_exis_variables })
 where
 	fresh_symbol_types [{ap_symbol={glob_object,glob_module},ap_expr}] common_defs td_attrs td_args var_store attr_store type_heaps all_exis_variables
@@ -901,13 +950,14 @@ freshSymbolType is_appl fresh_context_vars {st_vars,st_args,st_result,st_context
 	  (th_attrs, ts_attr_store)	= fresh_attributes st_attr_vars (ts_type_heaps.th_attrs, ts_attr_store)
 	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
 	  type_heaps 				= {ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs}
-	  (tst_args, (ts_var_store,ts_attr_store,ts_exis_variables,type_heaps))
-								= fresh_arg_types is_appl st_args ts_var_store ts_attr_store ts_exis_variables type_heaps
+	  (tst_args,var_contexts,ts_var_store,ts_attr_store,ts_exis_variables,type_heaps,ts_var_heap)
+								= fresh_arg_types is_appl st_args ts_var_store ts_attr_store ts_exis_variables type_heaps ts_var_heap
 	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
 	  (tst_context, (type_heaps, ts_var_heap)) = freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
 	  type_heaps = {type_heaps & th_attrs = clear_attributes st_attr_vars type_heaps.th_attrs}
+	  // to do collect cons variables in contexts in TFAC of arguments
 	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context []
-	  tst = {tst_args=tst_args, tst_result=tst_result, tst_context=tst_context, tst_attr_env=attr_env,
+	  tst = {tst_args=tst_args, tst_result=tst_result, tst_context=tst_context, tst_var_contexts=var_contexts, tst_attr_env=attr_env,
 			 tst_arity=st_arity, tst_lifted=0}
 	= (tst, {ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps, ts_var_heap = ts_var_heap,
 	   			  ts_cons_variables = cons_variables ++ ts_cons_variables, ts_exis_variables = ts_exis_variables})
@@ -957,21 +1007,38 @@ freshSymbolType is_appl fresh_context_vars {st_vars,st_args,st_result,st_context
 				= vars
 				= [var_id : add_variable new_var_id var_ids]
 
-		fresh_arg_types No arg_types var_store attr_store exis_variables type_heaps
+		fresh_arg_types No arg_types var_store attr_store exis_variables type_heaps var_heap
 			# (arg_types, type_heaps) = mapSt fresh_arg_type arg_types type_heaps
-			= (arg_types, (var_store, attr_store, exis_variables, type_heaps))
+			= (arg_types,NoVarContexts,var_store, attr_store, exis_variables, type_heaps, var_heap)
 		where
 			fresh_arg_type at=:{at_attribute, at_type = TFA vars type} type_heaps
 				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
 				  (at_type, type_heaps)			= freshCopyOfTFAType vars type {type_heaps & th_attrs = th_attrs}
 				= ({at & at_attribute = fresh_attribute, at_type = at_type}, type_heaps)
+			fresh_arg_type at=:{at_attribute, at_type = TFAC vars type contexts} type_heaps
+				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
+				  (at_type, type_heaps)			= freshCopyOfTFACType vars type contexts {type_heaps & th_attrs = th_attrs}
+				= ({at & at_attribute = fresh_attribute, at_type = at_type}, type_heaps)
 			fresh_arg_type at type_heaps
 				= freshCopy at type_heaps
 
-		fresh_arg_types (Yes pos) arg_types var_store attr_store exis_variables type_heaps
-			= mapSt (fresh_arg_type pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
+		fresh_arg_types (Yes pos) arg_types var_store attr_store exis_variables type_heaps var_heap
+			= fresh_arg_types pos arg_types NoVarContexts 0 var_store attr_store exis_variables type_heaps var_heap
 		where
-			fresh_arg_type pos at=:{at_attribute, at_type = TFA vars type} (var_store, attr_store, exis_variables, type_heaps)
+			fresh_arg_types :: p ![AType]  (VarContexts TypeContext) !Int  Int  Int  [(p,[Int])]  *TypeHeaps  *VarHeap
+							-> *(![AType],!(VarContexts TypeContext),     !Int,!Int,![(p,[Int])],!*TypeHeaps,!*VarHeap)
+			fresh_arg_types pos [arg_type:arg_types] var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
+				# (arg_types,var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+					= fresh_arg_types pos arg_types var_contexts (arg_n+1) var_store attr_store exis_variables type_heaps var_heap
+				# (arg_type,var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+					= fresh_arg_type pos arg_type var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
+				= ([arg_type:arg_types],var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+			fresh_arg_types pos [] var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
+				= ([],var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+
+			fresh_arg_type :: p !AType  (VarContexts TypeContext) !Int  Int  Int  [(p,[Int])]  *TypeHeaps  *VarHeap
+						   -> *(!AType,!(VarContexts TypeContext),     !Int,!Int,![(p,[Int])],!*TypeHeaps,!*VarHeap)
+			fresh_arg_type pos at=:{at_attribute, at_type = TFA vars type} var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
 				# (fresh_attribute, th_attrs) = freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
 				  (var_store, attr_store, new_exis_variables, bound_attr_vars, type_heaps)
 						= fresh_vars_and_attrs vars var_store attr_store {type_heaps & th_attrs = th_attrs}
@@ -980,10 +1047,22 @@ freshSymbolType is_appl fresh_context_vars {st_vars,st_args,st_result,st_context
 											 th_attrs = clear_binding_of_attr_vars bound_attr_vars type_heaps.th_attrs}
 				  exis_variables = addToExistentialVariables pos new_exis_variables exis_variables
 				  at = {at & at_attribute = fresh_attribute, at_type = fresh_type}
-				= (at, (var_store, attr_store, exis_variables, type_heaps))
-			fresh_arg_type _ at (var_store, attr_store, exis_variables, type_heaps)
+				= (at,var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+			fresh_arg_type pos at=:{at_attribute, at_type = TFAC vars type contexts} var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
+				# (fresh_attribute, th_attrs) = freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
+				  (var_store, attr_store, new_exis_variables, bound_attr_vars, type_heaps)
+						= fresh_vars_and_attrs vars var_store attr_store {type_heaps & th_attrs = th_attrs}
+				  (fresh_type, type_heaps) = freshCopy type type_heaps
+				  (fresh_context, (type_heaps,var_heap)) = freshTypeContexts fresh_context_vars contexts (type_heaps,var_heap)
+				  type_heaps = {type_heaps & th_vars = clear_binding_of_type_vars vars type_heaps.th_vars,
+				  							 th_attrs = clear_binding_of_attr_vars bound_attr_vars type_heaps.th_attrs}
+				  exis_variables = addToExistentialVariables pos new_exis_variables exis_variables
+				  at = {at & at_attribute = fresh_attribute, at_type = fresh_type}
+				  var_contexts = VarContext arg_n fresh_context at var_contexts
+				= (at,var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
+			fresh_arg_type _ at var_contexts arg_n var_store attr_store exis_variables type_heaps var_heap
 				# (fresh_at,type_heaps) = freshCopy at type_heaps
-				= (fresh_at,(var_store,attr_store,exis_variables,type_heaps))
+				= (fresh_at,var_contexts,var_store,attr_store,exis_variables,type_heaps,var_heap)
 
 			fresh_vars_and_attrs vars var_store attr_store type_heaps
 				= foldSt fresh_var_and_attr vars (var_store, attr_store, [], [], type_heaps)
@@ -1439,7 +1518,7 @@ getSymbolType pos ti=:{ti_common_defs} symbol=:{symb_ident, symb_kind = SK_Gener
 		No
 			# empty_atype={at_type=TE,at_attribute=TA_Multi}
 			  t_args=[empty_atype \\ _ <- [1..n_app_args]]
-			  empty_tst	= {tst_args=t_args, tst_arity=n_app_args, tst_lifted=0, tst_result=empty_atype, tst_context=[], tst_attr_env=[]}
+			  empty_tst	= {tst_args=t_args, tst_arity=n_app_args, tst_lifted=0, tst_result=empty_atype, tst_context=[], tst_var_contexts=NoVarContexts, tst_attr_env=[]}
 			  ts_error = checkError ("no generic instances of " +++ toString symb_ident +++ " for kind") kind ts.ts_error
 			-> (empty_tst, [], {ts & ts_error = ts_error})	
 		Yes member_glob
@@ -1460,6 +1539,21 @@ where
 		  		  (fresh_type, ts_type_heaps) = freshCopy type ts.ts_type_heaps
 				  ts_type_heaps = clear_vars_and_attrs vars ts_type_heaps
 				-> (fresh_type, Yes var_expr_ptr, (reqs, {ts & ts_type_heaps = ts_type_heaps}))
+			VI_FATypeC vars type contexts _
+				# ts = bind_vars_and_attrs vars ts
+		  		  (fresh_type, ts_type_heaps) = freshCopy type ts.ts_type_heaps
+				  (contexts,(ts_type_heaps,ts_var_heap)) = freshTypeContexts True contexts (ts_type_heaps,ts.ts_var_heap)
+				  ts_type_heaps = clear_vars_and_attrs vars ts_type_heaps
+ 
+				  {ts_expr_heap} = ts
+		  		  (new_var_expr_ptr,ts_expr_heap) = newPtr EI_Empty ts_expr_heap
+
+				  reqs = {reqs & req_overloaded_calls = [var_expr_ptr : reqs.req_overloaded_calls]}
+				  symbol = {symb_ident=var_ident,symb_kind=SK_TFACVar new_var_expr_ptr}
+				  ts_expr_heap = ts_expr_heap <:= (var_expr_ptr,EI_Overloaded {oc_symbol=symbol,oc_context=contexts,oc_specials=[]})
+				  ts = {ts & ts_type_heaps=ts_type_heaps,ts_expr_heap=ts_expr_heap,ts_var_heap=ts_var_heap}
+
+				-> (fresh_type, Yes new_var_expr_ptr, (reqs, ts))
 		  	_
 				-> abort "requirements BoundVar " // ---> (var_ident <<- var_info))
 		where
@@ -1492,14 +1586,19 @@ where
 instance requirements App
 where
 	requirements ti app=:{app_symb,app_args,app_info_ptr} (reqs=:{req_attr_coercions}, ts)
-		# ({tst_attr_env,tst_args,tst_result,tst_context}, specials, ts)
+		# ({tst_attr_env,tst_args,tst_result,tst_context,tst_var_contexts}, specials, ts)
 			= getSymbolType (CP_Expression (App app)) ti app_symb (length app_args) ts
 	  	  reqs = {reqs & req_attr_coercions = tst_attr_env ++ req_attr_coercions}
 		  (n_lifted_arguments,fun_args,ts) = get_n_lifted_arguments app_symb.symb_kind ti.ti_main_dcl_module_n ts
 		  (reqs, ts) = requirements_of_lifted_and_normal_args ti app_symb (1-n_lifted_arguments) fun_args app_args tst_args (reqs, ts)
-		| isEmpty tst_context
-			= (tst_result, No, (reqs, ts))
-			# app_info = EI_Overloaded {oc_symbol = app_symb, oc_context = tst_context, oc_specials = specials}
+		| case tst_var_contexts of NoVarContexts -> True; _ -> False
+			| isEmpty tst_context
+				= (tst_result, No, (reqs, ts))
+				# app_info = EI_Overloaded {oc_symbol=app_symb, oc_context=tst_context, oc_specials=specials}
+				= (tst_result, No, ({reqs & req_overloaded_calls = [app_info_ptr : reqs.req_overloaded_calls]}, 
+									{ts & ts_expr_heap = ts.ts_expr_heap <:= (app_info_ptr,app_info)}))
+			// special not yet implemented
+			# app_info = EI_OverloadedWithVarContexts {ocvc_symbol=app_symb, ocvc_context=tst_context, ocvc_var_contexts=tst_var_contexts}
 			= (tst_result, No, ({reqs & req_overloaded_calls = [app_info_ptr : reqs.req_overloaded_calls]}, 
 								{ts & ts_expr_heap = ts.ts_expr_heap <:= (app_info_ptr,app_info)}))
 	where
@@ -1541,30 +1640,37 @@ where
 	requirements ti {case_expr,case_guards,case_default,case_info_ptr,case_default_pos} reqs_ts
 		# (expr_type, opt_expr_ptr, (reqs, ts)) = requirements ti case_expr reqs_ts
 		  (fresh_v, ts) = freshAttributedVariable ts
-		  (cons_types, reqs_ts) = requirements_of_guarded_expressions case_guards ti case_expr expr_type opt_expr_ptr fresh_v reqs ts
+		  (case_info, reqs_ts) = requirements_of_guarded_expressions case_guards case_expr case_info_ptr ti expr_type opt_expr_ptr fresh_v reqs ts
 		  (reqs, ts) = requirements_of_default ti case_default case_default_pos fresh_v reqs_ts
-		  ts = {ts & ts_expr_heap = ts.ts_expr_heap <:= (case_info_ptr, EI_CaseType {ct_pattern_type = expr_type, ct_result_type = fresh_v, ct_cons_types = cons_types})}
+		  ts = {ts & ts_expr_heap = ts.ts_expr_heap <:= (case_info_ptr, case_info)}
 		= (fresh_v, No, ({reqs & req_case_and_let_exprs = [case_info_ptr : reqs.req_case_and_let_exprs]}, ts))
 	where
-		requirements_of_guarded_expressions (AlgebraicPatterns alg_type patterns) ti=:{ti_common_defs} match_expr pattern_type opt_pattern_ptr goal_type reqs ts
-			# (cons_types, result_type, new_attr_env,td_rhs,ts) = freshAlgebraicType alg_type patterns ti_common_defs ts
+		requirements_of_guarded_expressions (AlgebraicPatterns alg_type patterns) match_expr case_info_ptr ti=:{ti_common_defs} pattern_type opt_pattern_ptr goal_type reqs ts
+			# (cons_types, result_type, new_attr_env,constructor_contexts,td_rhs,ts) = freshAlgebraicType alg_type patterns ti_common_defs ts
 			  ts_var_heap = update_case_variable match_expr td_rhs cons_types alg_type ts.ts_var_heap
 			  (used_cons_types, (reqs, ts)) = requirements_of_algebraic_patterns ti patterns cons_types goal_type [] (reqs, {ts & ts_var_heap = ts_var_heap})
 			  ts_expr_heap = storeAttribute opt_pattern_ptr result_type.at_attribute ts.ts_expr_heap
 			  (position, ts_var_heap) = getPositionOfExpr match_expr ts.ts_var_heap
 			  reqs = {reqs & req_type_coercions = [{tc_demanded = result_type,tc_offered = pattern_type, tc_position = position, tc_coercible = True} : reqs.req_type_coercions],
 							 req_attr_coercions = new_attr_env ++ reqs.req_attr_coercions}
-			= (reverse used_cons_types, (reqs, {ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap}))
-
-		requirements_of_guarded_expressions (BasicPatterns bas_type patterns) ti match_expr pattern_type opt_pattern_ptr goal_type reqs ts
+			| isEmpty constructor_contexts
+				# case_info = EI_CaseType {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = reverse used_cons_types}
+				= (case_info,  (reqs, {ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap}))
+				# (constructor_contexts,ts_var_heap) = create_fresh_context_vars constructor_contexts ts_var_heap
+				  case_info = EI_CaseTypeWithContexts {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = reverse used_cons_types} constructor_contexts
+				  reqs = {reqs & req_overloaded_calls = [case_info_ptr : reqs.req_overloaded_calls]}
+				= (case_info,  (reqs, {ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap}))
+
+		requirements_of_guarded_expressions (BasicPatterns bas_type patterns) match_expr case_info_ptr ti pattern_type opt_pattern_ptr goal_type reqs ts
 			# (attr_bas_type, ts) = attributedBasicType bas_type ts
 			  (reqs, ts) = requirements_of_basic_patterns ti patterns goal_type (reqs, ts)
 			  ts_expr_heap = storeAttribute opt_pattern_ptr attr_bas_type.at_attribute ts.ts_expr_heap
 			  reqs = {reqs & req_type_coercions = [{tc_demanded = attr_bas_type,tc_offered = pattern_type, tc_position = CP_Expression match_expr, tc_coercible = True} :
 							 reqs.req_type_coercions]}
-			= ([], (reqs, {ts & ts_expr_heap = ts_expr_heap}))
+			  case_info = EI_CaseType {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = []}
+			= (case_info, (reqs, {ts & ts_expr_heap = ts_expr_heap}))
 
-		requirements_of_guarded_expressions (OverloadedListPatterns alg_type decons_expr=:(App {app_symb,app_info_ptr}) patterns) ti=:{ti_common_defs,ti_functions} match_expr pattern_type opt_pattern_ptr goal_type reqs ts
+		requirements_of_guarded_expressions (OverloadedListPatterns alg_type decons_expr=:(App {app_symb,app_info_ptr}) patterns) match_expr case_info_ptr ti=:{ti_common_defs,ti_functions} pattern_type opt_pattern_ptr goal_type reqs ts
 			# (position, ts_var_heap) = getPositionOfExpr match_expr ts.ts_var_heap
 			# ts = {ts & ts_var_heap = ts_var_heap}
 			# (cons_types, result_type, context, new_attr_env, ts) = freshOverloadedListType alg_type position patterns ti_common_defs ti_functions ts
@@ -1574,25 +1680,28 @@ where
 			  ts_expr_heap = writePtr app_info_ptr (EI_Overloaded {oc_symbol = app_symb, oc_context = context, oc_specials = []/*specials*/ }) ts_expr_heap			  
 			  reqs = {reqs & req_type_coercions = type_coercions,req_attr_coercions = new_attr_env ++ reqs.req_attr_coercions,
 							 req_overloaded_calls = [app_info_ptr : reqs.req_overloaded_calls]}
-			= (reverse used_cons_types,(reqs,{ts & ts_expr_heap = ts_expr_heap}))
+			  case_info = EI_CaseType {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = reverse used_cons_types}
+			= (case_info,(reqs,{ts & ts_expr_heap = ts_expr_heap}))
 
-		requirements_of_guarded_expressions (NewTypePatterns alg_type patterns) ti=:{ti_common_defs} match_expr pattern_type opt_pattern_ptr goal_type reqs ts
-			# (cons_types, result_type, new_attr_env,td_rhs,ts) = freshAlgebraicType alg_type patterns ti_common_defs ts
+		requirements_of_guarded_expressions (NewTypePatterns alg_type patterns) match_expr case_info_ptr ti=:{ti_common_defs} pattern_type opt_pattern_ptr goal_type reqs ts
+			# (cons_types, result_type, new_attr_env,constructor_contexts,td_rhs,ts) = freshAlgebraicType alg_type patterns ti_common_defs ts
 			  ts_var_heap = update_case_variable match_expr td_rhs cons_types alg_type ts.ts_var_heap
 			  (used_cons_types, (reqs, ts)) = requirements_of_algebraic_patterns ti patterns cons_types goal_type [] (reqs, { ts & ts_var_heap = ts_var_heap } )
 			  ts_expr_heap = storeAttribute opt_pattern_ptr result_type.at_attribute ts.ts_expr_heap
 			  (position, ts_var_heap) = getPositionOfExpr match_expr ts.ts_var_heap
 			  reqs = {reqs & req_type_coercions = [{tc_demanded = result_type,tc_offered = pattern_type, tc_position = position, tc_coercible = True} : reqs.req_type_coercions],
 							 req_attr_coercions = new_attr_env ++ reqs.req_attr_coercions}
-			= (reverse used_cons_types,(reqs,{ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap}))
+			  case_info = EI_CaseType {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = reverse used_cons_types}
+			= (case_info,  (reqs, { ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap }))
 
-		requirements_of_guarded_expressions (DynamicPatterns dynamic_patterns) ti match_expr pattern_type opt_pattern_ptr goal_type reqs ts
+		requirements_of_guarded_expressions (DynamicPatterns dynamic_patterns) match_expr case_info_ptr ti pattern_type opt_pattern_ptr goal_type reqs ts
 			# dyn_type = { at_type = TB BT_Dynamic, at_attribute = TA_Multi }
 			  (used_dyn_types, (reqs, ts)) = requirements_of_dynamic_patterns ti goal_type dynamic_patterns [] (reqs,ts)
 			  ts_expr_heap = storeAttribute opt_pattern_ptr TA_Multi ts.ts_expr_heap
 			  reqs = {reqs & req_type_coercions = [{tc_demanded = dyn_type, tc_offered = pattern_type, tc_position = CP_Expression match_expr, tc_coercible = True} :
 							 reqs.req_type_coercions]}
-			= (reverse used_dyn_types, (reqs, {ts & ts_expr_heap = ts_expr_heap}))
+			  case_info = EI_CaseType {ct_pattern_type = pattern_type, ct_result_type = goal_type, ct_cons_types = reverse used_dyn_types}
+			= (case_info, (reqs, { ts & ts_expr_heap = ts_expr_heap }))
 
 		requirements_of_algebraic_patterns ti [] cons_types goal_type used_cons_types reqs_ts
 			= (used_cons_types, reqs_ts)
@@ -1939,7 +2048,7 @@ where
 		attributedBasicType {box=type} ts=:{ts_attr_store}
 			= ({ at_attribute = TA_TempVar ts_attr_store, at_type = type}, {ts & ts_attr_store = inc ts_attr_store})
 
-	requirements ti (MatchExpr {glob_object={ds_arity, ds_index},glob_module} expr) reqs_ts=:(reqs, ts)
+	requirements ti (MatchExpr {glob_object={ds_arity,ds_index,ds_ident},glob_module} expr) reqs_ts=:(reqs, ts)
 		| glob_module==cPredefinedModuleIndex
 			&& (let
 					pd_cons_index=ds_index+FirstConstructorPredefinedSymbolIndex
@@ -1948,6 +2057,9 @@ where
 			= requirements ti expr reqs_ts
 			# cp = CP_Expression expr
 			  ({tst_result,tst_args,tst_attr_env}, ts) = standardLhsConstructorType cp ds_index glob_module ti ts	
+			  ts = if (Any is_TFAC tst_args)
+					{ts & ts_error = checkError ds_ident "selection not allowed for constructor with universally quantified context" ts.ts_error}
+					ts
 			  (e_type, opt_expr_ptr, (reqs, ts)) = requirements ti expr (reqs, ts)
 			  reqs = { reqs & req_attr_coercions =  tst_attr_env ++ reqs.req_attr_coercions,
 			  				  req_type_coercions = [{ tc_demanded = tst_result, tc_offered = e_type, tc_position = cp, tc_coercible = True } : reqs.req_type_coercions ] }
@@ -1956,6 +2068,9 @@ where
 				# tuple_type = MakeTypeSymbIdent { glob_object = PD_Arity2TupleTypeIndex+(ds_arity-2), glob_module = cPredefinedModuleIndex } predefined_idents.[PD_Arity2TupleType+(ds_arity-2)] ds_arity
 				= ({ at_type = TA tuple_type tst_args, at_attribute = TA_Unique }, No, (reqs, ts))
 				= ( hd tst_args, No, (reqs, ts))
+		where
+			is_TFAC {at_type=TFAC _ _ _} = True
+			is_TFAC _ = False
 
 	requirements ti (IsConstructor expr {glob_object={ds_arity,ds_index,ds_ident},glob_module} _ _ _ _) (reqs,ts)
 		# cp = CP_Expression expr
@@ -2104,6 +2219,8 @@ where
 
 addToBase info_ptr atype=:{at_type = TFA atvs type} optional_position ts_var_heap 
 	= ts_var_heap  <:= (info_ptr, VI_FAType atvs {atype & at_type = type} optional_position)
+addToBase info_ptr atype=:{at_type = TFAC atvs type contexts} optional_position ts_var_heap
+	= ts_var_heap  <:= (info_ptr, VI_FATypeC atvs {atype & at_type = type} contexts optional_position)
 addToBase info_ptr type optional_position ts_var_heap
 	= ts_var_heap  <:= (info_ptr, VI_Type type optional_position)
 
@@ -2170,11 +2287,11 @@ where
 		| is_start_rule && nr_of_args > 0
 			# (tst_args, ts) = fresh_attributed_type_variables (nr_of_args - 1) [{at_attribute = TA_Unique, /*at_annotation = AN_Strict,*/ at_type = TB BT_World }] ts
 			  (tst_result, ts) = (if is_caf freshNonUniqueVariable freshAttributedVariable) ts
-			= ({tst_args=tst_args, tst_arity=1, tst_result=tst_result, tst_context=[], tst_attr_env = [], tst_lifted=0}, ts)
+			= ({tst_args=tst_args, tst_arity=1, tst_result=tst_result, tst_context=[], tst_var_contexts=NoVarContexts, tst_attr_env=[], tst_lifted=0}, ts)
 			# (tst_args, ts) = fresh_attributed_type_variables nr_of_args [] ts
 			  (tst_args, ts) = fresh_attributed_type_variables nr_of_lifted_args tst_args ts
 			  (tst_result, ts) = (if is_caf freshNonUniqueVariable freshAttributedVariable) ts
-			= ({tst_args=tst_args, tst_arity=nr_of_args + nr_of_lifted_args, tst_result=tst_result, tst_context=[], tst_attr_env=[], tst_lifted=0}, ts)
+			= ({tst_args=tst_args, tst_arity=nr_of_args + nr_of_lifted_args, tst_result=tst_result, tst_context=[], tst_var_contexts=NoVarContexts, tst_attr_env=[], tst_lifted=0}, ts)
 
 	fresh_attributed_type_variables :: !Int ![AType] !*TypeState -> (![AType], !*TypeState)
 	fresh_attributed_type_variables n vars ts
@@ -2771,11 +2888,46 @@ where
 				(foldSt expand_type_contexts req_overloaded_calls subst_expr_heap) 
 
 	expand_type_contexts over_info_ptr (subst, expr_heap)
-		# (EI_Overloaded info, expr_heap) = readPtr over_info_ptr expr_heap
-		  (changed, oc_context, subst) = arraySubst info.oc_context subst
-		| changed
-			= (subst, expr_heap <:= (over_info_ptr, EI_Overloaded { info & oc_context = oc_context }))
-			= (subst, expr_heap)
+		= case readPtr over_info_ptr expr_heap of
+			(EI_Overloaded info, expr_heap)
+				# (changed,oc_context,subst) = arraySubst info.oc_context subst
+				| changed
+					-> (subst,expr_heap <:= (over_info_ptr, EI_Overloaded {info & oc_context = oc_context}))
+					-> (subst,expr_heap)
+			(EI_OverloadedWithVarContexts info, expr_heap)
+				# (changed,ocvc_context,subst) = arraySubst info.ocvc_context subst
+				| changed
+					# (changed2,ocvc_var_contexts,subst) = arraySubst info.ocvc_var_contexts subst
+					| changed2
+						# expr_heap = expr_heap <:= (over_info_ptr, EI_OverloadedWithVarContexts {info & ocvc_context=ocvc_context,ocvc_var_contexts=ocvc_var_contexts})
+						-> (subst,expr_heap)
+						# expr_heap = expr_heap <:= (over_info_ptr, EI_OverloadedWithVarContexts {info & ocvc_context=ocvc_context})
+						-> (subst,expr_heap)
+					# (changed,ocvc_var_contexts,subst) = arraySubst info.ocvc_var_contexts subst
+					| changed
+						# expr_heap = expr_heap <:= (over_info_ptr, EI_OverloadedWithVarContexts {info & ocvc_var_contexts=ocvc_var_contexts})
+						-> (subst,expr_heap)
+						-> (subst,expr_heap)
+			(EI_CaseTypeWithContexts case_type contexts, expr_heap)
+				# (changed,contexts,subst) = expand_constructor_contexts contexts subst
+				| changed
+					# expr_heap = expr_heap <:= (over_info_ptr, EI_CaseTypeWithContexts case_type contexts)
+					-> (subst,expr_heap)
+					-> (subst,expr_heap)
+
+	expand_constructor_contexts [context=:(cons_symbol,cons_context):contexts] subst
+		# (changed1,expanded_contexts,subst) = expand_constructor_contexts contexts subst
+		| changed1
+			# (changed2,cons_context,subst) = arraySubst cons_context subst
+			| changed2
+				= (True,[(cons_symbol,cons_context):expanded_contexts],subst)
+				= (True,[context:expanded_contexts],subst)
+			# (changed2,cons_context,subst) = arraySubst cons_context subst
+			| changed2
+				= (True,[(cons_symbol,cons_context):contexts],subst)
+				= (False,[context:contexts],subst)
+	expand_constructor_contexts [] subst
+		= (False,[],subst)
 
 	expand_case_or_let_types info_ptrs subst_expr_heap
 		= foldSt expand_case_or_let_type info_ptrs subst_expr_heap
@@ -2792,6 +2944,11 @@ where
 				| changed
 					-> (subst, expr_heap <:= (info_ptr, EI_LetType let_type))
 					-> (subst, expr_heap)
+			(EI_CaseTypeWithContexts case_type contexts, expr_heap)
+				# (changed, case_type, subst) = arraySubst case_type subst
+				| changed
+					-> (subst, expr_heap <:= (info_ptr, EI_CaseTypeWithContexts case_type contexts))
+					-> (subst, expr_heap)
 
 	expand_function_types :: ![Int] !*{!Type} *{! FunctionType} -> (!*{!Type}, *{! FunctionType})
 	expand_function_types [fun : funs] subst ts_fun_env
@@ -3042,6 +3199,8 @@ getTypeInfoOfVariable {var_info_ptr} var_heap
 			-> (type_info, var_heap)
 		VI_FAType _ _ type_info
 			-> (type_info, var_heap)
+		VI_FATypeC _ _ _ type_info
+			-> (type_info, var_heap)
 
 empty_id =: { id_name = "", id_info = nilPtr }
 
diff --git a/frontend/type_io.icl b/frontend/type_io.icl
index 97d4093..249b863 100644
--- a/frontend/type_io.icl
+++ b/frontend/type_io.icl
@@ -304,6 +304,11 @@ where
   		# wtis & wtis_type_heaps = {wtis_type_heaps & th_vars = th_vars}
 		= write_type_info type tcl_file wtis
 
+	write_type_info (TFAC uni_vars type _) tcl_file wtis=:{wtis_type_heaps}
+ 		# (_,th_vars) = foldSt normalize_atype_var uni_vars (0,wtis_type_heaps.th_vars)
+  		# wtis & wtis_type_heaps = {wtis_type_heaps & th_vars = th_vars}
+		= write_type_info type tcl_file wtis
+
 	write_type_info TE tcl_file wtis
 		# tcl_file
 			= fwritec TypeTECode tcl_file
@@ -346,6 +351,12 @@ where
 		# (tcl_file,wtis)
 			= write_type_info temp_var_id tcl_file wtis
 		= (tcl_file,wtis)	
+	write_type_info (TempQCDV temp_var_id) tcl_file wtis
+		# tcl_file
+			= fwritec ConsVariableTempQCVCode tcl_file
+		# (tcl_file,wtis)
+			= write_type_info temp_var_id tcl_file wtis
+		= (tcl_file,wtis)	
 
 instance WriteTypeInfo TypeSymbIdent
 where
diff --git a/frontend/typesupport.dcl b/frontend/typesupport.dcl
index 9a33146..f425bbf 100644
--- a/frontend/typesupport.dcl
+++ b/frontend/typesupport.dcl
@@ -56,6 +56,7 @@ beautifulizeAttributes :: !SymbolType !*AttrVarHeap -> (!SymbolType, !.AttrVarHe
 	,	tst_lifted		:: !Int
 	,	tst_result		:: !AType
 	,	tst_context		:: ![TypeContext]
+	,	tst_var_contexts :: !(VarContexts TypeContext)
 	,	tst_attr_env	:: ![AttrCoercion]
 	}
 
@@ -151,4 +152,3 @@ foldATypeSt on_atype on_type type st :== fold_atype_st type st
 	fold_atype_st atype=:{at_type} st
 		#! st = fold_type_st at_type st
 		= on_atype atype st
-
diff --git a/frontend/typesupport.icl b/frontend/typesupport.icl
index 9e291e5..6c016ce 100644
--- a/frontend/typesupport.icl
+++ b/frontend/typesupport.icl
@@ -16,6 +16,7 @@ import syntax, expand_types, unitype, utilities, checktypes
 	,	tst_lifted		:: !Int
 	,	tst_result		:: !AType
 	,	tst_context		:: ![TypeContext]
+	,	tst_var_contexts :: !(VarContexts TypeContext)
 	,	tst_attr_env	:: ![AttrCoercion]
 	}
 
@@ -192,6 +193,11 @@ instance clean_up [a] | clean_up a
 where
 	clean_up cui l cus = mapSt (clean_up cui) l cus
 
+instance clean_up DictionaryAndClassType where
+	clean_up cui {dc_var,dc_class_type} cus
+		# (dc_class_type,cus) = clean_up cui dc_class_type cus
+		= ({dc_var=dc_var,dc_class_type=dc_class_type},cus)
+
 cleanUpVariable _ TE tv_number cus=:{cus_heaps,cus_var_store,cus_var_env}
 	# (tv_info_ptr, th_vars) = newPtr TVI_Empty cus_heaps.th_vars
 	  new_var = TV {tv_ident = NewVarId cus_var_store, tv_info_ptr = tv_info_ptr}
@@ -211,6 +217,7 @@ cClosed				:== 0
 cDefinedVar			:== 1
 cUndefinedVar		:== 2
 cLiftedVar			:== 4
+cQVar				:== 8
 
 cleanUpClosedVariable TE env
 	= (cUndefinedVar, TE, env)
@@ -255,6 +262,10 @@ where
 			= (cur1, TempCV tv_number :@: types, env)
 			# (cur2, types, env) = cleanUpClosed types env
             = (combineCleanUpResults cur1 cur2, simplifyTypeApplication type types, env)
+	cleanUpClosed t=:(TempQV _) env
+		= (cQVar, t, env)
+	cleanUpClosed t=:(TempQDV _) env
+		= (cQVar, t, env)
 	cleanUpClosed t env
 		= (cClosed, t, env)
 
@@ -380,6 +391,13 @@ where
 			= ({ at & at_type = TFA avars type, at_attribute = at_attribute}, (all_exi_vars, cus))
 			= ({ at & at_type = TFA avars type, at_attribute = at_attribute},
 					(all_exi_vars, {cus & cus_error = existentialError cus.cus_error, cus_exis_vars = []}))
+	clean_up_arg_type cui at=:{at_type = TFAC avars type contexts, at_attribute} (all_exi_vars, cus)
+		# (at_attribute, cus) 	= cleanUpTypeAttribute False cui at_attribute cus
+		  (type, cus)			= clean_up cui type cus
+		| isEmpty cus.cus_exis_vars
+			= ({ at & at_type = TFAC avars type contexts, at_attribute = at_attribute}, (all_exi_vars, cus))
+			= ({ at & at_type = TFAC avars type contexts, at_attribute = at_attribute},
+					(all_exi_vars, {cus & cus_error = existentialError cus.cus_error, cus_exis_vars = []}))
 	clean_up_arg_type cui at (all_exi_vars, cus)
 		# (at, cus) = clean_up cui at cus
 		  (cus_exis_vars, cus) = cus!cus_exis_vars
@@ -412,9 +430,9 @@ where
 		|  spec_type
 			# var_heap = foldSt (mark_specified_context derived_context) spec_context var_heap
 			  (rev_contexts, env, error) = foldSt clean_up_lifted_type_context derived_context ([], env, error)
-			  (rev_contexts, env, error) = foldSt clean_up_type_context spec_context (rev_contexts, env, error)
+			  (rev_contexts, env, var_heap, error) = foldSt clean_up_type_context spec_context (rev_contexts, env, var_heap, error)
 			= (reverse rev_contexts, env, var_heap, error)
-			# (rev_contexts, env, error) = foldSt clean_up_type_context derived_context ([], env, error)
+			# (rev_contexts, env, var_heap, error) = foldSt clean_up_type_context derived_context ([], env, var_heap, error)
 			= (reverse rev_contexts, env, var_heap, error)
 
 	mark_specified_context [] spec_tc var_heap
@@ -426,13 +444,17 @@ where
 				= var_heap <:= (spec_tc.tc_var, VI_ForwardClassVar tc_var)
 			= mark_specified_context tcs spec_tc var_heap
 
-	clean_up_type_context tc=:{tc_types, tc_class} (collected_contexts, env, error)
+	clean_up_type_context tc=:{tc_types,tc_class,tc_var} (collected_contexts, env, var_heap, error)
+		| case sreadPtr tc_var var_heap of VI_EmptyConstructorClassVar-> True; _ -> False
+			= (collected_contexts, env, var_heap, error)
 		# (cur, tc_types, env) = cleanUpClosed tc_types env
 		| checkCleanUpResult cur cUndefinedVar
-			= (collected_contexts, env, error)
+			= (collected_contexts, env, var_heap, error)
 		| checkCleanUpResult cur cLiftedVar
-			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, liftedContextError (toString tc_class) error)
-			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, error)
+			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, var_heap, liftedContextError (toString tc_class) error)
+		| checkCleanUpResult cur cQVar
+			= (collected_contexts, env, var_heap, error)
+			= ([{ tc & tc_types = tc_types } : collected_contexts ], env, var_heap, error)
 
 	clean_up_lifted_type_context tc=:{tc_types} (collected_contexts, env, error)
 		# (cur, tc_types, env) = cleanUpClosed tc.tc_types env
@@ -512,6 +534,35 @@ where
 				EI_DictionaryType dict_type
 					# (dict_type, cus) = clean_up cui dict_type cus
 					-> (expr_heap <:= (expr_ptr, EI_DictionaryType dict_type), cus)
+				EI_ContextWithVarContexts class_expressions var_contexts
+					# (var_contexts,cus) = clean_up_var_contexts var_contexts cus
+					-> (writePtr expr_ptr (EI_ContextWithVarContexts class_expressions var_contexts) expr_heap,cus)
+				where
+					clean_up_var_contexts (VarContext arg_n type_contexts arg_atype var_contexts) cus
+						# (type_contexts,cus) = clean_up cui type_contexts cus
+						  (arg_atype,cus) = clean_up cui arg_atype cus
+						  (var_contexts,cus) = clean_up_var_contexts var_contexts cus
+						= (VarContext arg_n type_contexts arg_atype var_contexts,cus)
+					clean_up_var_contexts NoVarContexts cus
+						= (NoVarContexts,cus)
+				EI_CaseTypeWithContexts case_type constructor_contexts
+					# (case_type, cus) = clean_up cui case_type cus
+					  (constructor_contexts, cus) = clean_up_constructor_contexts cui constructor_contexts cus
+					-> (expr_heap <:= (expr_ptr, EI_CaseTypeWithContexts case_type constructor_contexts), cus)
+				where
+					clean_up_constructor_contexts cui [(ds,type_contexts):constructor_contexts] cus
+						# (type_contexts,cus) = clean_up_type_contexts cui type_contexts cus
+						  (constructor_contexts,cus) = clean_up_constructor_contexts cui constructor_contexts cus
+						= ([(ds,type_contexts):constructor_contexts],cus)
+					clean_up_constructor_contexts cui [] cus
+						= ([],cus)
+
+					clean_up_type_contexts cui [type_contexts=:{tc_types}:constructor_contexts] cus
+						# (tc_types,cus) = clean_up cui tc_types cus
+						  (constructor_contexts,cus) = clean_up_type_contexts cui constructor_contexts cus
+						= ([{type_contexts & tc_types=tc_types}:constructor_contexts],cus)
+					clean_up_type_contexts cui [] cus
+						= ([],cus)
 
  	check_type_of_start_rule is_start_rule {st_context,st_arity,st_args} cus_error
  		| is_start_rule
@@ -540,6 +591,10 @@ where
 			# (at_attribute, cus) 	= cleanUpTypeAttribute False cui at_attribute cus
 			  (type, cus)			= clean_up cui type cus
 			= ({ at & at_type = TFA avars type, at_attribute = at_attribute}, cus)
+		clean_up_arg_type cui at=:{at_type = TFAC avars type contexts, at_attribute} cus
+			# (at_attribute, cus) 	= cleanUpTypeAttribute False cui at_attribute cus
+			  (type, cus)			= clean_up cui type cus
+			= ({ at & at_type = TFAC avars type contexts, at_attribute = at_attribute}, cus)
 		clean_up_arg_type cui at cus
 			= clean_up cui at cus
 
@@ -564,6 +619,9 @@ where
 	bind_instances_in_arg_type {at_type = TFA vars type1} {at_type = TFA _ type2} heaps
 		# heaps = clear_atype_vars vars heaps
 		= {heaps & th_vars = bindInstances type1 type2 heaps.th_vars}
+	bind_instances_in_arg_type {at_type = TFAC vars type1 _} {at_type = TFAC _ type2 _} heaps
+		# heaps = clear_atype_vars vars heaps
+		= {heaps & th_vars = bindInstances type1 type2 heaps.th_vars}
 	bind_instances_in_arg_type { at_type } atype2 heaps=:{th_vars}
 		= { heaps & th_vars = bindInstances at_type atype2.at_type th_vars }
 
@@ -594,6 +652,35 @@ where
 			EI_DictionaryType dict_type
 				# (_, dict_type, type_heaps) = substitute dict_type type_heaps
 				-> (type_heaps, expr_heap <:= (expr_ptr, EI_DictionaryType dict_type))
+			EI_ContextWithVarContexts class_expressions var_contexts
+				# (var_contexts,type_heaps) = substitute_var_contexts var_contexts type_heaps
+				-> (type_heaps,writePtr expr_ptr (EI_ContextWithVarContexts class_expressions var_contexts) expr_heap)
+			where
+				substitute_var_contexts (VarContext arg_n type_contexts arg_atype var_contexts) type_heaps
+					# (_, type_contexts,type_heaps) = substitute type_contexts type_heaps
+					  (_, arg_atype,type_heaps) = substitute arg_atype type_heaps
+					  (var_contexts,type_heaps) = substitute_var_contexts var_contexts type_heaps
+					= (VarContext arg_n type_contexts arg_atype var_contexts,type_heaps)
+				substitute_var_contexts NoVarContexts type_heaps
+					= (NoVarContexts,type_heaps)
+			EI_CaseTypeWithContexts case_type constructor_contexts
+				# (_,case_type, type_heaps) = substitute case_type type_heaps
+				  (constructor_contexts, type_heaps) = substitute_constructor_contexts constructor_contexts type_heaps
+				-> (type_heaps, expr_heap <:= (expr_ptr, EI_CaseTypeWithContexts case_type constructor_contexts))
+		where
+			substitute_constructor_contexts [(cons_symbol,context):constructor_contexts] type_heaps
+				# (_, context, type_heaps) = substitute context type_heaps
+				  (constructor_contexts, type_heaps) = substitute_constructor_contexts constructor_contexts type_heaps
+				= ([(cons_symbol,context):constructor_contexts],type_heaps)
+			substitute_constructor_contexts [] type_heaps
+				= ([],type_heaps)
+
+instance substitute DictionaryAndClassType where
+	substitute {dc_var,dc_class_type} type_heaps
+		# (changed,dc_class_type_r,type_heaps) = substitute dc_class_type type_heaps
+		| changed
+			= (True, {dc_var=dc_var,dc_class_type=dc_class_type_r},type_heaps)
+			= (False, {dc_var=dc_var,dc_class_type=dc_class_type},type_heaps)
 
 class bindInstances a :: !a !a !*TypeVarHeap -> *TypeVarHeap
 
@@ -784,6 +871,8 @@ where
 		= equiv types1 types2 heaps
 	equiv (TFA vars1 type1) (TFA vars2 type2) heaps
 		= equiv type1 type2 heaps
+	equiv (TFAC vars1 type1 _) (TFAC vars2 type2 _) heaps
+		= equiv type1 type2 heaps
 	equiv type1 type2 heaps
 		= (False, heaps)
 
@@ -1182,6 +1271,11 @@ where
 		 # (file, opt_beautifulizer) = writeType (file <<< "(A.") opt_beautifulizer (form, vars)
 		 # (file, opt_beautifulizer) = writeType (file <<< ":") opt_beautifulizer (clearProperty form cBrackets, type)
 		 = (file <<< ")", opt_beautifulizer)
+	writeType file opt_beautifulizer (form, TFAC vars type contexts)
+		 # (file, opt_beautifulizer) = writeType (file <<< "(A.") opt_beautifulizer (form, vars)
+		   (file, opt_beautifulizer) = writeType (file <<< ":") opt_beautifulizer (clearProperty form cBrackets, type)
+		   (file, opt_beautifulizer) = show_context form contexts (file,opt_beautifulizer)
+		 = (file <<< ")", opt_beautifulizer)
 	writeType file opt_beautifulizer (form, TQV varid)
 		= (file <<< "E." <<< varid, opt_beautifulizer)
 	writeType file opt_beautifulizer (form, TempQV tv_number)
@@ -1435,6 +1529,8 @@ getImplicitAttrInequalities st=:{st_args, st_result}
 		= get_ineqs_of_atype_list args
 	get_ineqs_of_type (TFA vars type)
 		= get_ineqs_of_type type
+	get_ineqs_of_type (TFAC vars type type_contexts)
+		= get_ineqs_of_type type
 	get_ineqs_of_type _
 		= Empty
 
@@ -1619,6 +1715,9 @@ anonymizeAttrVars st=:{st_attr_vars, st_args, st_result, st_attr_env} implicit_i
 	anonymize_type (TFA vars type) th_attrs
 		# (type, th_attrs) = anonymize_type type th_attrs
 		= (TFA vars type, th_attrs)
+	anonymize_type (TFAC vars type type_contexts) th_attrs
+		# (type, th_attrs) = anonymize_type type th_attrs
+		= (TFAC vars type type_contexts, th_attrs)
 	anonymize_type x th_attrs
 		= (x, th_attrs)
 
@@ -1885,6 +1984,8 @@ instance performOnAttrVars Type
 		= performOnAttrVars f at st
 	performOnAttrVars f (TFA vars type) st
 		= performOnAttrVars f type st
+	performOnAttrVars f (TFAC vars type type_contexts) st
+		= performOnAttrVars f type st
 	performOnAttrVars f _ st
 		= st
 
diff --git a/frontend/unitype.dcl b/frontend/unitype.dcl
index 12512e2..438637e 100644
--- a/frontend/unitype.dcl
+++ b/frontend/unitype.dcl
@@ -9,9 +9,7 @@ import syntax, analunitypes
 	,	crc_td_infos	:: !.TypeDefInfos
 	}
 
-class coerce a ::  !Sign !{# CommonDefs} !{# BOOLVECT} !TypePosition !a !a !*CoercionState -> (!Optional TypePosition, !*CoercionState)
-
-instance coerce AType
+coerce :: !Sign !{#CommonDefs} !{#BOOLVECT} !TypePosition !AType !AType !*CoercionState -> (!Optional TypePosition, !*CoercionState)
 
 ::	TypePosition :== [Int]
 
@@ -39,9 +37,8 @@ BITINDEX temp_var_id :== temp_var_id >> 5
 BITNUMBER temp_var_id :== temp_var_id bitand 31
 set_bit :: !Int !*{# BOOLVECT} -> .{# BOOLVECT}
 
-determineAttributeCoercions :: !AType !AType !Bool !u:{! Type} !*Coercions !{# CommonDefs } 
-	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps
-		-> (!Optional (TypePosition, AType), !u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps) 
+determineAttributeCoercions :: !AType !AType !Bool !u:{!Type} !*Coercions !{#CommonDefs} !{#BOOLVECT} !*TypeDefInfos !*TypeHeaps
+		-> (!Optional (TypePosition, AType), !u:{!Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps)
 
 ::	AttributePartition	:== {# Int}
 
diff --git a/frontend/unitype.icl b/frontend/unitype.icl
index 0de10bf..e865a0c 100644
--- a/frontend/unitype.icl
+++ b/frontend/unitype.icl
@@ -34,23 +34,19 @@ isPositive :: !TempVarId !{# BOOLVECT } -> Bool
 isPositive var_id cons_vars
 	= cons_vars.[BITINDEX var_id] bitand (1 << BITNUMBER var_id) <> 0
 
-
-determineAttributeCoercions :: !AType !AType !Bool !u:{! Type} !*Coercions !{# CommonDefs } 
-	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps
-		-> (!Optional (TypePosition, AType), !u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps) 
+determineAttributeCoercions :: !AType !AType !Bool !u:{!Type} !*Coercions !{#CommonDefs} !{#BOOLVECT} !*TypeDefInfos !*TypeHeaps
+	-> (!Optional (TypePosition, AType), !u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps) 
 determineAttributeCoercions off_type dem_type coercible subst coercions defs cons_vars td_infos type_heaps
 	# (_, exp_off_type, es) = expandType defs cons_vars off_type (subst, { es_type_heaps = type_heaps, es_td_infos = td_infos})
 	  (_, exp_dem_type, (subst, {es_td_infos,es_type_heaps})) = expandType defs cons_vars dem_type es
 	  (result, {crc_type_heaps, crc_coercions, crc_td_infos}) = coerce (if coercible PositiveSign TopSign) defs cons_vars [] exp_off_type exp_dem_type 
 	  		 { crc_type_heaps = es_type_heaps, crc_coercions = coercions, crc_td_infos = es_td_infos}
-
 	= case result of
 		No
 	  		-> (No, subst, crc_coercions, crc_td_infos, crc_type_heaps)
 	  	Yes pos
 			-> (Yes (pos, exp_off_type), subst, crc_coercions, crc_td_infos, crc_type_heaps)
 
-
 /*
 	= case result of
 		No
@@ -70,16 +66,12 @@ determineAttributeCoercions off_type dem_type coercible subst coercions defs con
 				-> undef
 
 file_to_true :: !File -> Bool
-file_to_true file = code {
-  .inline file_to_true
-          pop_b 2
-          pushB TRUE
-  .end
-  }
+file_to_true file = True
 */
 
 NotChecked :== -1	
 DummyAttrNumber :== -1
+
 ::	AttributeGroups	:== {! [Int]}
 
 partitionateAttributes :: !{! CoercionTree} !{! *CoercionTree} -> (!AttributePartition, !*{! CoercionTree})
@@ -190,7 +182,6 @@ where
 
 ::	CoercionTreeRecord = { tree :: !.CoercionTree }
 
-
 liftSubstitution :: !*{! Type} !{# CommonDefs } !{# BOOLVECT }  !Int !*TypeHeaps !*TypeDefInfos -> (*{! Type}, !Int, !*TypeHeaps, !*TypeDefInfos)
 liftSubstitution subst modules cons_vars attr_store type_heaps td_infos 
 	# ls = { ls_next_attr = attr_store, ls_td_infos = td_infos, ls_type_heaps = type_heaps}
@@ -216,7 +207,6 @@ adjustPropClass prop_class arity :== prop_class >> arity
 	,	ls_td_infos			:: !.TypeDefInfos
 	}
 
-
 liftTempTypeVariable :: !{# CommonDefs } !{# BOOLVECT } !TempVarId !*{! Type} !*LiftState
 	-> (!Bool, !Type, !*{! Type}, !*LiftState)
 liftTempTypeVariable modules cons_vars tv_number subst ls
@@ -232,6 +222,8 @@ typeIsNonCoercible _ (TempV _)
 	= True
 typeIsNonCoercible _ (TempQV _)
 	= True
+typeIsNonCoercible _ (TempQDV _)
+	= True
 typeIsNonCoercible _ (_ --> _)
 	= True
 typeIsNonCoercible _ TArrow
@@ -245,7 +237,7 @@ typeIsNonCoercible cons_vars (_ :@: _)
 typeIsNonCoercible _ _
 	= False
 
-class lift a :: !{# CommonDefs } !{# BOOLVECT } !a !*{! Type} !*LiftState -> (!Bool,!a, !*{! Type}, !*LiftState)
+class lift a :: !{#CommonDefs} !{#BOOLVECT} !a !*{!Type} !*LiftState -> (!Bool,!a, !*{! Type}, !*LiftState)
 
 liftTypeApplication modules cons_vars t0=:(TA cons_id=:{type_ident,type_index={glob_object,glob_module},type_arity,type_prop=type_prop0} cons_args) subst ls
 	# ({tdi_kinds}, ls) = ls!ls_td_infos.[glob_module].[glob_object]
@@ -275,8 +267,8 @@ liftTypeApplication modules cons_vars t0=:(TAS cons_id=:{type_ident,type_index={
 		| equal_type_prop type_prop type_prop0
 			= (False, t0, subst, ls)
 			= (True, TAS { cons_id & type_prop = type_prop } cons_args strictness, subst, ls)
-liftTypeApplication modules cons_vars type  subst ls
-	= lift modules cons_vars type  subst ls
+liftTypeApplication modules cons_vars type subst ls
+	= lift modules cons_vars type subst ls
 
 lift_list :: !{#CommonDefs} !{# BOOLVECT } ![AType] ![TypeKind] !*{!Type} !*LiftState
 	-> (!Bool,![AType], ![SignClassification], ![PropClassification], !*{!Type}, !*LiftState)
@@ -337,7 +329,7 @@ where
 		# (changed, arg_type, subst, ls) = lift modules cons_vars arg_type subst ls
 		| changed 
 			= (True, TArrow1 arg_type, subst, ls)
-			= (False, type, subst, ls)	
+			= (False, type, subst, ls)
 	lift modules cons_vars type=:(TempCV temp_var :@: types) subst ls
 		# (changed, var_type, subst, ls) = liftTempTypeVariable modules cons_vars temp_var subst ls
 		  (changed_types, types, subst, ls) = lift_list modules cons_vars types subst ls
@@ -351,6 +343,8 @@ where
 					-> (True, TempCV tv_number :@: types, subst, ls)
 				TempQV tv_number
 					-> (True, TempQCV tv_number :@: types, subst, ls)
+				TempQDV tv_number
+					-> (True, TempQCDV tv_number :@: types, subst, ls)
 				cons_var :@: cv_types
 					-> (True, cons_var :@: (cv_types ++ types), subst, ls)
 				TArrow -> case types of
@@ -419,7 +413,7 @@ where
 					-> abort ("expand_attribute (unitype.icl)" )//---> (av_ident <<- info ))
 		expand_attribute attr attr_var_heap
 			= (False, attr, attr_var_heap)
-	
+
 expandTempTypeVariable :: !TempVarId !*(!u:{! Type}, !*ExpansionState) -> (!Bool, !Type, !*(!u:{! Type}, !*ExpansionState))
 expandTempTypeVariable tv_number (subst, es)
 	# (type, subst) = subst![tv_number]
@@ -506,6 +500,8 @@ where
 					-> (True, TempCV tv_number :@: types, es)
 				TempQV tv_number
 					-> (True, TempQCV tv_number :@: types, es)
+				TempQDV tv_number
+					-> (True, TempQCDV tv_number :@: types, es)
 				cons_var :@: cv_types
 					-> (True, cons_var :@: (cv_types ++ types), es)
 				TArrow -> case types of
@@ -519,7 +515,6 @@ where
 	expandType modules cons_vars type es
 		= (False, type, es)
 
-
 expand_type_list ::  !{#CommonDefs} !{# BOOLVECT } ![AType] ![TypeKind] !(!u:{!Type}, !*ExpansionState)
 	-> (!Bool,![AType], ![SignClassification], ![PropClassification], !(!u:{!Type}, !*ExpansionState))
 expand_type_list modules cons_vars [] _ es
@@ -585,10 +580,8 @@ where
 ::	TypePosition :== [Int]
 
 /*
-
 'coerceAttributes offered_attribute offered_attribute sign coercions' coerce offered_attribute to
 offered_attribute according to sign. Failure is indicated by returning False as a result.
-
 */
 
 coerceAttributes :: !.TypeAttribute !.TypeAttribute !.Sign *Coercions -> (!Bool,.Coercions);
@@ -635,7 +628,6 @@ where
 		| isNonUnique coer_offered.[dem_attr] || isUnique coer_demanded.[off_attr]
 			= (True, coercions)
 			= (True, newInequality off_attr dem_attr coercions)
-					
 coerceAttributes TA_Unique (TA_TempVar av_number) {neg_sign} coercions=:{coer_offered}
 	| isNonUnique coer_offered.[av_number]
 		= (False, coercions)
@@ -747,96 +739,96 @@ tryToMakeNonUnique attr coercions=:{coer_demanded}
 		= (True, makeNonUnique attr coercions)
 //				---> ("tryToMakeNonUnique", attr)
 
-class coerce a ::  !Sign !{# CommonDefs} !{# BOOLVECT} !TypePosition !a !a !*CoercionState -> (!Optional TypePosition, !*CoercionState)
-
 Success No		=  True
 Success (Yes _)	=  False
 
-instance coerce AType
-where
-	coerce sign defs cons_vars tpos at1=:{at_attribute=attr1, at_type = type1} at2=:{at_attribute=attr2}  cs=:{crc_coercions}
-		#!attr_sign = adjust_sign sign type1 cons_vars
-		  (succ, crc_coercions) = coerceAttributes attr1 attr2 attr_sign crc_coercions
-		| succ
-			# (succ, cs) = coerceTypes sign defs cons_vars tpos at1 at2 { cs & crc_coercions = crc_coercions }
-			| Success succ
-				# (succ1, crc_coercions) = add_propagation_inequalities cons_vars attr1 type1 cs.crc_coercions
-				  (succ2, crc_coercions) = add_propagation_inequalities cons_vars attr2 at2.at_type crc_coercions
-				= (if (succ1 && succ2) No (Yes tpos), { cs & crc_coercions = crc_coercions })
-				= (succ, cs)
-			= (Yes tpos, { cs & crc_coercions = crc_coercions })
-	where		
-		adjust_sign :: !Sign !Type {# BOOLVECT} -> Sign
-		adjust_sign sign (TempV _) cons_vars
-			= TopSign
-		adjust_sign sign (TempQV _) cons_vars
-			= TopSign
-		adjust_sign sign (_ --> _) cons_vars
-			= TopSign
-		adjust_sign sign (TA {type_ident, type_prop={tsp_coercible}} _) cons_vars
-			| tsp_coercible
-				= sign
-				= TopSign
-		adjust_sign sign (TAS {type_ident, type_prop={tsp_coercible}} _ _) cons_vars
-			| tsp_coercible
-				= sign
-				= TopSign
-		adjust_sign sign TArrow cons_vars
+coerce :: !Sign !{#CommonDefs} !{#BOOLVECT} !TypePosition !AType !AType !*CoercionState -> (!Optional TypePosition, !*CoercionState)
+
+coerce sign defs cons_vars tpos at1=:{at_attribute=attr1, at_type = type1} at2=:{at_attribute=attr2} cs=:{crc_coercions}
+	#!attr_sign = adjust_sign sign type1 cons_vars
+	  (succ, crc_coercions) = coerceAttributes attr1 attr2 attr_sign crc_coercions
+	| succ
+		# (succ, cs) = coerceTypes sign defs cons_vars tpos at1 at2 { cs & crc_coercions = crc_coercions }
+		| Success succ
+			# (succ1, crc_coercions) = add_propagation_inequalities cons_vars attr1 type1 cs.crc_coercions
+			  (succ2, crc_coercions) = add_propagation_inequalities cons_vars attr2 at2.at_type crc_coercions
+			= (if (succ1 && succ2) No (Yes tpos), { cs & crc_coercions = crc_coercions })
+			= (succ, cs)
+		= (Yes tpos, { cs & crc_coercions = crc_coercions })
+where		
+	adjust_sign :: !Sign !Type {# BOOLVECT} -> Sign
+	adjust_sign sign (TempV _) cons_vars
+		= TopSign
+	adjust_sign sign (TempQV _) cons_vars
+		= TopSign
+	adjust_sign sign (TempQDV _) cons_vars
+		= TopSign
+	adjust_sign sign (_ --> _) cons_vars
+		= TopSign
+	adjust_sign sign (TA {type_ident, type_prop={tsp_coercible}} _) cons_vars
+		| tsp_coercible
+			= sign
 			= TopSign
-		adjust_sign sign (TArrow1 _) cons_vars
-			= TopSign					
-		adjust_sign sign (TempCV tmp_var_id :@: _) cons_vars
-			| isPositive tmp_var_id cons_vars
-				= sign
-				= TopSign
-		adjust_sign sign (_ :@: _) cons_vars
+	adjust_sign sign (TAS {type_ident, type_prop={tsp_coercible}} _ _) cons_vars
+		| tsp_coercible
+			= sign
 			= TopSign
-		adjust_sign sign _ cons_vars
+	adjust_sign sign TArrow cons_vars
+		= TopSign
+	adjust_sign sign (TArrow1 _) cons_vars
+		= TopSign					
+	adjust_sign sign (TempCV tmp_var_id :@: _) cons_vars
+		| isPositive tmp_var_id cons_vars
 			= sign
-
-		add_propagation_inequalities cons_vars attr (TA {type_prop={tsp_propagation}} cons_args) coercions
-			= add_inequalities_for_TA tsp_propagation attr cons_args coercions
-		add_propagation_inequalities cons_vars attr (TAS {type_prop={tsp_propagation}} cons_args _) coercions
-			= add_inequalities_for_TA tsp_propagation attr cons_args coercions
-		add_propagation_inequalities cons_vars attr (TempCV tmp_var_id :@: types) coercions
-			| isPositive tmp_var_id cons_vars
-				= add_inequalities attr types coercions
-				= (True, coercions)
-		where
-			add_inequalities attr [] coercions
-				= (True, coercions)
-			add_inequalities attr [{at_attribute} : args] coercions
-				# (succ, coercions) = coerceAttributes attr at_attribute PositiveSign coercions
-				| succ
-					= add_inequalities attr args coercions
-					= (False, coercions)
-		add_propagation_inequalities cons_vars attr type coercions
-				= (True, coercions)
-
-		add_inequalities_for_TA prop_class attr [] coercions
+			= TopSign
+	adjust_sign sign (_ :@: _) cons_vars
+		= TopSign
+	adjust_sign sign _ cons_vars
+		= sign
+
+	add_propagation_inequalities cons_vars attr (TA {type_prop={tsp_propagation}} cons_args) coercions
+		= add_inequalities_for_TA tsp_propagation attr cons_args coercions
+	add_propagation_inequalities cons_vars attr (TAS {type_prop={tsp_propagation}} cons_args _) coercions
+		= add_inequalities_for_TA tsp_propagation attr cons_args coercions
+	add_propagation_inequalities cons_vars attr (TempCV tmp_var_id :@: types) coercions
+		| isPositive tmp_var_id cons_vars
+			= add_inequalities attr types coercions
+			= (True, coercions)
+	where
+		add_inequalities attr [] coercions
 			= (True, coercions)
-		add_inequalities_for_TA prop_class attr [{at_attribute} : args] coercions
-			| (prop_class bitand 1) == 0
-				= add_inequalities_for_TA (prop_class >> 1) attr args coercions
+		add_inequalities attr [{at_attribute} : args] coercions
 			# (succ, coercions) = coerceAttributes attr at_attribute PositiveSign coercions
 			| succ
-				= add_inequalities_for_TA (prop_class >> 1) attr args coercions
+				= add_inequalities attr args coercions
 				= (False, coercions)
+	add_propagation_inequalities cons_vars attr type coercions
+			= (True, coercions)
+
+	add_inequalities_for_TA prop_class attr [] coercions
+		= (True, coercions)
+	add_inequalities_for_TA prop_class attr [{at_attribute} : args] coercions
+		| (prop_class bitand 1) == 0
+			= add_inequalities_for_TA (prop_class >> 1) attr args coercions
+		# (succ, coercions) = coerceAttributes attr at_attribute PositiveSign coercions
+		| succ
+			= add_inequalities_for_TA (prop_class >> 1) attr args coercions
+			= (False, coercions)
 
 tryToExpandTypeSyn :: !{#CommonDefs} !{#BOOLVECT} !Type !TypeSymbIdent ![AType] !TypeAttribute !*TypeHeaps !*TypeDefInfos
 	-> (!Bool, !Type, !*TypeHeaps, !*TypeDefInfos)
 tryToExpandTypeSyn defs cons_vars type cons_id=:{type_index={glob_object,glob_module}} type_args attribute type_heaps td_infos
 	# {td_rhs,td_args,td_attribute,td_ident} = defs.[glob_module].com_type_defs.[glob_object]
 	= case td_rhs of
-		SynType {at_type}			
+		SynType {at_type}
 			# type_heaps = bindTypeVarsAndAttributes td_attribute attribute td_args type_args type_heaps
 			  (_, expanded_type, (_, {es_type_heaps, es_td_infos})) = expandType defs cons_vars at_type
 			  		({}, { es_type_heaps = type_heaps, es_td_infos = td_infos })
 			-> (True, expanded_type, clearBindingsOfTypeVarsAndAttributes attribute td_args es_type_heaps, es_td_infos)
 
 		_
-			-> (False, type/*TA cons_id type_args*/, type_heaps, td_infos)
-		
+			-> (False, type, type_heaps, td_infos)
+
 coerceTypes :: !Sign !{# CommonDefs} !{# BOOLVECT} !TypePosition !AType !AType !*CoercionState -> (!Optional TypePosition, !*CoercionState)		
 coerceTypes sign defs cons_vars tpos dem_type=:{at_type=type1=:TA dem_cons dem_args} off_type=:{at_type=type2=:TA off_cons off_args}  cs=:{crc_type_heaps, crc_td_infos}
 	| dem_cons == off_cons