uniqueness unification for types of functions that are generated

during the transformation phase


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

12 files changed, 1023 insertions, 727 deletions

diff --git a/frontend/analunitypes.icl b/frontend/analunitypes.icl
index f099825..ab31866 100644
--- a/frontend/analunitypes.icl
+++ b/frontend/analunitypes.icl
@@ -305,6 +305,11 @@ signClassOfType type _ _ _ _ scs
 propClassification :: !Index !Index ![PropClassification] !{# CommonDefs } !*TypeVarHeap !*TypeDefInfos
 	-> (!PropClassification, !*TypeVarHeap, !*TypeDefInfos)
 propClassification type_index module_index hio_props defs type_var_heap td_infos
+// MW3..
+	| type_index>=size td_infos.[module_index]
+		// must be a dictionary => doesn't propagate
+		= (0, type_var_heap, td_infos)
+// ..MW3
 	# {td_args, td_name} = defs.[module_index].com_type_defs.[type_index]
 	  (td_info, td_infos) = td_infos![module_index].[type_index]
 	= determinePropClassOfTypeDef type_index module_index td_args td_info hio_props defs type_var_heap td_infos
@@ -540,6 +545,3 @@ where
 propClassOfType _ _ _ pcs
 	= (NoPropClass, NoPropClass, pcs)
 
-instance == SignClassification
-where
-	== sc1 sc2 = sc1.sc_pos_vect == sc2.sc_pos_vect && sc1.sc_neg_vect == sc2.sc_neg_vect
diff --git a/frontend/frontend.icl b/frontend/frontend.icl
index 6e2b5d6..f70ca43 100644
--- a/frontend/frontend.icl
+++ b/frontend/frontend.icl
@@ -118,7 +118,7 @@ frontEndInterface upToPhase mod_ident search_paths dcl_modules functions_and_mac
 	| upToPhase == FrontEndPhaseCheck
 		=	frontSyntaxTree cached_functions_and_macros n_functions_and_macros_in_dcl_modules main_dcl_module_n predef_symbols hash_table files error io out icl_mod dcl_mods fun_defs components array_instances optional_dcl_icl_conversions global_fun_range heaps
 
-	# (ok, fun_defs, array_instances, type_code_instances, common_defs, imported_funs, heaps, predef_symbols, error,out)
+	# (ok, fun_defs, array_instances, type_code_instances, common_defs, imported_funs, type_def_infos, heaps, predef_symbols, error,out)
 		= typeProgram (components -*-> "Typing") main_dcl_module_n icl_functions icl_specials list_inferred_types icl_common [a\\a<-:icl_import] dcl_mods icl_used_module_numbers heaps predef_symbols error out
 
 	| not ok
@@ -145,7 +145,7 @@ frontEndInterface upToPhase mod_ident search_paths dcl_modules functions_and_mac
 		 = analyseGroups common_defs array_instances main_dcl_module_n (components -*-> "Analyse") fun_defs var_heap expression_heap
 
 	  (components, fun_defs, dcl_types, used_conses, var_heap, type_heaps, expression_heap)
-	  	= transformGroups cleanup_info main_dcl_module_n (components -*-> "Transform")  fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics var_heap type_heaps expression_heap
+	  	= transformGroups cleanup_info main_dcl_module_n (components -*-> "Transform")  fun_defs acc_args common_defs imported_funs dcl_types used_conses_in_dynamics type_def_infos var_heap type_heaps expression_heap
 
 	| upToPhase == FrontEndPhaseTransformGroups
 		# heaps = {hp_var_heap=var_heap, hp_type_heaps=type_heaps, hp_expression_heap=expression_heap}
diff --git a/frontend/syntax.dcl b/frontend/syntax.dcl
index a846939..91f2457 100644
--- a/frontend/syntax.dcl
+++ b/frontend/syntax.dcl
@@ -54,7 +54,6 @@ instance toString Ident
 				| STE_Imported !STE_Kind !Index
 				| STE_DclFunction
 				| STE_Module !(Module (CollectedDefinitions ClassInstance IndexRange))
-				| STE_OpenModule !Int !(Module (CollectedDefinitions ClassInstance IndexRange))
 				| STE_ClosedModule
 				| STE_Empty
 					/* for creating class dictionaries */
@@ -833,17 +832,15 @@ cNonRecursiveAppl	:== False
 					| TVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
 					| TVI_AType !AType /* auxiliary used in module comparedefimp */
 					| TVI_Used /* to administer that this variable is encountered (in checkOpenTypes) */
-//					| TVI_Clean !Int /* to keep the unique number that has been assigned to this variable during 'clean_up' */
 					| TVI_TypeCode !TypeCodeExpression
-// MdM
 					| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
-// ... MdM
-
+					
 ::	TypeVarInfoPtr	:== Ptr TypeVarInfo
 ::	TypeVarHeap 	:== Heap TypeVarInfo
 
 ::	AttrVarInfo  	= AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId 
 					| AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
+					| AVI_Used
 					| AVI_Count !Int /* auxiliary used in module typesupport */
 					
 ::	AttrVarInfoPtr	:== Ptr AttrVarInfo
@@ -866,9 +863,10 @@ cNonRecursiveAppl	:== False
 	}
 
 ::	TypeAttribute = TA_Unique | TA_Multi | TA_Var !AttributeVar | TA_RootVar AttributeVar | TA_TempVar !Int  | TA_TempExVar
-				  | TA_Anonymous | TA_None
-				  | TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
-
+					| 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_name			:: !Ident
 	,	av_info_ptr		:: !AttrVarInfoPtr
diff --git a/frontend/syntax.icl b/frontend/syntax.icl
index f5ee540..62e5fc6 100644
--- a/frontend/syntax.icl
+++ b/frontend/syntax.icl
@@ -54,7 +54,6 @@ where toString {import_module} = toString import_module
 				| STE_Imported !STE_Kind !Index
 				| STE_DclFunction
 				| STE_Module !(Module (CollectedDefinitions ClassInstance IndexRange))
-				| STE_OpenModule !Int !(Module (CollectedDefinitions ClassInstance IndexRange))
 				| STE_ClosedModule
 				| STE_Empty 
 				| STE_DictType !CheckedTypeDef
@@ -425,8 +424,8 @@ cIsALocalVar	:== False
 
 ::	ConsClasses =
 	{	cc_size			::!Int
-	,	cc_args			::![ConsClass]	// the lists have the
-	,	cc_linear_bits	::![Bool]		// same length
+	,	cc_args			::![ConsClass]
+	,	cc_linear_bits	::![Bool]
 	}
 					
 ::	ConsClass	:== Int
@@ -778,15 +777,14 @@ cNotVarNumber :== -1
 					| TVI_AType !AType /* auxiliary used in module comparedefimp */
 					| TVI_Used /* to adminster that this variable is encountered (in checkOpenTypes) */
 					| TVI_TypeCode !TypeCodeExpression
-// MdM
 					| TVI_CPSLocalTypeVar !Int /* MdM - the index of the variable as generated by the theorem prover */
-// ... MdM
 
 ::	TypeVarInfoPtr	:== Ptr TypeVarInfo
 ::	TypeVarHeap 	:== Heap TypeVarInfo
 
 ::	AttrVarInfo  	= AVI_Empty | AVI_Attr !TypeAttribute | AVI_Forward !TempAttrId
 					| AVI_CorrespondenceNumber !Int /* auxiliary used in module comparedefimp */
+					| AVI_Used
 					| AVI_Count !Int /* auxiliary used in module typesupport */
 
 ::	AttrVarInfoPtr	:== Ptr AttrVarInfo
@@ -810,8 +808,9 @@ cNotVarNumber :== -1
 	}
 
 ::	TypeAttribute = TA_Unique | TA_Multi | TA_Var !AttributeVar | TA_RootVar AttributeVar | TA_TempVar !Int | TA_TempExVar
-				  | TA_Anonymous | TA_None
-				  | TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
+					| TA_Anonymous | TA_None
+					| TA_List !Int !TypeAttribute | TA_Locked !TypeAttribute
+					| TA_MultiOfPropagatingConsVar
 
 ::	AttributeVar =
 	{	av_name			:: !Ident
@@ -1219,6 +1218,8 @@ where
 		= ""
 	toString TA_Multi
 		= "o "
+	toString TA_MultiOfPropagatingConsVar
+		= "@@ "
 	toString (TA_List _ _)
 		= "??? "
 	toString TA_TempExVar
@@ -1344,8 +1345,7 @@ where
 
 instance <<< AlgebraicPattern
 where
-//	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " -> " <<< g.ap_expr
-	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " " <<< g.ap_position <<< "-> " <<< g.ap_expr
+	(<<<) file g = file <<< g.ap_symbol <<< g.ap_vars <<< " -> " <<< g.ap_expr
 
 instance <<< BasicPattern
 where
@@ -1585,10 +1585,8 @@ where
 	(<<<) file {fun_symb,fun_body=ParsedBody bodies} = file <<< fun_symb <<< '.' <<< ' ' <<< bodies 
 	(<<<) file {fun_symb,fun_body=CheckedBody {cb_args,cb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '.'
 			<<< "C " <<< cb_args <<< " = " <<< cb_rhs 
-//			<<< '.' <<< fi_def_level <<< ' ' <<< '[' <<< fi_free_vars <<< ']' <<< cb_args <<< " = " <<< cb_rhs 
-	(<<<) file {fun_symb,fun_body=TransformedBody {tb_args,tb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '.'
-			<<< "T "  <<< tb_args <<< '[' <<< fi_calls <<< ']' <<< " = " <<< tb_rhs 
-//			<<< '.' <<< fi_def_level <<< ' ' <<< '[' <<< fi_free_vars <<< ']' <<< tb_args <<< " = " <<< tb_rhs 
+	(<<<) file {fun_symb,fun_index,fun_body=TransformedBody {tb_args,tb_rhs},fun_info={fi_free_vars,fi_def_level,fi_calls}} = file <<< fun_symb <<< '@' <<< fun_index
+			<<< tb_args <<< " = " <<< tb_rhs 
 	(<<<) file {fun_symb,fun_body=BackendBody body,fun_type=Yes type} = file <<< type <<< '\n' <<< fun_symb <<< '.'
 			<<< body <<< '\n'
 	(<<<) file {fun_symb,fun_body=NoBody,fun_type=Yes type} = file <<< type <<< '\n' <<< fun_symb <<< '.'
@@ -1830,7 +1828,7 @@ where
 		show_expression file (Update expr1 selectors expr2)
 			= file <<< "update"
 		show_expression file (TupleSelect {ds_arity} elem_nr expr)
-			= file <<< "argument" <<< (elem_nr + 1) <<< " of " <<< ds_arity <<< "-tuple"
+			= file <<< "argument " <<< (elem_nr + 1) <<< " of " <<< ds_arity <<< "-tuple"
 		show_expression file (BasicExpr bv _)
 			= file <<< bv
 		show_expression file (MatchExpr _ _ expr)
@@ -1891,9 +1889,6 @@ where
 		(STE_Module _)
 			= file <<< "STE_Module"
 	(<<<) file
-		(STE_OpenModule _ _)
-			= file <<< "STE_OpenModule"
-	(<<<) file
 		STE_ClosedModule
 			= file <<< "STE_ClosedModule"
 	(<<<) file
diff --git a/frontend/trans.dcl b/frontend/trans.dcl
index dd6d153..5eff949 100644
--- a/frontend/trans.dcl
+++ b/frontend/trans.dcl
@@ -14,8 +14,8 @@ analyseGroups	:: !{# CommonDefs} !IndexRange !Int !*{! Group} !*{#FunDef} !*VarH
 				-> (!CleanupInfo, !*{! ConsClasses}, !*{! Group}, !*{#FunDef}, !*VarHeap, !*ExpressionHeap)
 
 transformGroups :: !CleanupInfo !Int !*{! Group} !*{#FunDef} !{!.ConsClasses} !{# CommonDefs}  !{# {# FunType} }
-		!*{#{# CheckedTypeDef}} !ImportedConstructors !*VarHeap !*TypeHeaps !*ExpressionHeap
-			-> (!*{! Group}, !*{#FunDef}, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*VarHeap, !*TypeHeaps, !*ExpressionHeap)
+					!*{#{# CheckedTypeDef}} !ImportedConstructors !*TypeDefInfos !*VarHeap !*TypeHeaps !*ExpressionHeap
+				-> (!*{! Group}, !*{#FunDef}, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*VarHeap, !*TypeHeaps, !*ExpressionHeap)
 
 partitionateFunctions :: !*{# FunDef} ![IndexRange] -> (!*{! Group}, !*{# FunDef})
 
diff --git a/frontend/trans.icl b/frontend/trans.icl
index 68c7a9f..7dae3e8 100644
--- a/frontend/trans.icl
+++ b/frontend/trans.icl
@@ -2,7 +2,7 @@ implementation module trans
 
 import StdEnv
 
-import syntax, transform, checksupport, StdCompare, check, utilities //,RWSDebug
+import syntax, transform, checksupport, StdCompare, check, utilities, unitype, typesupport, type
 
 ::	PartitioningInfo = 
 	{	pi_marks :: 		!.{# Int}
@@ -347,7 +347,7 @@ instance consumerRequirements Case where
 			  all_constructors = [ ds_index \\ {ds_index}<-defined_symbols ]
 			  pattern_constructors = [ glob_object.ds_index \\ {ap_symbol={glob_object}}<-algebraic_patterns]	
 			  sorted_pattern_constructors = sort pattern_constructors unsafe_bits
-			  all_sorted_constructors = if (is_sorted all_constructors) all_constructors (quicksort (<) all_constructors)
+			  all_sorted_constructors = if (is_sorted all_constructors) all_constructors (sortBy (<) all_constructors)
 			= (appearance_loop all_sorted_constructors sorted_pattern_constructors, not (multimatch_loop has_default sorted_pattern_constructors))
 		  where
 			is_sorted [x]
@@ -363,7 +363,7 @@ instance consumerRequirements Case where
 			= (False, False)
 
 		sort constr_indices unsafe_bits
-			= quicksort smaller (zip3 constr_indices [0..] unsafe_bits)
+			= sortBy smaller (zip3 constr_indices [0..] unsafe_bits)
 		  where
 			smaller (i1,si1,_) (i2,si2,_)
 				| i1<i2		= True
@@ -480,7 +480,6 @@ independentConsumerRequirements exprs common_defs ai=:{ai_cur_ref_counts}
 	unify_ref_counts 1 x = if (x==0) 1 2
 	unify_ref_counts 2 _ = 2
 
-
 analyseGroups	:: !{# CommonDefs} !IndexRange !Int !*{! Group} !*{#FunDef} !*VarHeap !*ExpressionHeap 
 				-> (!CleanupInfo, !*{! ConsClasses}, !*{! Group}, !*{#FunDef}, !*VarHeap, !*ExpressionHeap)
 analyseGroups common_defs {ir_from, ir_to} main_dcl_module_n groups fun_defs var_heap expr_heap
@@ -550,7 +549,7 @@ where
 
 	analyse_functions common_defs [fun : funs] cfvog_accu ai fun_defs
 		#  (fun_def, fun_defs) = fun_defs![fun]
-		#  (TransformedBody {tb_args, tb_rhs}) = fun_def.fun_body
+ 		   (TransformedBody {tb_args, tb_rhs}) = fun_def.fun_body
 		   nr_of_args = length tb_args
 		   ai = { ai & ai_cur_ref_counts = createArray (nr_of_args + length fun_def.fun_info.fi_local_vars) 0,
 						ai_next_var_of_fun = nr_of_args }
@@ -601,6 +600,7 @@ mapAndLength f []
 	,	ti_var_heap				:: !.VarHeap
 	,	ti_symbol_heap			:: !.ExpressionHeap
 	,	ti_type_heaps			:: !.TypeHeaps
+	,	ti_type_def_infos		:: !.TypeDefInfos
 	,	ti_next_fun_nr			:: !Index
 	,	ti_cleanup_info			:: !CleanupInfo
 	,	ti_recursion_introduced	:: !Optional Index
@@ -974,14 +974,6 @@ possibly_generate_case_function kees=:{case_info_ptr} aci=:{aci_free_vars} ro ti
 		# (FI_Function {gf_fun_def, gf_cons_args}, fun_heap) = readPtr fun_info_ptr fun_heap
 		= (gf_fun_def, gf_cons_args, fun_defs, fun_heap)
 
-/*
-	get_fun_def_and_cons_args (SK_Function {glob_object}) cons_args fun_defs fun_heap
-		# (fun_def, fun_defs) = fun_defs![glob_object]
-		= (fun_def, cons_args.[glob_object], fun_defs, fun_heap)
-	get_fun_def_and_cons_args (SK_GeneratedFunction fun_info_ptr _) cons_args fun_defs fun_heap
-		# (FI_Function {gf_fun_def, gf_cons_args}, fun_heap) = readPtr fun_info_ptr fun_heap
-		= (gf_fun_def, gf_cons_args, fun_defs, fun_heap)
-*/
 	generate_case_function old_ti_recursion_introduced fun_index case_info_ptr new_expr outer_fun_def outer_cons_args used_mask
 						{ro_fun=ro_fun=:{symb_kind=SK_GeneratedFunction fun_info_ptr _}, ro_fun_args} ti
 //		| False->>"generate_case_function"
@@ -994,9 +986,9 @@ possibly_generate_case_function kees=:{case_info_ptr} aci=:{aci_free_vars} ro ti
 		  (EI_CaseType {ct_result_type}, ti_symbol_heap) = readExprInfo case_info_ptr ti.ti_symbol_heap
 		  (form_vars, ti_var_heap) = mapSt bind_to_fresh_var ro_fun_args ti_var_heap
 		  arg_types = lifted_types++types_from_outer_fun
-		  type_variables = getTypeVars [ct_result_type:arg_types]
 		  {th_vars,th_attrs} = ti.ti_type_heaps
-		  (fresh_type_vars, th_vars) = mapSt bind_to_fresh_type_var type_variables th_vars
+		  (type_variables, th_vars) = getTypeVars [ct_result_type:arg_types] th_vars
+		  (fresh_type_vars, th_vars) = mapSt bind_to_fresh_type_variable type_variables th_vars
 		  (fresh_arg_types, ti_type_heaps) = substitute arg_types { th_vars = th_vars, th_attrs = th_attrs }
 		  (fresh_result_type, ti_type_heaps) = substitute ct_result_type ti_type_heaps
 		  us = { us_var_heap = ti_var_heap, us_symbol_heap = ti_symbol_heap, us_opt_type_heaps = Yes ti_type_heaps, 
@@ -1044,10 +1036,6 @@ possibly_generate_case_function kees=:{case_info_ptr} aci=:{aci_free_vars} ro ti
 			  form_var = { fv_name = fv_name, fv_info_ptr = new_info_ptr, fv_count = undeff, fv_def_level = NotALevel }
 			  act_var = { var_name = fv_name, var_info_ptr = new_info_ptr, var_expr_ptr = nilPtr }
 			= (form_var, writeVarInfo fv_info_ptr (VI_Expression (Var act_var)) var_heap)
-		bind_to_fresh_type_var tv type_var_heap
-			# (new_info_ptr, type_var_heap) = newPtr TVI_Empty type_var_heap
-			  new_type_var = { tv_name = tv.tv_name, tv_info_ptr = new_info_ptr }
-			= (new_type_var, writePtr tv.tv_info_ptr (TVI_Type (TV new_type_var)) type_var_heap)
 		get_type_of_local_var {fv_info_ptr} var_heap
 			# (VI_Extended (EVI_VarType a_type) _, var_heap) = readPtr fv_info_ptr var_heap
 			= (a_type, var_heap)
@@ -1062,7 +1050,7 @@ removeNeverMatchingSubcases keesExpr=:(Case kees)
 	  filtered_default = get_filtered_default case_default
 	= case case_guards of
 		AlgebraicPatterns i alg_patterns
-			| not (any (is_never_matching_case o get_alg_rhs) alg_patterns)
+			| not (any (is_never_matching_case o get_alg_rhs) alg_patterns) && not (is_never_matching_default case_default)
 				-> keesExpr // frequent case: all subexpressions can't fail
 			# filtered_case_guards = filter (not o is_never_matching_case o get_alg_rhs) alg_patterns
 			| has_become_never_matching filtered_default filtered_case_guards
@@ -1071,7 +1059,7 @@ removeNeverMatchingSubcases keesExpr=:(Case kees)
 				-> fromYes case_default
 			-> Case {kees & case_guards = AlgebraicPatterns i filtered_case_guards, case_default = filtered_default }
 		BasicPatterns bt basic_patterns
-			| not (any (is_never_matching_case o get_basic_rhs) basic_patterns)
+			| not (any (is_never_matching_case o get_basic_rhs) basic_patterns) && not (is_never_matching_default case_default)
 				-> keesExpr // frequent case: all subexpressions can't fail
 			# filtered_case_guards = filter (not o is_never_matching_case o get_basic_rhs) basic_patterns
 			| has_become_never_matching filtered_default filtered_case_guards
@@ -1096,6 +1084,10 @@ removeNeverMatchingSubcases keesExpr=:(Case kees)
 		= False
 	get_alg_rhs {ap_expr} = ap_expr
 	get_basic_rhs {bp_expr} = bp_expr
+	is_never_matching_default No
+		= False
+	is_never_matching_default (Yes expr)
+		= is_never_matching_case expr
 removeNeverMatchingSubcases expr
 	= expr
 
@@ -1220,78 +1212,282 @@ searchInstance prods1 (II_Node prods2 fun_info_ptr left right)
 	= searchInstance prods1 left
 */
 
+coercionsToAttrEnv :: !{!TypeAttribute} !Coercions -> [AttrInequality]
+coercionsToAttrEnv attr_vars {coer_demanded, coer_offered}
+	= flatten [ [ {ai_offered = toAttrVar attr_vars.[offered],
+					ai_demanded = toAttrVar attr_vars.[demanded] }
+				\\ offered <- fst (flattenCoercionTree offered_tree) ]
+			  \\ offered_tree<-:coer_offered & demanded<-[0..] ]
+  where
+	toAttrVar (TA_Var av) = av
+
+:: UniquenessRequirement =
+	{	ur_offered		:: !AType
+	,	ur_demanded		:: !AType
+	,	ur_attr_ineqs	:: ![AttrCoercion]
+	}
+
+// XXX unused!
+instance == AttributeVar
+where
+	(==) av1 av2 = av1.av_info_ptr==av2.av_info_ptr
+
+
+readableCoercions {coer_demanded}
+	= [ (i, readable coer_demanded.[i]) \\ i<-[0..size coer_demanded - 1] ]
+  where
+	readable CT_Unique
+	 	= [TA_Unique]
+	readable CT_NonUnique
+	 	= [TA_Multi]
+	readable ct
+		# (vars, _) = flattenCoercionTree ct
+		= map TA_TempVar vars
+
 generateFunction :: !FunDef !ConsClasses !{! Producer} !FunctionInfoPtr !ReadOnlyTI !*TransformInfo -> (!Index, !Int, !*TransformInfo)
 generateFunction fd=:{fun_body = TransformedBody {tb_args,tb_rhs},fun_info = {fi_group_index}} 
 				 {cc_args,cc_linear_bits} prods fun_def_ptr ro
-				 ti=:{ti_var_heap,ti_next_fun_nr,ti_new_functions,ti_fun_heap,ti_symbol_heap,ti_fun_defs,ti_type_heaps,ti_cons_args,ti_cleanup_info}
+				 ti=:{ti_var_heap,ti_next_fun_nr,ti_new_functions,ti_fun_heap,ti_symbol_heap,ti_fun_defs,
+				 		ti_type_heaps,ti_cons_args,ti_cleanup_info, ti_type_def_infos}
 /*
 	| False->>("generating new function",fd.fun_symb.id_name,fd.fun_index,"->",ti_next_fun_nr)
 		= undef
+	| False--->("with type",fd.fun_type)
+		= undef
 	| False--->("producers:",II_Node prods nilPtr II_Empty II_Empty,("cc_args",cc_args,("cc_linear_bits",cc_linear_bits)))
 		= undef
 */
-	#!fi_group_index = max_group_index 0 prods fi_group_index ti_fun_defs ti_fun_heap ti_cons_args
-	# (Yes fun_type=:{st_vars,st_attr_vars,st_args,st_result}) = fd.fun_type
-	  th_vars = foldSt (\tv type_var_heap -> type_var_heap <:= (tv.tv_info_ptr, TVI_Type (TV tv))) st_vars ti_type_heaps.th_vars 
-	  th_attrs = foldSt (\av attr_var_heap -> attr_var_heap <:= (av.av_info_ptr, AVI_Attr TA_Multi)) st_attr_vars ti_type_heaps.th_attrs 
-	  ti_type_heaps = { ti_type_heaps & th_attrs = th_attrs, th_vars = th_vars }
-	  
-	  (new_fun_args, new_arg_types_array, new_result_type, new_type_vars, new_linear_bits, new_cons_args, ti_type_heaps, ti_symbol_heap, ti_fun_defs, ti_fun_heap, ti_var_heap)
-			= determine_args cc_linear_bits cc_args 0 prods tb_args (st_args_array st_args) st_result st_vars (ti_cons_args, tb_rhs, ro) ti_type_heaps
-							 ti_symbol_heap ti_fun_defs ti_fun_heap ti_var_heap
+	#!fi_group_index
+			= max_group_index 0 prods fi_group_index ti_fun_defs ti_fun_heap ti_cons_args
+	# (Yes consumer_symbol_type) 
+			= fd.fun_type
+	  (function_producer_types, ti_fun_defs, ti_fun_heap)
+	  		= iFoldSt (accum_function_producer_type prods ro) 0 (size prods) 
+	  				([], ti_fun_defs, ti_fun_heap)
+	  (fresh_function_producer_types, ti_type_heaps)
+	  		= mapSt copy_opt_symbol_type function_producer_types ti_type_heaps
+	  ([Yes sound_consumer_symbol_type:opt_sound_function_producer_types], (ti_type_heaps, ti_type_def_infos))
+	  		= mapSt (add_propagation_attributes ro.ro_common_defs) [Yes consumer_symbol_type: fresh_function_producer_types]
+	  				(ti_type_heaps, ti_type_def_infos)
+	  ({st_vars,st_attr_vars,st_args,st_result,st_attr_env})
+	  		= sound_consumer_symbol_type
+/* HACK..
+	  (st_attr_vars, th_attrs)
+	  		= getAttrVars (st_args, st_result) ti_type_heaps.th_attrs
+	  ti_type_heaps = { ti_type_heaps & th_attrs = th_attrs }
+// ..HACK
+*/
+	  (class_types, ti_fun_defs, ti_fun_heap)
+	  		= iFoldSt (accum_class_type prods ro) 0 (size prods) 
+	  				([], ti_fun_defs, ti_fun_heap)
+	  (type_vars_in_class_types, th_vars)
+	  		= mapSt getTypeVars class_types ti_type_heaps.th_vars
+	  sound_function_producer_types
+	  		= [x \\ Yes x <- opt_sound_function_producer_types]
+	  all_involved_types
+	  		= class_types ++ (flatten (map (\{st_args, st_result}-> [st_result:st_args]) 
+					  					[sound_consumer_symbol_type:sound_function_producer_types]))
+	  (propagating_cons_vars, th_vars)
+	  		= collectPropagatingConsVars all_involved_types th_vars
+	  all_type_vars
+	  		=   flatten [st_vars \\ {st_vars} <- [sound_consumer_symbol_type:sound_function_producer_types]]
+	  		  ++flatten type_vars_in_class_types
+	  (nr_of_all_type_vars, th_vars)
+	  		=  foldSt bind_to_temp_type_var all_type_vars (0, th_vars)
+	  subst
+	  		= createArray nr_of_all_type_vars TE
+	  (next_attr_nr, th_attrs)
+	  		= foldSt bind_to_temp_attr_var st_attr_vars (FirstAttrVar, ti_type_heaps.th_attrs)
+	  ti_type_heaps
+	  		= { ti_type_heaps & th_attrs = th_attrs, th_vars = th_vars }
+	  ((st_args,st_result), ti_type_heaps)
+	  		= substitute (st_args,st_result) ti_type_heaps
+	  (new_fun_args, new_arg_types_array, next_attr_nr,
+	    new_linear_bits, new_cons_args, uniqueness_requirements, subst, ti_type_heaps=:{th_vars, th_attrs},
+	    ti_symbol_heap, ti_fun_defs, ti_fun_heap, ti_var_heap)
+			= determine_args cc_linear_bits cc_args 0 prods opt_sound_function_producer_types tb_args
+							(st_args_array st_args)
+							next_attr_nr (ti_cons_args, tb_rhs, ro) [] subst ti_type_heaps
+							ti_symbol_heap ti_fun_defs ti_fun_heap ti_var_heap
 	  new_arg_types = flatten [ el \\ el<-:new_arg_types_array ]
-	  (fresh_type_vars, ti_type_heaps) = accTypeVarHeap (mapSt bind_to_fresh_type_variable new_type_vars) ti_type_heaps
-	  (fresh_arg_types, ti_type_heaps) = substitute new_arg_types ti_type_heaps
-	  (fresh_result_type, ti_type_heaps) = substitute new_result_type ti_type_heaps
-	  fun_arity = length new_fun_args
-	  new_fun_type = Yes { st_vars = fresh_type_vars, st_args = fresh_arg_types, st_arity = fun_arity,
-							st_result = fresh_result_type, st_context = [], st_attr_vars = [], st_attr_env = [] }
-
-	  new_fd_expanding = { fd & fun_body = Expanding new_fun_args, fun_arity = fun_arity,fun_type=new_fun_type, fun_index=ti_next_fun_nr,
-								fun_info.fi_group_index = fi_group_index}
-	  new_gen_fd = { gf_fun_def = new_fd_expanding,	gf_instance_info = II_Empty, gf_fun_index = ti_next_fun_nr,
-					 gf_cons_args = {cc_args = new_cons_args, cc_size = length new_cons_args, cc_linear_bits=new_linear_bits} }
-	  ti_fun_heap = writePtr fun_def_ptr (FI_Function new_gen_fd) ti_fun_heap
-	  us = { us_var_heap = ti_var_heap, us_symbol_heap = ti_symbol_heap, us_opt_type_heaps = Yes ti_type_heaps,
-			 us_cleanup_info=ti_cleanup_info }
-	  ui = {ui_handle_aci_free_vars = RemoveThem, ui_convert_module_n= -1,ui_conversion_table=No }
-	  (tb_rhs, {us_var_heap,us_symbol_heap,us_opt_type_heaps=Yes type_heaps, us_cleanup_info}) = unfold tb_rhs ui us
-	  ro =	{ ro &	ro_root_case_mode = case tb_rhs of 
-	  					Case _
-	  						-> RootCase
-	  					_	-> NotRootCase,
-					ro_fun= { symb_name = fd.fun_symb, symb_kind = SK_GeneratedFunction fun_def_ptr ti_next_fun_nr, symb_arity = fun_arity},
-					ro_fun_args = new_fun_args
-			}
-	  ti_trace=False
+	  (cons_vars, th_vars)
+			= foldSt set_cons_var_bit propagating_cons_vars
+					(createArray (inc (BITINDEX nr_of_all_type_vars)) 0, th_vars)
+//	| False--->("subst before", [el\\el<-:subst], "cons_vars", [el\\el<-:cons_vars])
+//		= undef
+	# (subst, next_attr_nr, th_vars, ti_type_def_infos)
+	  		= liftSubstitution subst ro.ro_common_defs cons_vars next_attr_nr th_vars ti_type_def_infos
+//	| False--->("subst after lifting", [el\\el<-:subst])
+//		= undef
+	# coer_demanded
+	  		= {{ CT_Empty \\ i <- [0 .. next_attr_nr - 1] } & [AttrUni] = CT_Unique }
+	  coer_offered
+	  		= {{ CT_Empty \\ i <- [0 .. next_attr_nr - 1] } & [AttrMulti] = CT_NonUnique }
+//	  			--->(("next_attr_nr", next_attr_nr)
+//	  			--->("nr_of_all_type_vars", nr_of_all_type_vars))
+	  (consumer_attr_inequalities, th_attrs)
+			= mapSt substitute_attr_inequality st_attr_env th_attrs
+	  coercions 
+	  		= foldSt new_inequality consumer_attr_inequalities
+	  				{ coer_offered = coer_offered, coer_demanded = coer_demanded }
+	  coercions 
+	  		= foldSt (\{ur_attr_ineqs} coercions
+	  					-> foldSt new_inequality ur_attr_ineqs coercions)
+		  			uniqueness_requirements coercions
+	  (subst, coercions, ti_type_def_infos, ti_type_heaps)
+	  		= foldSt (coerce_types ro.ro_common_defs cons_vars) uniqueness_requirements
+	  				(subst, coercions, ti_type_def_infos, { ti_type_heaps & th_vars = th_vars, th_attrs = th_attrs })
+//	| False--->("cons_vars", [el\\el<-:cons_vars])
+//		= undef
+//	  expansion_state
+//	  		= { es_type_heaps = ti_type_heaps, es_td_infos = ti_type_def_infos }
+//	# ([st_result:new_arg_types], (coercions, subst, { es_type_heaps = ti_type_heaps=:{th_vars}, es_td_infos = ti_type_def_infos }))
+//	  		= mapSt (expand_type ro.ro_common_defs cons_vars) [st_result:new_arg_types] (subst, expansion_state)
+	# ([st_result:new_arg_types], (coercions, subst, ti_type_heaps=:{th_vars}, ti_type_def_infos))
+	  		= mapSt (expand_type ro.ro_common_defs cons_vars) [st_result:new_arg_types]
+	  				(coercions, subst, ti_type_heaps, ti_type_def_infos)
+	  with
+		expand_type ro_common_defs cons_vars atype (coercions, subst, ti_type_heaps, ti_type_def_infos)
+			| is_dictionary atype ti_type_def_infos
+				# (atype, subst) = arraySubst atype subst
+				= (atype, (coercions, subst, ti_type_heaps, ti_type_def_infos))
+			# es
+		  			= { es_type_heaps = ti_type_heaps, es_td_infos = ti_type_def_infos }
+			  (btype, (subst, es))
+			  		= expandType ro_common_defs cons_vars atype (subst, es)
+	 		  { es_type_heaps = ti_type_heaps, es_td_infos = ti_type_def_infos }
+					= es
+			  cs
+					= { crc_type_heaps = ti_type_heaps, crc_coercions = coercions, crc_td_infos = ti_type_def_infos }
+			# (_, cs)
+			  		= coerce PositiveSign ro_common_defs cons_vars [] btype btype cs
+			  { crc_type_heaps = ti_type_heaps, crc_coercions = coercions, crc_td_infos = ti_type_def_infos }
+			  		= cs
+			= (btype, (coercions, subst, ti_type_heaps, ti_type_def_infos))
+/*
+	| False--->("unified type", new_arg_types, "->", st_result)
+		= undef
+	| False--->("coercions", readableCoercions coercions)
+		= undef
+*/
+	# (fresh_type_vars, th_vars) 
+			= iFoldSt allocate_fresh_type_var 0 nr_of_all_type_vars ([], th_vars)
+	  fresh_type_vars_array
+	  		= { el \\ el <- fresh_type_vars }
+	  (attr_partition, demanded) 
+	  		= partitionateAttributes coercions.coer_offered coercions.coer_demanded
+	  		// to eliminate circles in the attribute inequalities graph that was built during "determine_args"
+	  (fresh_attr_vars, ti_type_heaps)
+	  		= accAttrVarHeap (create_fresh_attr_vars demanded (size demanded)) { ti_type_heaps & th_vars = th_vars }
+	  		// the attribute variables stored in the "demanded" graph are represented as integers: 
+	  		// prepare to replace them by pointers
+	  ((fresh_arg_types, fresh_result_type), used_attr_vars) 
+	  		= replaceIntegers (new_arg_types, st_result) (fresh_type_vars_array, fresh_attr_vars, attr_partition)
+	  				 (createArray (size demanded) False)
+			// replace the integer-attribute-variables with pointer-attribute-variables or TA_Unique or TA_Multi
+	  final_coercions 
+	  		= removeUnusedAttrVars demanded [i \\ i<-[0..(size used_attr_vars)-1] | not used_attr_vars.[i]]
+			// the attribute inequalities graph may have contained unused attribute variables.
+ 	  (all_attr_vars2, th_attrs)
+ 	  		= getAttrVars (fresh_arg_types, fresh_result_type) ti_type_heaps.th_attrs
+	  all_attr_vars
+	  		= [ attr_var \\ TA_Var attr_var
+	  							<- [fresh_attr_vars.[i] \\ i<-[0..(size used_attr_vars)-1] | used_attr_vars.[i]]]
+// sanity.. remove! (XXX)
+	| any (\attr_var -> not (isMember attr_var all_attr_vars2)) all_attr_vars ||
+	  any (\attr_var -> not (isMember attr_var all_attr_vars)) all_attr_vars2
+		= abort "sanity chek 046 in m trans failed"
+// ..sanity
+ 	# (all_fresh_type_vars, th_vars)
+ 	  		= getTypeVars (fresh_arg_types, fresh_result_type) ti_type_heaps.th_vars
+	  fun_arity
+	  		= length new_fun_args
+	  new_fun_type
+	  		= Yes { st_vars = all_fresh_type_vars, st_args = fresh_arg_types, st_arity = fun_arity,
+					st_result = fresh_result_type, st_context = [], st_attr_vars = all_attr_vars,
+					st_attr_env = coercionsToAttrEnv fresh_attr_vars final_coercions }
+	  new_fd_expanding 
+	  		= { fd & fun_body = Expanding new_fun_args, fun_arity = fun_arity,fun_type=new_fun_type, fun_index = ti_next_fun_nr,
+					fun_info.fi_group_index = fi_group_index}
+	  new_gen_fd
+	  		= { gf_fun_def = new_fd_expanding,	gf_instance_info = II_Empty, gf_fun_index = ti_next_fun_nr,
+				 gf_cons_args = {cc_args = new_cons_args, cc_size = length new_cons_args, cc_linear_bits=new_linear_bits} }
+	  ti_fun_heap
+	  		= writePtr fun_def_ptr (FI_Function new_gen_fd) ti_fun_heap
+	  (subst, _)
+	  		= iFoldSt (replace_integers_in_substitution (fresh_type_vars_array, fresh_attr_vars, attr_partition))
+	  				0 nr_of_all_type_vars (subst, createArray (size demanded) False)
+	  (_, th_vars)
+	  		= foldSt (\{tv_info_ptr} (i, th_vars) 
+	  					-> case subst.[i] of
+	  						TE
+	  							-> (i+1, writePtr tv_info_ptr (TVI_Type (TV fresh_type_vars_array.[i])) th_vars)
+	  						_
+	  							-> (i+1, writePtr tv_info_ptr (TVI_Type subst.[i]) th_vars))
+	  				all_type_vars (0, th_vars)
+	  us 	
+	  		= { us_var_heap = ti_var_heap, us_symbol_heap = ti_symbol_heap,
+	  			us_opt_type_heaps = Yes { ti_type_heaps & th_vars = th_vars, th_attrs = th_attrs },
+				 us_cleanup_info=ti_cleanup_info }
+ 	  ui	
+ 	  		= {ui_handle_aci_free_vars = RemoveThem, ui_convert_module_n= -1,ui_conversion_table=No }
+	  (tb_rhs, {us_var_heap,us_symbol_heap,us_opt_type_heaps=Yes ti_type_heaps, us_cleanup_info})
+	  		= unfold tb_rhs ui us
+	  ro 	=	{ ro &	ro_root_case_mode = case tb_rhs of 
+	  						Case _
+	  							-> RootCase
+	  						_	-> NotRootCase,
+						ro_fun= { symb_name = fd.fun_symb, symb_kind = SK_GeneratedFunction fun_def_ptr ti_next_fun_nr, symb_arity = fun_arity},
+						ro_fun_args = new_fun_args
+				}
+	  ti_trace
+	  		=False
 	| ti_trace && (False--->("transforming new function:",tb_rhs))
 		= undef
-	# (new_fun_rhs, ti) = transform tb_rhs ro { ti & ti_var_heap = us_var_heap, ti_fun_heap = ti_fun_heap, ti_symbol_heap = us_symbol_heap,
-	  			ti_next_fun_nr = inc ti_next_fun_nr, ti_new_functions = [fun_def_ptr : ti_new_functions],
-				ti_type_heaps = type_heaps, ti_fun_defs=ti_fun_defs,ti_cleanup_info = us_cleanup_info, ti_trace=ti_trace }
-	  new_fd = { new_fd_expanding & fun_body = TransformedBody {tb_args = new_fun_args, tb_rhs = new_fun_rhs} }
-//	| (False--->("generated function", new_fd, '\n', new_fd.fun_type))
+	# ti
+			= { ti & ti_var_heap = us_var_heap, ti_fun_heap = ti_fun_heap, ti_symbol_heap = us_symbol_heap,
+	  			ti_next_fun_nr = inc ti_next_fun_nr, ti_type_def_infos = ti_type_def_infos,
+	  			ti_new_functions = [fun_def_ptr : ti_new_functions], ti_fun_defs = ti_fun_defs,
+	  			ti_type_heaps = ti_type_heaps, ti_cleanup_info = us_cleanup_info, ti_trace=ti_trace }
+	  (new_fun_rhs, ti)
+			= transform tb_rhs ro ti
+	  new_fd
+	  		= { new_fd_expanding & fun_body = TransformedBody {tb_args = new_fun_args, tb_rhs = new_fun_rhs} }
+//	| (False--->("generated function", new_fd.fun_symb, '\n', new_fd.fun_type, new_cons_args))
 //		= undef
 	= (ti_next_fun_nr, fun_arity, { ti & ti_fun_heap = ti.ti_fun_heap <:= (fun_def_ptr, FI_Function { new_gen_fd & gf_fun_def = new_fd })})
 where
+	is_dictionary {at_type=TA {type_index} _} es_td_infos
+		= type_index.glob_object>=size es_td_infos.[type_index.glob_module]
+	is_dictionary _ es_td_infos
+		= False
+
 	st_args_array :: ![AType] -> .{![AType]}
 	st_args_array st_args
 		= { [el] \\ el <- st_args }
 		
-	determine_args _ [] prod_index producers forms arg_types result_type type_vars _ type_heaps symbol_heap fun_defs fun_heap var_heap
+	determine_args _ [] prod_index producers prod_atypes forms arg_types next_attr_nr _ 
+				uniqueness_requirements subst type_heaps symbol_heap fun_defs fun_heap var_heap
 		# (vars, var_heap) = new_variables forms var_heap
-		= (vars, arg_types, result_type, type_vars, [], [], type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
-	determine_args [linear_bit : linear_bits] [cons_arg : cons_args ] prod_index producers [form : forms] arg_types result_type
-					type_vars input type_heaps symbol_heap fun_defs fun_heap var_heap
+		= (vars, arg_types, next_attr_nr, [], [], uniqueness_requirements, 
+			subst, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
+	determine_args [linear_bit : linear_bits] [cons_arg : cons_args ] prod_index producers [prod_atype:prod_atypes]
+					[form : forms] arg_types next_attr_nr
+					input uniqueness_requirements subst type_heaps symbol_heap fun_defs fun_heap var_heap
 		| cons_arg == cActive
-			# new_args = determine_args linear_bits cons_args (inc prod_index) prods forms arg_types result_type type_vars input type_heaps 
+			# new_args = determine_args linear_bits cons_args (inc prod_index) prods prod_atypes forms arg_types
+									next_attr_nr input uniqueness_requirements subst type_heaps 
 									symbol_heap fun_defs fun_heap var_heap
-			= determine_arg producers.[prod_index] form prod_index ((linear_bit,cons_arg), input) new_args
-			# (vars, arg_types, result_type, type_vars, new_linear_bits, new_cons_args, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap) 
-					= determine_args linear_bits cons_args (inc prod_index) prods forms arg_types result_type type_vars input type_heaps symbol_heap fun_defs fun_heap var_heap
+			= determine_arg producers.[prod_index] prod_atype form prod_index ((linear_bit,cons_arg), input) new_args
+			# (vars, arg_types, next_attr_nr, new_linear_bits, new_cons_args, uniqueness_requirements, subst,
+				type_heaps, symbol_heap, fun_defs, fun_heap, var_heap) 
+					= determine_args linear_bits cons_args (inc prod_index) prods prod_atypes forms
+									arg_types next_attr_nr
+									input uniqueness_requirements subst type_heaps symbol_heap fun_defs fun_heap var_heap
 			  (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
-			= ([{ form & fv_info_ptr = new_info_ptr } : vars], arg_types, result_type, type_vars, [linear_bit : new_linear_bits], [cons_arg : new_cons_args], type_heaps, symbol_heap, fun_defs,
-					fun_heap, writeVarInfo form.fv_info_ptr (VI_Variable form.fv_name new_info_ptr) var_heap)
+			= ([{ form & fv_info_ptr = new_info_ptr } : vars], arg_types, next_attr_nr, 
+				[linear_bit : new_linear_bits], [cons_arg : new_cons_args], uniqueness_requirements, subst, type_heaps, symbol_heap, fun_defs,
+				fun_heap, writeVarInfo form.fv_info_ptr (VI_Variable form.fv_name new_info_ptr) var_heap)
 	where
 		build_var_args [] form_vars act_vars var_heap
 			= (form_vars, act_vars, var_heap)
@@ -1301,54 +1497,96 @@ where
 			  act_var = { var_name = new_name, var_info_ptr = info_ptr, var_expr_ptr = nilPtr }
 			= build_var_args new_names [form_var : form_vars] [Var act_var : act_vars] var_heap
 
-		determine_arg PR_Empty form=:{fv_name,fv_info_ptr} _ ((linear_bit,cons_arg), _)
-						(vars, arg_types, result_type, type_vars, new_linear_bits, new_cons_args, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
+		determine_arg PR_Empty _ form=:{fv_name,fv_info_ptr} _ ((linear_bit,cons_arg), _)
+						(vars, arg_types, next_attr_nr, new_linear_bits,
+							new_cons_args, uniqueness_requirements, subst, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
 			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
-			= (	[{ form & fv_info_ptr = new_info_ptr } : vars], arg_types, result_type, type_vars,
-				[linear_bit : new_linear_bits], [cons_arg /* was cActive*/ : new_cons_args], type_heaps, symbol_heap, fun_defs, fun_heap,
+			= (	[{ form & fv_info_ptr = new_info_ptr } : vars], arg_types, next_attr_nr,
+				[linear_bit : new_linear_bits], [cons_arg /* was cActive*/ : new_cons_args], uniqueness_requirements, subst, type_heaps, symbol_heap, fun_defs, fun_heap,
 				writeVarInfo fv_info_ptr (VI_Variable fv_name new_info_ptr) var_heap)
 
-		determine_arg (PR_Class class_app free_vars class_type) {fv_info_ptr,fv_name} prod_index (_,(_, _, ro))
-					  (vars, arg_types, result_type, type_vars, new_linear_bits, new_cons_args, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
-			# (arg_type, arg_types) = arg_types![prod_index]
-			  empty_atype = { at_attribute = TA_Multi, at_annotation = AN_None, at_type = TE }
-			  (unbounded_type_vars, type_heaps)
-			  		= createBindingsForUnifiedTypes { empty_atype & at_type = class_type } (hd arg_type)
-			  										((getTypeVars class_type)++type_vars) ro.ro_common_defs type_heaps
-			  (arg_types, type_heaps) = substituteArr { arg_types & [prod_index] = repeatn (length free_vars) empty_atype} type_heaps
-			  (result_type, type_heaps) = substitute result_type type_heaps
+		determine_arg (PR_Class class_app free_vars class_type) _ {fv_info_ptr,fv_name} prod_index (_,(_, _, ro))
+					  (vars, arg_types, next_attr_nr, new_linear_bits, new_cons_args, 
+						uniqueness_requirements, subst, type_heaps, symbol_heap, fun_defs, fun_heap, var_heap)
+			# (arg_type, arg_types)
+					= arg_types![prod_index]
+			  (int_class_type, type_heaps)
+			  		= substitute class_type type_heaps
+			  type_input
+			  		= { ti_common_defs = ro.ro_common_defs
+			  		  , ti_functions = ro.ro_imported_funs
+					  ,	ti_main_dcl_module_n = ro.ro_main_dcl_module_n
+					  }
+			  (succ, subst, type_heaps)
+			  		= case isEmptyType int_class_type || isEmptyType (hd arg_type).at_type of
+			  			True
+			  				-> (True, subst, type_heaps)
+			  			_
+			  				-> unify { empty_atype & at_type = int_class_type } (hd arg_type) type_input subst type_heaps
+			  with
+				isEmptyType TE = True
+				isEmptyType _ = False
+			| not succ
+				= abort ("sanity check nr 93 in module trans failed"--->({ empty_atype & at_type = int_class_type }, (hd arg_type)))
+// XXX sanity check: remove later..
+			# (attr_vars, type_heaps) = accAttrVarHeap (getAttrVars (class_type, hd arg_type)) type_heaps
+			| not (isEmpty attr_vars)
+				= abort "sanity check nr 78 in module trans failed"
+// ..sanity check
 			= ( mapAppend (\{var_info_ptr,var_name} 
 							-> { fv_name = var_name, fv_info_ptr = var_info_ptr, fv_def_level = NotALevel, fv_count = 0 })
 						  free_vars vars
-			  , arg_types
-			  , result_type
-			  , unbounded_type_vars
+			  , { arg_types & [prod_index] = repeatn (length free_vars) empty_atype}
+			  , next_attr_nr
 			  , mapAppend (\_ -> True) free_vars new_linear_bits
 			  , mapAppend (\_ -> cActive) free_vars new_cons_args
+			  , uniqueness_requirements
+			  , subst
 			  , type_heaps
 			  , symbol_heap
 			  , fun_defs
 			  , fun_heap
 			  , writeVarInfo fv_info_ptr (VI_Dictionary class_app.app_symb class_app.app_args class_type) var_heap
 			  )
-		determine_arg producer {fv_info_ptr,fv_name} prod_index ((linear_bit, _),(ti_cons_args, consumer_body_rhs, ro))
-						(vars, arg_types, result_type, type_vars, new_linear_bits, new_cons_args, type_heaps=:{th_vars, th_attrs}, symbol_heap, fun_defs, fun_heap, var_heap)
-			# symbol = get_producer_symbol producer
-			  (symbol_type, fun_defs, fun_heap)
-					= get_producer_type symbol ro fun_defs fun_heap
-			  curried = is_curried producer
-			#! size_fun_defs = size fun_defs
-			# ({cc_args, cc_linear_bits}, fun_heap) = calc_cons_args curried symbol ti_cons_args linear_bit size_fun_defs fun_heap
-			  nr_of_applied_args = symbol.symb_arity
-			  application_type = build_application_type symbol_type nr_of_applied_args
-			  (arg_type, arg_types) = arg_types![prod_index]
-			  th_attrs = foldSt (\av attr_var_heap -> attr_var_heap <:= (av.av_info_ptr, AVI_Attr TA_Multi)) symbol_type.st_attr_vars th_attrs 
-			  (unbounded_type_vars, type_heaps) 
-			  		= createBindingsForUnifiedTypes application_type (hd arg_type) (symbol_type.st_vars++type_vars) 
-			  								ro.ro_common_defs { th_vars = th_vars, th_attrs = th_attrs }
-			  (arg_types, type_heaps) = substituteArr { arg_types & [prod_index] = take nr_of_applied_args symbol_type.st_args }
-					  								type_heaps
-			  (result_type, type_heaps) = substitute result_type type_heaps
+		determine_arg producer (Yes {st_args, st_result, st_attr_vars, st_context, st_attr_env, st_arity})
+						{fv_info_ptr,fv_name} prod_index 
+						((linear_bit, _),(ti_cons_args, consumer_body_rhs, ro))
+						(vars, arg_types, next_attr_nr, new_linear_bits, new_cons_args, 
+							uniqueness_requirements, subst, type_heaps=:{th_vars, th_attrs}, symbol_heap,
+							fun_defs, fun_heap, var_heap)
+			# symbol
+					= get_producer_symbol producer
+			  curried
+			  		= is_curried producer
+			#! size_fun_defs
+					= size fun_defs
+			# ({cc_args, cc_linear_bits}, fun_heap)
+					= calc_cons_args curried symbol ti_cons_args linear_bit size_fun_defs fun_heap
+			  (arg_type, arg_types)
+			  		= arg_types![prod_index]
+			  (next_attr_nr, th_attrs)
+			  		= foldSt bind_to_temp_attr_var st_attr_vars (next_attr_nr, th_attrs)
+			  		// prepare for substitute calls
+			  ((st_args, st_result), type_heaps)
+			  		= substitute (st_args, st_result) { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
+			  nr_of_applied_args
+			  		= symbol.symb_arity
+			  application_type
+			  		= build_application_type st_arity (length st_context) st_result st_args nr_of_applied_args
+			  type_input
+			  		= { ti_common_defs = ro.ro_common_defs
+			  		  , ti_functions = ro.ro_imported_funs
+					  ,	ti_main_dcl_module_n = ro.ro_main_dcl_module_n
+					  }
+			  (succ, subst, type_heaps)
+			  		= unify application_type (hd arg_type) type_input subst type_heaps
+			| not succ
+				= abort "sanity check nr 94 in module trans failed"
+			# (attr_inequalities, type_heaps)
+					= accAttrVarHeap (mapSt substitute_attr_inequality st_attr_env) type_heaps
+			  new_uniqueness_requirement
+			  		= { ur_offered = application_type, ur_demanded = hd arg_type,
+			  			ur_attr_ineqs = attr_inequalities }
 			  (opt_body, var_names, fun_defs, fun_heap)
 			  		= case producer of
 			  			(PR_Curried {symb_arity, symb_kind=SK_Function {glob_module}})
@@ -1370,13 +1608,14 @@ where
 							# (TransformedBody tb) = opt_body
 							-> (VI_Body symbol tb (take nr_of_applied_args form_vars), var_heap)
 			| nr_of_applied_args<>length cc_linear_bits || nr_of_applied_args<>length cc_args
-				= abort "Martin REALLY missed something XXX"
+				= abort ("Martin REALLY missed something XXX")
 			= (	form_vars
-			  , arg_types
-			  , result_type
-			  , unbounded_type_vars
+			  , { arg_types & [prod_index] = take nr_of_applied_args st_args }
+			  , next_attr_nr
 			  , cc_linear_bits++new_linear_bits
 			  , cc_args++new_cons_args
+			  , [new_uniqueness_requirement:uniqueness_requirements]
+			  , subst
 			  , type_heaps
 			  , symbol_heap
 			  , fun_defs
@@ -1385,28 +1624,20 @@ where
 			  ) 
 		  where
 			
-			get_producer_symbol (PR_Curried symbol)
-				= symbol
-			get_producer_symbol (PR_Function symbol _)
-				= symbol
-			get_producer_symbol (PR_GeneratedFunction symbol _)
-				= symbol
-			
-			get_producer_type {symb_kind=SK_Function {glob_module, glob_object}} ro fun_defs fun_heap
-				| glob_module == ro.ro_main_dcl_module_n
-					# ({fun_type=Yes symbol_type}, fun_defs) = fun_defs![glob_object]
-					= (symbol_type, fun_defs, fun_heap)
-				# {ft_type} = ro.ro_imported_funs.[glob_module].[glob_object]
-				  st_args = addTypesOfDictionaries ro.ro_common_defs ft_type.st_context ft_type.st_args
-				= ({ft_type & st_args = st_args, st_arity = length st_args, st_context = [] },
-					fun_defs, fun_heap)
-			get_producer_type {symb_kind=SK_LocalMacroFunction glob_object} ro fun_defs fun_heap
-				# ({fun_type=Yes symbol_type}, fun_defs) = fun_defs![glob_object]
-				= (symbol_type, fun_defs, fun_heap)
-			get_producer_type {symb_kind=SK_GeneratedFunction fun_ptr _} ro fun_defs fun_heap
-				# (FI_Function {gf_fun_def={fun_type=Yes symbol_type}}, fun_heap) = readPtr fun_ptr fun_heap
-				= (symbol_type, fun_defs, fun_heap)
-
+// XXX...
+			traceAttrEnv st_attr_env th_attrs
+				# th_attrs = th_attrs--->("producer attr inequalities")
+				  th_attrs = foldSt traceOne st_attr_env th_attrs
+				= forget th_attrs
+			  where
+				forget :: !x -> Bool
+				forget th_attrs = False
+				traceOne {ai_offered, ai_demanded} th_attrs
+					# (AVI_Attr (TA_TempVar o), th_attrs) = readPtr ai_offered.av_info_ptr th_attrs
+					  (AVI_Attr (TA_TempVar d), th_attrs) = readPtr ai_demanded.av_info_ptr th_attrs
+					  th_attrs = th_attrs--->("u"+++toString o+++" <= u"+++toString d)
+					= th_attrs 
+// ...XXX
 			calc_cons_args curried {symb_kind, symb_arity} ti_cons_args linear_bit size_fun_defs fun_heap
 				# (opt_cons_classes, fun_heap)
 						= case symb_kind of
@@ -1427,15 +1658,16 @@ where
 								-> (Yes gf_cons_args, fun_heap)
 				= case opt_cons_classes of
 					Yes cons_classes
-						| curried
-							-> ({ cc_size = symb_arity, cc_args = take symb_arity cons_classes.cc_args, 
-					  				cc_linear_bits = repeatn symb_arity linear_bit}, fun_heap)
-						-> (cons_classes, fun_heap)
+						-> ({ cc_size = symb_arity, cc_args = take symb_arity cons_classes.cc_args, 
+				  				cc_linear_bits = if curried (repeatn symb_arity linear_bit) 
+				  									(take symb_arity cons_classes.cc_linear_bits)}
+				  			, fun_heap)
 					No
 						-> ({cc_size = symb_arity, cc_args = repeatn symb_arity cPassive,
 								cc_linear_bits = repeatn symb_arity linear_bit}, fun_heap)
 
-			get_fun_def (SK_Function {glob_module, glob_object}) main_dcl_module_n fun_defs fun_heap
+
+ 			get_fun_def (SK_Function {glob_module, glob_object}) main_dcl_module_n fun_defs fun_heap
 				| glob_module<>main_dcl_module_n
 					= abort "sanity check 2 failed in module trans"
 				# (fun_def, fun_defs) = fun_defs![glob_object]
@@ -1450,26 +1682,158 @@ where
 			is_curried (PR_Curried _) = True
 			is_curried _ = False
 			
-		substituteArr :: !*{![AType]} !*TypeHeaps -> (!.{![AType]}, !.TypeHeaps)
-		// apply substitute on every array element
-		substituteArr arg_types type_heaps
-			#! size = size arg_types
-			= iFoldSt substitute_element 0 size (arg_types, type_heaps)
-		  where
-		  	substitute_element i (arg_types, type_heaps)
-		  		# (arg_type, arg_types) = arg_types![i]
-		  		  (arg_type, type_heaps) = substitute arg_type type_heaps
-				= ({ arg_types & [i] = arg_type }, type_heaps)
-
-		build_application_type :: !SymbolType !Int -> AType
-		build_application_type symbol_type=:{st_arity, st_context, st_result, st_args} nr_of_applied_args
-			# nr_context_args = length st_context
+		build_application_type st_arity nr_context_args st_result st_args nr_of_applied_args
 			| st_arity+nr_context_args==nr_of_applied_args
 				= st_result
 			| nr_of_applied_args<nr_context_args
 				= abort "sanity check nr 234 failed in module trans"
-			= foldr (\atype1 atype2->{at_attribute=TA_None, at_annotation=AN_None, at_type=atype1-->atype2})
-					st_result (drop (nr_of_applied_args-nr_context_args) st_args)
+			# (applied_args, unapplied_args) = splitAt (nr_of_applied_args-nr_context_args) st_args
+			  attr_approx = if (any has_unique_attribute applied_args) TA_Unique TA_Multi
+			= foldr (\atype1 atype2->{at_attribute=attr_approx, at_annotation=AN_None, at_type=atype1-->atype2})
+					st_result unapplied_args
+		  where
+			has_unique_attribute {at_attribute=TA_Unique} = True
+			has_unique_attribute _ = False
+
+	substitute_attr_inequality {ai_offered, ai_demanded} th_attrs
+		#! ac_offered = pointer_to_int ai_offered th_attrs
+		   ac_demanded = pointer_to_int ai_demanded th_attrs
+		= ({ ac_offered = ac_offered, ac_demanded = ac_demanded }, th_attrs)
+	  where
+		pointer_to_int {av_info_ptr} th_attrs
+			# (AVI_Attr (TA_TempVar i)) = sreadPtr av_info_ptr th_attrs
+			= i
+
+	new_inequality {ac_offered, ac_demanded} coercions
+		= newInequality ac_offered ac_demanded coercions
+
+	bind_to_temp_type_var {tv_info_ptr} (next_type_var_nr, th_vars)
+		= (next_type_var_nr+1, writePtr tv_info_ptr (TVI_Type (TempV next_type_var_nr)) th_vars)
+	
+	bind_to_temp_attr_var {av_info_ptr} (next_attr_var_nr, th_attrs)
+		= (next_attr_var_nr+1, writePtr av_info_ptr (AVI_Attr (TA_TempVar next_attr_var_nr)) th_attrs)
+
+	set_cons_var_bit {tv_info_ptr} (cons_vars, th_vars)
+		# (TVI_Type (TempV i), th_vars) = readPtr tv_info_ptr th_vars 
+		= (set_bit i cons_vars, th_vars)
+
+	copy_opt_symbol_type No ti_type_heaps
+		= (No, ti_type_heaps)
+	copy_opt_symbol_type (Yes symbol_type=:{st_vars, st_attr_vars, st_args, st_result, st_attr_env})
+				ti_type_heaps=:{th_vars, th_attrs}
+		# (fresh_st_vars, th_vars)
+				= mapSt bind_to_fresh_type_variable st_vars th_vars
+		  (fresh_st_attr_vars, th_attrs)
+				= mapSt bind_to_fresh_attr_variable st_attr_vars th_attrs
+		  ([fresh_st_result:fresh_st_args], ti_type_heaps)
+		  		= substitute [st_result:st_args] { ti_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
+		  (fresh_st_attr_env, ti_type_heaps)
+		  		= substitute st_attr_env ti_type_heaps
+		= (Yes { symbol_type & st_vars = fresh_st_vars, st_attr_vars = fresh_st_attr_vars, st_args = fresh_st_args,
+				st_result = fresh_st_result, st_attr_env = fresh_st_attr_env}, ti_type_heaps)
+
+	add_propagation_attributes ro_common_defs No state
+		= (No, state)
+	add_propagation_attributes ro_common_defs (Yes st=:{st_args, st_result, st_attr_env, st_attr_vars})
+				(ti_type_heaps, ti_type_def_infos)
+		# ([sound_st_result:sound_st_args], ps)
+			  	= add_propagation_attributes_to_atypes ro_common_defs [st_result:st_args]
+					{ prop_type_heaps = ti_type_heaps, prop_td_infos = ti_type_def_infos,
+					  prop_attr_vars = st_attr_vars, prop_attr_env = st_attr_env, prop_error = No }
+		  ({prop_type_heaps = ti_type_heaps, prop_td_infos = ti_type_def_infos, prop_attr_vars, prop_attr_env})
+		  		= ps
+		  sound_symbol_type
+		  		= { st & st_args = sound_st_args, st_result = sound_st_result, st_attr_env = prop_attr_env,
+		  			st_attr_vars = prop_attr_vars } 
+		= (Yes sound_symbol_type, (ti_type_heaps, ti_type_def_infos))
+
+	add_propagation_attributes_to_atypes :: {#CommonDefs} ![AType] !*PropState -> (![AType],!*PropState)
+	add_propagation_attributes_to_atypes modules types ps
+		= mapSt (add_propagation_attributes_to_atype modules) types ps
+
+	add_propagation_attributes_to_atype modules type ps
+		| is_dictionary type ps.prop_td_infos
+			= (type, ps)
+		# (type, prop_class, ps) = addPropagationAttributesToAType modules type ps
+		= (type, ps)
+	
+	empty_atype = { at_attribute = TA_Multi, at_annotation = AN_None, at_type = TE }
+
+	accum_class_type prods ro i (type_accu, ti_fun_defs, ti_fun_heap)
+		= case prods.[i] of
+			PR_Class _ _ class_type
+				-> ([{empty_atype & at_type = class_type}  : type_accu ], ti_fun_defs, ti_fun_heap)
+			_
+				-> (type_accu, ti_fun_defs, ti_fun_heap)
+
+
+	accum_function_producer_type prods ro i (type_accu, ti_fun_defs, ti_fun_heap)
+		= case prods.[size prods-i-1] of
+			PR_Empty
+				-> ([No:type_accu], ti_fun_defs, ti_fun_heap)
+			PR_Class _ _ class_type
+				-> ([No:type_accu], ti_fun_defs, ti_fun_heap)
+			producer
+				# symbol = get_producer_symbol producer
+				  (symbol_type, ti_fun_defs, ti_fun_heap)
+						= get_producer_type symbol ro ti_fun_defs ti_fun_heap
+				-> ([Yes symbol_type:type_accu], ti_fun_defs, ti_fun_heap)
+
+	coerce_types common_defs cons_vars {ur_offered, ur_demanded} (subst, coercions, ti_type_def_infos, ti_type_heaps)
+//		| False--->("determineAttributeCoercions", ur_offered, ur_demanded)
+//			= undef
+		# (opt_error_info, subst, coercions, ti_type_def_infos, ti_type_heaps)
+				= determineAttributeCoercions ur_offered ur_demanded True /*XXX True?*/
+						subst coercions common_defs cons_vars ti_type_def_infos ti_type_heaps
+		= case opt_error_info of
+			Yes _
+				-> abort "sanity check nr 5623 failed in module trans"
+			No
+				-> (subst, coercions, ti_type_def_infos, ti_type_heaps)
+
+	collectPropagatingConsVars type th_vars
+		# th_vars
+				= performOnTypeVars initializeToTVI_Empty type th_vars
+		= performOnTypeVars collect_unencountered_cons_var type ([], th_vars)
+	  where
+		collect_unencountered_cons_var TA_MultiOfPropagatingConsVar tv=:{tv_info_ptr} (cons_var_accu, th_vars)
+			# (tvi, th_vars) = readPtr tv_info_ptr th_vars
+			= case tvi of
+				TVI_Empty
+					-> ([tv:cons_var_accu], writePtr tv_info_ptr TVI_Used th_vars)
+				TVI_Used
+					-> (cons_var_accu, th_vars)
+		collect_unencountered_cons_var _ _ state
+			= state
+
+	get_producer_symbol (PR_Curried symbol)
+		= symbol
+	get_producer_symbol (PR_Function symbol _)
+		= symbol
+	get_producer_symbol (PR_GeneratedFunction symbol _)
+		= symbol
+
+	replace_integers_in_substitution replace_input i (subst, used)
+		# (subst_i, subst)
+				= subst![i]
+		  (subst_i, used)
+		  		= replaceIntegers subst_i replace_input used
+		= ({ subst & [i] = subst_i }, used)
+
+	get_producer_type {symb_kind=SK_Function {glob_module, glob_object}} ro fun_defs fun_heap
+		| glob_module == ro.ro_main_dcl_module_n
+			# ({fun_type=Yes symbol_type}, fun_defs) = fun_defs![glob_object]
+			= (symbol_type, fun_defs, fun_heap)
+		# {ft_type} = ro.ro_imported_funs.[glob_module].[glob_object]
+		  st_args = addTypesOfDictionaries ro.ro_common_defs ft_type.st_context ft_type.st_args
+		= ({ft_type & st_args = st_args, st_arity = length st_args, st_context = [] },
+			fun_defs, fun_heap)
+	get_producer_type {symb_kind=SK_LocalMacroFunction glob_object} ro fun_defs fun_heap
+		# ({fun_type=Yes symbol_type}, fun_defs) = fun_defs![glob_object]
+		= (symbol_type, fun_defs, fun_heap)
+	get_producer_type {symb_kind=SK_GeneratedFunction fun_ptr _} ro fun_defs fun_heap
+		# (FI_Function {gf_fun_def={fun_type=Yes symbol_type}}, fun_heap) = readPtr fun_ptr fun_heap
+		= (symbol_type, fun_defs, fun_heap)
 
 	new_variables [] var_heap
 		= ([], var_heap)
@@ -1503,24 +1867,6 @@ where
 		= max_group_index_of_fun_with_fun_index_and_ptr fun_ptr fun_index current_max fun_defs fun_heap
 	max_group_index_of_producer prod current_max fun_defs fun_heap cons_args
 		= abort ("trans.icl: max_group_index_of_producer" ---> prod)
-/* was
-	max_group_index_of_producer PR_Empty current_max fun_defs fun_heap cons_args
-		= current_max
-	max_group_index_of_producer (PR_Class {app_args} _ _) current_max fun_defs fun_heap cons_args
-		= max_group_index_of_members app_args current_max fun_defs fun_heap cons_args
-	max_group_index_of_producer (PR_Curried _) current_max fun_defs fun_heap cons_args
-		= current_max
-	max_group_index_of_producer (PR_Function _ fun_index) current_max fun_defs fun_heap cons_args
-		# (fun_def, fun_defs) = fun_defs![fun_index]
-		= max fun_def.fun_info.fi_group_index current_max
-	max_group_index_of_producer (PR_GeneratedFunction { symb_kind = SK_GeneratedFunction fun_ptr fun_index} _)
-								current_max fun_defs fun_heap cons_args
-		| fun_index < size fun_defs
-			# {fun_info} = fun_defs.[fun_index] 
-			= max fun_info.fi_group_index current_max
-			# (FI_Function generated_function) = sreadPtr fun_ptr fun_heap
-			= max generated_function.gf_fun_def.fun_info.fi_group_index current_max
-*/
 	ro_main_dcl_module_n = ro.ro_main_dcl_module_n
 
 	max_group_index_of_member fun_defs fun_heap cons_args current_max (App {app_symb = {symb_name, symb_kind = SK_Function { glob_object = fun_index, glob_module = mod_index}}}) 
@@ -1555,6 +1901,72 @@ where
 			# (FI_Function generated_function) = sreadPtr fun_ptr fun_heap
 			= max generated_function.gf_fun_def.fun_info.fi_group_index current_max
 
+	create_fresh_attr_vars :: !{!CoercionTree} !Int !*AttrVarHeap -> (!{!TypeAttribute}, !.AttrVarHeap)
+	create_fresh_attr_vars demanded nr_of_attr_vars th_attrs
+		# fresh_array = createArray nr_of_attr_vars TA_None
+		= iFoldSt (allocate_fresh_attr_var demanded) 0 nr_of_attr_vars (fresh_array, th_attrs)
+	  where
+		allocate_fresh_attr_var demanded i (attr_var_array, th_attrs)
+			= case demanded.[i] of
+				CT_Unique
+					-> ({ attr_var_array & [i] = TA_Unique}, th_attrs)
+				CT_NonUnique
+					-> ({ attr_var_array & [i] = TA_Multi}, th_attrs)
+				_
+					# (new_info_ptr, th_attrs) = newPtr AVI_Empty th_attrs
+					-> ({ attr_var_array & [i] = TA_Var { av_name = NewAttrVarId i, av_info_ptr = new_info_ptr }}, th_attrs)
+
+class replaceIntegers a :: !a !({!TypeVar}, !{!TypeAttribute}, !AttributePartition) !*{#Bool} -> (!a, !.{#Bool})
+	// get rid of all those TempV and TA_Var things
+
+instance replaceIntegers (a, b) | replaceIntegers a & replaceIntegers b where
+	replaceIntegers (a, b) input used
+		# (a, used) = replaceIntegers a input used
+		  (b, used) = replaceIntegers b input used
+		= ((a, b), used)
+
+instance replaceIntegers [a] | replaceIntegers a where
+	replaceIntegers [] input used
+		= ([], used)
+	replaceIntegers [h:t] input used
+		# (h, used) = replaceIntegers h input used
+		  (t, used) = replaceIntegers t input used
+		= ([h:t], used)
+
+instance replaceIntegers TypeAttribute where
+	replaceIntegers (TA_TempVar i) (_, attributes, attr_partition) used
+		# index = attr_partition.[i]
+		  attribute = attributes.[index]
+		= (attribute, { used & [index] = isAttrVar attribute })
+	  where
+		isAttrVar (TA_Var _) = True
+		isAttrVar _ = False
+	replaceIntegers ta _ used
+		= (ta, used)
+
+instance replaceIntegers Type where
+	replaceIntegers (TA type_symb_ident args) input used
+		# (args, used) = replaceIntegers args input used
+		= (TA type_symb_ident args, used)
+	replaceIntegers (a --> b) input used
+		# (a, used) = replaceIntegers a input used
+		  (b, used) = replaceIntegers b input used
+		= (a --> b, used)
+	replaceIntegers (consvar :@: args) input=:(fresh_type_vars, _, _) used
+		# (TempCV i) = consvar
+		  (args, used) = replaceIntegers args input used
+		= (CV fresh_type_vars.[i] :@: args, used)
+	replaceIntegers (TempV i) (fresh_type_vars, _, _) used
+		= (TV fresh_type_vars.[i], used)
+	replaceIntegers type input used
+		= (type, used)
+
+instance replaceIntegers AType where
+	replaceIntegers atype=:{at_attribute, at_type} input used
+		# (at_attribute, used) = replaceIntegers at_attribute input used
+		  (at_type, used) = replaceIntegers at_type input used
+		= ({atype & at_attribute = at_attribute, at_type = at_type}, used)
+		
 (-!->) infix :: !.a !b -> .a | <<< b
 (-!->) a b = a ---> b
 
@@ -1563,180 +1975,16 @@ bind_to_fresh_type_variable {tv_name, tv_info_ptr} th_vars
 	  tv = { tv_name=tv_name, tv_info_ptr=new_tv_info_ptr }
 	= (tv, writePtr tv_info_ptr (TVI_Type (TV tv)) th_vars)
 
-appTypeVarHeap f type_heaps :== let th_vars = f type_heaps.th_vars in { type_heaps & th_vars = th_vars }
-accTypeVarHeap f type_heaps :== let (r, th_vars) = f type_heaps.th_vars in (r, { type_heaps & th_vars = th_vars })
+bind_to_fresh_attr_variable {av_name, av_info_ptr} th_attrs
+	# (new_av_info_ptr, th_attrs) = newPtr AVI_Empty th_attrs
+	  av = { av_name=av_name, av_info_ptr=new_av_info_ptr }
+	= (av, writePtr av_info_ptr (AVI_Attr (TA_Var av)) th_attrs)
 
-createBindingsForUnifiedTypes :: !AType !AType ![TypeVar] !{#CommonDefs} !*TypeHeaps -> (![TypeVar], !.TypeHeaps)
-createBindingsForUnifiedTypes type_1 type_2 all_type_vars common_defs type_heaps=:{th_vars}
-/* unify the two type arguments and generate new bindings. The resulting list of type variables should only
-   contain variables that occur in the second type argument (the "demanded" type).
-*/
-//	| False --->("createBindingsForUnifiedTypes", type_1, type_2, all_type_vars)
-//		= undef
-	# th_vars = foldSt (\tv th_vars -> th_vars <:= (tv.tv_info_ptr, TVI_Empty)) all_type_vars th_vars
-	  (type_heaps=:{th_vars}) = bind_and_unify_atypes type_1 type_2 common_defs { type_heaps & th_vars = th_vars }
-//	  th_vars = th_vars -!-> ""
-//	  th_vars = foldSt trace_type_var all_type_vars th_vars
-	  th_vars = foldSt (\ a b -> snd (bind_to_root a b)) all_type_vars th_vars
-//	  th_vars = th_vars -!-> ""
-//	  th_vars = foldSt trace_type_var all_type_vars th_vars
-	  (unbound_type_vars, th_vars) = foldSt get_unbound_var all_type_vars ([], th_vars)
-//	  th_vars = th_vars -!-> ""
-//	  th_vars = foldSt trace_type_var all_type_vars th_vars
-	= (unbound_type_vars, { type_heaps & th_vars = th_vars })
-  where
-	bind_and_unify_types (TV tv_1) (TV tv_2) common_defs type_heaps=:{th_vars}
-		# (root_1, th_vars) = get_root tv_1 th_vars
-		  (root_2, th_vars) = get_root tv_2 th_vars
-		  maybe_root_tv_1 = only_tv root_1
-		  maybe_root_tv_2 = only_tv root_2
-		  type_heaps = { type_heaps & th_vars = th_vars }
-		= case (maybe_root_tv_1, maybe_root_tv_2) of
-						(Yes root_tv_1, No)
-							-> appTypeVarHeap (bind_root_variable_to_type root_tv_1 root_2) type_heaps
-						(No, Yes root_tv_2)
-							-> appTypeVarHeap (bind_root_variable_to_type root_tv_2 root_1) type_heaps
-						(Yes root_tv_1, Yes root_tv_2)
-							| root_tv_1.tv_info_ptr==root_tv_2.tv_info_ptr
-								-> type_heaps
-							-> appTypeVarHeap (bind_roots_together root_tv_1 root_2) type_heaps
-						(No, No)
-							-> bind_and_unify_types root_1 root_2 common_defs type_heaps
-	bind_and_unify_types (TV tv_1) type common_defs type_heaps=:{th_vars}
-		| not (is_non_variable_type type)
-			= abort ("compiler error in trans.icl: assertion failed (1) XXX"--->type)
-		# th_vars = bind_variable_to_type tv_1 type th_vars
-		= { type_heaps & th_vars = th_vars }
-	bind_and_unify_types type (TV tv_1) common_defs type_heaps=:{th_vars}
-		| not (is_non_variable_type type)
-			= abort ("compiler error in trans.icl: assertion failed (2) XXX"--->type)
-		# th_vars = bind_variable_to_type tv_1 type th_vars
-		= { type_heaps & th_vars = th_vars }
-	bind_and_unify_types (TA _ arg_types1) (TA _ arg_types2) common_defs type_heaps
-		= bind_and_unify_atype_lists arg_types1 arg_types2 common_defs type_heaps
-	bind_and_unify_types (l1 --> r1) (l2 --> r2) common_defs type_heaps
-		= bind_and_unify_atypes r1 r2 common_defs (bind_and_unify_atypes l1 l2 common_defs type_heaps)
-	bind_and_unify_types (TB _) (TB _) common_defs type_heaps
-		= type_heaps
-	bind_and_unify_types ((CV l1) :@: r1) ((CV l2) :@: r2) common_defs type_heaps
-		= bind_and_unify_atype_lists r1 r2 common_defs (bind_and_unify_types (TV l1) (TV l2) common_defs type_heaps)
-	bind_and_unify_types (TA type_symb r1) ((CV l2) :@: r2) common_defs type_heaps
-		= bind_and_unify_atype_lists r1 r2 common_defs (bind_and_unify_types (TA type_symb []) (TV l2) common_defs type_heaps)
-	bind_and_unify_types ((CV l1) :@: r1) (TA type_symb r2) common_defs type_heaps
-		= bind_and_unify_atype_lists r1 r2 common_defs (bind_and_unify_types (TV l1) (TA type_symb []) common_defs type_heaps)
-	bind_and_unify_types TE y common_defs type_heaps
-		= type_heaps
-	bind_and_unify_types x TE common_defs type_heaps
-		= type_heaps
-	bind_and_unify_types x y _ _
-		= abort ("bind_and_unify_types"--->(x,y))
-
-	bind_and_unify_atype_lists [] [] common_defs type_heaps
-		= type_heaps
-	bind_and_unify_atype_lists [x:xs] [y:ys] common_defs type_heaps
-		= bind_and_unify_atype_lists xs ys common_defs (bind_and_unify_atypes x y common_defs type_heaps)
-	
-	bind_and_unify_atypes {at_type=TA type_symb_1 type_args_1} {at_type=TA type_symb_2 type_args_2} common_defs type_heaps
-		| type_symb_1==type_symb_2
-			= bind_and_unify_atype_lists type_args_1 type_args_2 common_defs type_heaps
-		// otherwise further with next alternative ("functional GOTO")
-	bind_and_unify_atypes atype_1 atype_2 common_defs type_heaps
-		# (mb_expanded_1, type_heaps) = try_to_expand atype_1 common_defs type_heaps
-		  (mb_expanded_2, type_heaps) = try_to_expand atype_2 common_defs type_heaps
-		= bind_and_unify_types mb_expanded_1 mb_expanded_2 common_defs type_heaps
-	  where
-		try_to_expand {at_type=actual_type=:TA {type_index={glob_object,glob_module}} actual_args, at_attribute=actual_type_attr}
-						common_defs type_heaps
-			#! type_def = common_defs.[glob_module].com_type_defs.[glob_object]
-			= case type_def.td_rhs of
-				SynType {at_type=rhs_type}
-					-> expandTypeApplication type_def.td_args type_def.td_attribute rhs_type actual_args actual_type_attr type_heaps
-				_
-					-> (actual_type, type_heaps)
-		try_to_expand {at_type} _ type_heaps
-			= (at_type, type_heaps)
-
-	bind_to_root :: !TypeVar !*TypeVarHeap -> (!TypeVarInfo,!.TypeVarHeap);
-	bind_to_root this_tv th_vars
-		# (tv_info, th_vars) = readPtr this_tv.tv_info_ptr th_vars
-		= case tv_info of
-			TVI_Empty
-				-> (tv_info, th_vars)
-			(TVI_Type type)
-				| is_non_variable_type type
-					 -> (tv_info, th_vars)
-				-> case type of
-					(TV next_tv)
-						# (root_tvi, th_vars) = bind_to_root next_tv th_vars
-						-> case root_tvi of
-							TVI_Empty
-								// this_tv is already bound to the root which is a type variable itself
-								-> (tv_info, th_vars)
-							_
-								// the root type is root_tvi
-							 	-> (root_tvi, th_vars <:= (this_tv.tv_info_ptr, root_tvi))
-
-	get_unbound_var tv=:{tv_info_ptr} (unbound_type_vars_accu, th_vars)
-		# (tv_info, th_vars) = readPtr tv_info_ptr th_vars
-		= case tv_info of
-			TVI_Empty
-				-> ([tv:unbound_type_vars_accu], th_vars)
-			(TVI_Type type)
-				-> (unbound_type_vars_accu, th_vars)
-
-	only_tv :: Type -> Optional TypeVar
-	only_tv (TV tv) = Yes tv
-	only_tv _ = No
-	
-	is_non_variable_type (TA _ _)	= True
-	is_non_variable_type (_ --> _)	= True
-	is_non_variable_type (_ :@: _)	= True
-	is_non_variable_type (TB _)		= True
-	is_non_variable_type _			= False
-	
-	bind_variable_to_type tv type th_vars
-		# (root, th_vars) = get_root tv th_vars
-		= case (only_tv root) of
-			(Yes tv)	-> bind_root_variable_to_type tv type th_vars
-			No 			-> th_vars
-	
-	bind_root_variable_to_type {tv_info_ptr} type th_vars
-		= th_vars <:= (tv_info_ptr, TVI_Type type)
-	
-	bind_roots_together :: TypeVar Type *(Heap TypeVarInfo) -> .Heap TypeVarInfo;
-	bind_roots_together root_tv_1 root_type_2 th_vars
-		= th_vars <:= (root_tv_1.tv_info_ptr, TVI_Type root_type_2)
-	
-	get_root :: TypeVar *(Heap TypeVarInfo) -> (Type,.Heap TypeVarInfo);
-	get_root this_tv th_vars
-		# (tv_info, th_vars) = readPtr this_tv.tv_info_ptr th_vars
-		= case tv_info of
-			TVI_Empty
-				-> (TV this_tv, th_vars)
-			(TVI_Type type)
-				| is_non_variable_type type
-					 -> (type, th_vars)
-				-> case type of
-					(TV next_tv) -> get_root next_tv th_vars
-	// XXX for tracing
-	trace_type_var tv th_vars
-		= trace_type_vars tv (th_vars -!-> "TYPE VARIABLE")
-	
-	trace_type_vars this_tv th_vars
-		# th_vars = th_vars -!-> this_tv
-		# (tv_info, th_vars) = readPtr this_tv.tv_info_ptr th_vars
-		= case tv_info of
-			TVI_Empty
-				-> th_vars
-			(TVI_Type type)
-				| is_non_variable_type type
-					-> (th_vars -!-> ("TVI_Type", type))
-				-> case type of
-					(TV next_tv) -> trace_type_vars next_tv th_vars
-//			(TVI_FreshTypeVar root_type_var)
-//				-> th_vars -!-> ("TVI_FreshTypeVar",root_type_var)
+allocate_fresh_type_var i (accu, th_vars)
+	# (new_tv_info_ptr, th_vars) = newPtr TVI_Empty th_vars
+	  tv = { tv_name = { id_name = "a"+++toString i, id_info = nilPtr }, tv_info_ptr=new_tv_info_ptr }
+	= ([tv:accu], th_vars)
 
-	
 transformFunctionApplication fun_def instances cc=:{cc_size, cc_args, cc_linear_bits} app=:{app_symb,app_args} extra_args ro ti
 	# (app_symb, app_args, extra_args) = complete_application app_symb fun_def.fun_arity app_args extra_args
 	| cc_size > 0
@@ -1862,9 +2110,9 @@ where
 		= (producers, [arg : new_args], ti)
 
 // XXX check for linear_bit also in case of a constructor ?
-determineProducer _ _ {app_symb = {symb_arity}, app_args} _ new_args prod_index producers _ ti
+determineProducer _ _ app=:{app_symb = {symb_arity}, app_args} _ new_args prod_index producers _ ti
 	| symb_arity<>length app_args
-		= abort "XXX Martin missed something"
+		= abort "sanity check 98765 failed in module trans"
 determineProducer _ _ app=:{app_symb = symb=:{symb_kind = SK_Constructor _}, app_args} (EI_DictionaryType type) new_args prod_index producers _ ti
 	# (app_args, (new_vars, ti_var_heap)) = renewVariables app_args ([], ti.ti_var_heap)
 	  (new_args, ti_var_heap) = mapAppendSt retrieve_old_var new_vars new_args ti_var_heap
@@ -1975,26 +2223,26 @@ where
 ::	ImportedConstructors	:== [Global Index]
 
 transformGroups :: !CleanupInfo !Int !*{! Group} !*{#FunDef} !{!.ConsClasses} !{# CommonDefs}  !{# {# FunType} }
-		!*{#{# CheckedTypeDef}} !ImportedConstructors !*VarHeap !*TypeHeaps !*ExpressionHeap
+		!*{#{# CheckedTypeDef}} !ImportedConstructors !*TypeDefInfos !*VarHeap !*TypeHeaps !*ExpressionHeap
 			-> (!*{! Group}, !*{#FunDef}, !*{#{# CheckedTypeDef}}, !ImportedConstructors, !*VarHeap, !*TypeHeaps, !*ExpressionHeap)
-
-transformGroups cleanup_info main_dcl_module_n groups fun_defs cons_args common_defs imported_funs imported_types collected_imports var_heap type_heaps symbol_heap
-	#! (nr_of_funs, fun_defs) = usize fun_defs
+transformGroups cleanup_info main_dcl_module_n groups fun_defs cons_args common_defs imported_funs imported_types
+		collected_imports type_def_infos var_heap type_heaps symbol_heap
+	#! nr_of_funs = size fun_defs
 	# (groups, imported_types, collected_imports, ti)
 		= transform_groups 0 groups common_defs imported_funs imported_types collected_imports
 			{ti_fun_defs = fun_defs, ti_instances = createArray nr_of_funs II_Empty,
 				ti_cons_args = cons_args, ti_new_functions = [], ti_fun_heap = newHeap, ti_var_heap = var_heap,
-				ti_symbol_heap = symbol_heap, ti_type_heaps = type_heaps, ti_next_fun_nr = nr_of_funs, ti_cleanup_info = cleanup_info,
-				ti_recursion_introduced = No, ti_trace = False }
+				ti_symbol_heap = symbol_heap, ti_type_heaps = type_heaps, ti_type_def_infos = type_def_infos,
+				ti_next_fun_nr = nr_of_funs, ti_cleanup_info = cleanup_info,
+				ti_recursion_introduced = No, ti_trace = False}
 	  {ti_fun_defs,ti_new_functions,ti_var_heap,ti_symbol_heap,ti_fun_heap,ti_next_fun_nr,ti_type_heaps,ti_cleanup_info} = ti
 	  (groups, new_fun_defs, imported_types, collected_imports, ti_type_heaps, ti_var_heap) 
 	  		= foldSt (add_new_function_to_group common_defs ti_fun_heap) ti_new_functions
 	  				(groups, [], imported_types, collected_imports, ti_type_heaps, ti_var_heap)
-	  ti_symbol_heap = foldSt cleanup ti_cleanup_info ti_symbol_heap
+	  ti_symbol_heap = foldSt cleanup_attributes ti_cleanup_info ti_symbol_heap
 	= ( groups, { fundef \\ fundef <- [ fundef \\ fundef <-: ti_fun_defs ] ++ new_fun_defs }, imported_types, collected_imports,
 			ti_var_heap, ti_type_heaps, ti_symbol_heap)
-
-where
+  where
 	transform_groups group_nr groups common_defs imported_funs imported_types collected_imports ti
 		| group_nr < size groups
 			# (group, groups) = groups![group_nr]
@@ -2046,7 +2294,7 @@ where
 		  		= convertSymbolType common_defs fun_type main_dcl_module_n imported_types collected_imports type_heaps var_heap
 		= ({ fun_defs & [fun_index] = { fun_def & fun_type = Yes fun_type }}, imported_types, collected_imports, type_heaps, var_heap)
 
-	cleanup expr_info_ptr symbol_heap
+	cleanup_attributes expr_info_ptr symbol_heap
 		# (expr_info, symbol_heap) = readPtr expr_info_ptr symbol_heap
 		= case expr_info of
 			EI_Extended _ expr_info -> writePtr expr_info_ptr expr_info symbol_heap
@@ -2080,10 +2328,19 @@ addTypesOfDictionaries common_defs type_contexts type_args
 	= mapAppend (add_types_of_dictionary common_defs) type_contexts type_args
 where
 	add_types_of_dictionary common_defs {tc_class = {glob_module, glob_object={ds_index}}, tc_types}
-		# {class_arity, class_dictionary={ds_ident,ds_index}} = common_defs.[glob_module].com_class_defs.[ds_index]
-		  dict_type_symb = 	MakeTypeSymbIdent { glob_object = ds_index, glob_module = glob_module } ds_ident class_arity
+		# {class_arity, class_dictionary={ds_ident,ds_index}, class_cons_vars}
+				= common_defs.[glob_module].com_class_defs.[ds_index]
+		  dict_type_symb
+		  		= 	MakeTypeSymbIdent { glob_object = ds_index, glob_module = glob_module } ds_ident class_arity
 		= { at_attribute = TA_Multi, at_annotation = AN_Strict, at_type = TA dict_type_symb (
-				map (\type -> { at_attribute = TA_Multi, at_annotation = AN_None, at_type = type }) tc_types) }
+//				map (\type -> { at_attribute = TA_Multi, at_annotation = AN_None, at_type = type }) tc_types) }
+				fst (mapSt 	(\type class_cons_vars
+								-> let at_attribute = if (lowest_bit class_cons_vars) TA_MultiOfPropagatingConsVar TA_Multi
+							   		in ( { at_attribute = at_attribute, at_annotation = AN_None, at_type = type },
+						   				class_cons_vars>>1)
+						   	)
+						  	tc_types
+						  	class_cons_vars))}
 	
 class expandSynTypes a :: !{# CommonDefs} !a !*ExpandTypeState -> (!a, !*ExpandTypeState)
 
@@ -2095,15 +2352,9 @@ instance expandSynTypes SymbolType
 where
 	expandSynTypes common_defs st=:{st_args,st_result,st_context} ets
 		# ((st_args,st_result), ets) = expandSynTypes common_defs (st_args,st_result) ets
-		# st_args = addTypesOfDictionaries common_defs st_context st_args
+		  st_args = addTypesOfDictionaries common_defs st_context st_args
 		= ({st & st_args = st_args, st_result = st_result, st_arity = length st_args, st_context = [] }, ets)
 
-add_types_of_dictionary common_defs {tc_class = {glob_module, glob_object={ds_index}}, tc_types}
-	# {class_arity, class_dictionary={ds_ident,ds_index}} = common_defs.[glob_module].com_class_defs.[ds_index]
-	  dict_type_symb = 	MakeTypeSymbIdent { glob_object = ds_index, glob_module = glob_module } ds_ident class_arity
-	= { at_attribute = TA_Multi, at_annotation = AN_Strict, at_type = TA dict_type_symb (
-			map (\type -> { at_attribute = TA_Multi, at_annotation = AN_None, at_type = type }) tc_types) }
-
 instance expandSynTypes Type
 where
 	expandSynTypes common_defs (arg_type --> res_type) ets
@@ -2369,95 +2620,8 @@ app_EEI_ActiveCase transformer expr_info_ptr expr_heap
 			-> writePtr expr_info_ptr (EI_Extended (EEI_ActiveCase (transformer aci)) original_expr_info) expr_heap
 		_	-> expr_heap
 
-getTypeVars types
-	# (type_variables,_) = get_type_vars types ([],[])
-	= removeDuplicates smaller_type_vars type_variables
-
-removeDuplicates smaller l
-	// XXX speed this up by using heap
-	# sorted = quicksort smaller l
-	  partitions = partitionate sorted
-	= flatten [removeDup uneq partition \\ partition<-partitions]
-  where
-	partitionate []
-		= []
-	partitionate [h:t]
-		= partitions_with t [h]
-	partitions_with [] accu
-		= [accu]
-	partitions_with [h2:t] accu=:[h:_]
-		| h.tv_name.id_name==h2.tv_name.id_name
-			= partitions_with t [h2:accu]
-		= [accu:partitions_with t [h2]]
-	removeDup uneq [x:xs] = [x:removeDup uneq (filter (uneq x) xs)]
-	removeDup uneq _      = []
-	uneq {tv_info_ptr=p1} {tv_info_ptr=p2}
-		= p1<>p2
-		
-quicksort _ []
-	= []
-quicksort smaller [h:t]
-	# left = [ el \\ el<-t | smaller el h ]
-	  right = [ el \\ el<-t | not (smaller el h) ]
-	= (quicksort smaller left)++[h]++(quicksort smaller right)
-
-smaller_type_vars {tv_name={id_name=n1}} {tv_name={id_name=n2}}
-	= n1<n2
-
 undeff :== -1
 
-class get_type_vars a :: a !(![TypeVar], ![AttributeVar]) -> (![TypeVar], ![AttributeVar])
-
-instance get_type_vars Type
-  where
-	get_type_vars (TA _ args) accu
-		= get_type_vars args accu
-	get_type_vars (at1 --> at2) accu
-		= get_type_vars at2 (get_type_vars at1 accu)
-	get_type_vars (cv :@: at) accu
-		= get_type_vars cv (get_type_vars at accu)
-	get_type_vars (GTV t_var) (t_vars,a_vars)
-		= ([t_var:t_vars], a_vars)
-	get_type_vars (TV t_var) (t_vars,a_vars)
-		= ([t_var:t_vars], a_vars)
-	get_type_vars (TQV t_var) (t_vars,a_vars)
-		= ([t_var:t_vars], a_vars)
-	get_type_vars _ accu
-		= accu
-
-instance get_type_vars AType
-  where
-	get_type_vars {at_attribute, at_type} accu
-		= get_type_vars at_attribute (get_type_vars at_type accu)
-
-instance get_type_vars ConsVariable
-  where
-	get_type_vars (CV t_var) (t_vars,a_vars)
-		= ([t_var:t_vars], a_vars)
-
-instance get_type_vars TypeAttribute
-  where
-	get_type_vars (TA_Var a_var) (t_vars,a_vars)
-		= (t_vars, [a_var:a_vars])
-	get_type_vars (TA_RootVar a_var) (t_vars,a_vars)
-		= (t_vars, [a_var:a_vars])
-	get_type_vars (TA_List _ ta) accu
-		= get_type_vars ta accu
-	get_type_vars _ accu
-		= accu
-
-instance get_type_vars [a] | get_type_vars a
-  where
-	get_type_vars [] accu
-		= accu
-	get_type_vars [h:t] accu
-		= get_type_vars t (get_type_vars h accu)
-
-instance get_type_vars (a, b) | get_type_vars a & get_type_vars b
-  where
-	get_type_vars (a, b) accu
-		= get_type_vars a (get_type_vars b accu)
-
 
 /*
 instance <<< InstanceInfo
@@ -2474,10 +2638,21 @@ where
 	(<<<) file (PR_GeneratedFunction symbol index)
 		= file <<< "(G)" <<< symbol.symb_name <<< index
 	(<<<) file PR_Empty = file <<< 'E'
-	(<<<) file (PR_Class _ _ _) = file <<< "(Class)"
-	(<<<) file (PR_Curried {symb_name}) = file <<< "(Curried)" <<< symb_name
+	(<<<) file (PR_Class _ _ type) = file <<< "(Class(" <<< type <<< "))"
+	(<<<) file (PR_Curried {symb_name, symb_kind}) = file <<< "(Curried)" <<< symb_name <<< symb_kind
 	(<<<) file _ = file
 
+instance <<< SymbKind
+where
+	(<<<) file (SK_Function gi) = file <<< "(SK_Function)" <<< gi
+	(<<<) file (SK_LocalMacroFunction gi) = file <<< gi
+	(<<<) file (SK_OverloadedFunction gi) = file <<< "(SK_OverloadedFunction)" <<< gi
+	(<<<) file (SK_Constructor gi) = file <<< gi
+	(<<<) file (SK_Macro gi) = file <<< gi
+	(<<<) file (SK_GeneratedFunction _ gi) = file <<< "(SK_GeneratedFunction)" <<< gi
+	(<<<) file _ = file
+
+
 instance <<< FunCall
 where
 	(<<<) file {fc_index} = file <<< fc_index
@@ -2501,3 +2676,8 @@ instance <<< (Ptr a)
 where
 	(<<<) file p = file <<< ptrToInt p
 
+
+lowest_bit int :== int bitand 1 <> 0
+
+isYes (Yes _) = True
+isYes _ = False
\ No newline at end of file
diff --git a/frontend/type.dcl b/frontend/type.dcl
index 6049c37..383bfe0 100644
--- a/frontend/type.dcl
+++ b/frontend/type.dcl
@@ -4,4 +4,28 @@ import StdArray
 import syntax, check
 
 typeProgram ::!{! Group} !Int !*{# FunDef} !IndexRange !(Optional Bool) !CommonDefs ![Declaration] !{# DclModule} !NumberSet !*Heaps !*PredefinedSymbols !*File !*File
-	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !*Heaps, !*PredefinedSymbols, !*File, !*File)
+	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !.TypeDefInfos, !*Heaps, !*PredefinedSymbols, !*File, !*File)
+
+addPropagationAttributesToAType :: {#CommonDefs} !AType !*PropState -> *(!AType,Int,!*PropState);
+
+::	PropState =
+	{	prop_type_heaps	:: !.TypeHeaps
+	,	prop_td_infos	:: !.TypeDefInfos
+	,	prop_attr_vars	:: ![AttributeVar]
+	,	prop_attr_env	:: ![AttrInequality]
+	,	prop_error		:: !.Optional .ErrorAdmin
+	}
+
+class unify a :: !a !a !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)
+
+instance unify AType
+
+::	TypeInput =
+	{	ti_common_defs	:: !{# CommonDefs }
+	,	ti_functions	:: !{# {# FunType }}
+	,	ti_main_dcl_module_n :: !Int
+	}
+
+class arraySubst type :: !type !u:{!Type} -> (!type, !u:{! Type})
+
+instance arraySubst AType
diff --git a/frontend/type.icl b/frontend/type.icl
index 3be3387..da6ada5 100644
--- a/frontend/type.icl
+++ b/frontend/type.icl
@@ -2,6 +2,7 @@ implementation module type
 
 import StdEnv
 import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor // , RWSDebug
+import cheat
 
 ::	TypeInput =
 	{	ti_common_defs	:: !{# CommonDefs }
@@ -18,7 +19,7 @@ import syntax, typesupport, check, analtypes, overloading, unitype, refmark, pre
 	,	ts_expr_heap	:: !.ExpressionHeap 
 	,	ts_td_infos		:: !.TypeDefInfos
 	,	ts_error		:: !.ErrorAdmin
-	,	ts_out			:: !.File // MW4++
+	,	ts_out			:: !.File
 	}
 
 ::	TypeCoercion =
@@ -36,18 +37,16 @@ import syntax, typesupport, check, analtypes, overloading, unitype, refmark, pre
 ::	Requirements =
 	{	req_overloaded_calls	:: ![ExprInfoPtr]
 	,	req_type_coercions		:: ![TypeCoercion]
-	,	req_type_coercion_groups:: ![TypeCoercionGroup] // MW4++
+	,	req_type_coercion_groups:: ![TypeCoercionGroup]
 	,	req_attr_coercions		:: ![AttrCoercion]
 	,	req_cons_variables		:: ![[TempVarId]]
 	,	req_case_and_let_exprs	:: ![ExprInfoPtr]
 	}
 
-// MW4 added..
 ::	TypeCoercionGroup =
 	{	tcg_type_coercions	:: ![TypeCoercion]
 	,	tcg_position		:: !Position
 	}
-// ..MW4
 
 instance toString BoundVar
 where
@@ -400,20 +399,11 @@ where
 	contains_var var_id _
 		= False
 
-type_error =: "Type error" // MW4++
-type_error_format =: { form_properties = cNoProperties, form_attr_position = No } // MW4++
-
-/* MW4 was:
-cannotUnify t1 t2 position err 
-	# err = errorHeading "Type error" err
-	  format = { form_properties = cNoProperties, form_attr_position = No }
-	= { err & ea_file = err.ea_file <<< optionalFrontPosition position <<< " cannot unify " <:: (format, t1) 
-							<<< " with " <:: (format, t2) <<< position <<< '\n' }
-*/
+type_error =: "Type error"
+type_error_format =: { form_properties = cNoProperties, form_attr_position = No }
 
 cannotUnify t1 t2 position=:(CP_Expression expr) err=:{ea_loc=[ip:_]} 
 	= case tryToOptimizePosition expr of
-// MW0		Yes ident_pos
 		Yes (id_name, line)
 			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
 			  err = errorHeading type_error err
@@ -441,7 +431,6 @@ cannot_unify t1 t2 position err
 	  				-> ea_file <<< " near " <<< position
 	= { err & ea_file = ea_file <<< '\n' }
 
-// MW4..
 tryToOptimizePosition (Case {case_ident=Yes {id_name}})
 	= optBeautifulizeIdent id_name
 tryToOptimizePosition (App {app_symb={symb_name}})
@@ -852,27 +841,33 @@ freshAttribute ts=:{ts_attr_store}
 	,	prop_td_infos	:: !.TypeDefInfos
 	,	prop_attr_vars	:: ![AttributeVar]
 	,	prop_attr_env	:: ![AttrInequality]
-	,	prop_error		:: !.ErrorAdmin
+	,	prop_error		:: !.Optional .ErrorAdmin
 	}
 
-attribute_error type_attr err
+attribute_error type_attr No
+	= abort ("sanity check nr 723 failed in module type"--->("type_attr", type_attr))
+attribute_error type_attr (Yes err)
 	# err = errorHeading "Type error" err
-	= { err & ea_file = err.ea_file <<< "* attribute expected instead of " <<< type_attr <<< '\n' }
+	= Yes { err & ea_file = err.ea_file <<< "* attribute expected instead of " <<< type_attr <<< '\n' }
 
 addPropagationAttributesToAType :: {#CommonDefs} !AType !*PropState -> *(!AType,Int,!*PropState);
-//addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index={glob_object,glob_module}} cons_args, at_attribute} ps
 addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index={glob_object,glob_module},type_name} cons_args, at_attribute} ps
 	# (cons_args, props, ps=:{prop_td_infos,prop_type_heaps,prop_attr_vars,prop_attr_env,prop_error})
 			= add_propagation_attributes_to_atypes modules cons_args ps
 	  (prop_class, th_vars, prop_td_infos) = propClassification glob_object glob_module props modules prop_type_heaps.th_vars prop_td_infos
 	  (at_attribute, prop_class, th_attrs, prop_attr_vars, prop_attr_env, prop_error)
 	  		= determine_attribute_of_cons modules at_attribute cons_args prop_class prop_type_heaps.th_attrs prop_attr_vars prop_attr_env prop_error
-// MW32..
 	  ({tdi_kinds}, prop_td_infos)
 	  		= prop_td_infos![glob_module,glob_object]
-	  (_, prop_error)
-	  		= unsafeFold2St (check_kind type_name modules) tdi_kinds cons_args (1, prop_error)
-// ..MW32
+	  prop_error
+	  		= case prop_error of
+	  			No
+	  				// this function is called after typechecking (during transformations)
+	  				-> No
+	  			Yes error_admin
+	  				# (_, error_admin)
+	  					= unsafeFold2St (check_kind type_name modules) tdi_kinds cons_args (1, error_admin)
+	  				-> Yes error_admin
 	= ({ type & at_type = TA cons_id cons_args, at_attribute = at_attribute }, prop_class,  { ps & prop_attr_vars = prop_attr_vars,
 			prop_td_infos = prop_td_infos, prop_attr_env = prop_attr_env,
 				prop_type_heaps = { prop_type_heaps & th_vars = th_vars, th_attrs = th_attrs}, prop_error = prop_error })
@@ -904,7 +899,8 @@ addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index
 						-> determine_cummulative_attribute types cumm_attr attr_vars (prop_class >> 1)
 					TA_Var attr_var
 						-> determine_cummulative_attribute types at_attribute [attr_var : attr_vars] (prop_class >> 1)
-		
+					TA_MultiOfPropagatingConsVar
+						-> determine_cummulative_attribute types cumm_attr attr_vars (prop_class >> 1)
 
 		combine_attributes (TA_Var attr_var) cumm_attr prop_vars attr_var_heap attr_vars attr_env ps_error
 			= case cumm_attr of
@@ -933,14 +929,13 @@ addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index
 		combine_attributes cons_attr _ _ attr_var_heap attr_vars attr_env ps_error
 			= (cons_attr, attr_var_heap, attr_vars, attr_env, ps_error)
 
-// MW32..
-		check_kind type_name modules type_kind {at_type} (arg_nr, prop_error)
+		check_kind type_name modules type_kind {at_type} (arg_nr, error_admin)
 			# ok
 					= kind_is_ok modules (my_kind_to_int type_kind) at_type
 			| ok
-				= (arg_nr+1, prop_error)
-			# prop_error = errorHeading type_error prop_error
-			= (arg_nr+1, { prop_error & ea_file = prop_error.ea_file <<< " argument " <<< arg_nr <<< " of type " <<< type_name 
+				= (arg_nr+1, error_admin)
+			# error_admin = errorHeading type_error error_admin
+			= (arg_nr+1, { error_admin & ea_file = error_admin.ea_file <<< " argument " <<< arg_nr <<< " of type " <<< type_name 
 													<<< " expected kind " <<< type_kind <<< "\n" })
 		  where
 			kind_is_ok modules demanded_kind (TA {type_index={glob_object,glob_module}} args)
@@ -966,7 +961,6 @@ addPropagationAttributesToAType modules type=:{at_type = TA cons_id=:{type_index
 				= 0
 			my_kind_to_int (KindArrow int_kind)
 				= int_kind
-// ..MW32
 
 addPropagationAttributesToAType modules type=:{at_type} ps
 	# (at_type, ps) = addPropagationAttributesToType modules at_type ps
@@ -982,6 +976,7 @@ addPropagationAttributesToType modules (type_var :@: types) ps
 addPropagationAttributesToType modules type ps
 	= (type, ps)
 
+addPropagationAttributesToATypes :: {#CommonDefs} ![AType] !*PropState -> (![AType],!*PropState)
 addPropagationAttributesToATypes modules types ps
 	= mapSt (add_propagation_attributes_to_atype modules) types ps
 where
@@ -1049,12 +1044,12 @@ determineSymbolTypeOfFunction ident act_arity st=:{st_args,st_result,st_attr_var
 		_	
 			# (st_args, ps) = addPropagationAttributesToATypes common_defs st_args
 					{ prop_type_heaps = ts.ts_type_heaps, prop_td_infos = ts.ts_td_infos,
-					  prop_attr_vars = st_attr_vars, prop_attr_env = st_attr_env, prop_error = ts.ts_error}
-			  (st_result, _, {prop_type_heaps,prop_td_infos,prop_attr_vars,prop_error,prop_attr_env})
+					  prop_attr_vars = st_attr_vars, prop_attr_env = st_attr_env, prop_error = Yes ts.ts_error}
+			  (st_result, _, {prop_type_heaps,prop_td_infos,prop_attr_vars,prop_error = Yes ts_error,prop_attr_env})
 			  			= addPropagationAttributesToAType common_defs st_result ps
 			  st = { st & st_args = st_args, st_result = st_result, st_attr_vars = prop_attr_vars, st_attr_env = prop_attr_env }
 	   		# (copy_symb_type, cons_variables, ts) = freshSymbolType cWithFreshContextVars st common_defs { ts &
-	   										ts_type_heaps = prop_type_heaps, ts_td_infos = prop_td_infos, ts_error = prop_error,
+	   										ts_type_heaps = prop_type_heaps, ts_td_infos = prop_td_infos, ts_error = ts_error,
 											ts_var_heap = ts.ts_var_heap <:= (type_ptr, VI_PropagationType st) }
 			  (curried_st, ts) = currySymbolType copy_symb_type act_arity ts
 			-> (curried_st, cons_variables, ts)
@@ -1189,12 +1184,10 @@ where
 
 instance requirements Case
 where
-// MW4 was:	requirements ti {case_expr,case_guards,case_default,case_info_ptr} reqs_ts
 	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 ti case_guards case_expr expr_type opt_expr_ptr fresh_v (reqs, ts)
-// MW4 was:		  (reqs, ts) = requirements_of_default ti case_default fresh_v reqs_ts
 		  (reqs, ts) = requirements_of_default ti case_default case_default_pos fresh_v reqs_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 })
 		= (fresh_v, No, ({ reqs & req_case_and_let_exprs = [case_info_ptr : reqs.req_case_and_let_exprs]},
@@ -1223,18 +1216,6 @@ where
 			= (reverse used_dyn_types, ({ 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] }, { ts & ts_expr_heap = ts_expr_heap }))
 	
-/* MW4 was:
-		requirements_of_algebraic_patterns ti [] cons_types goal_type used_cons_types reqs_ts
-			= (used_cons_types, reqs_ts)
-		requirements_of_algebraic_patterns ti=:{ti_common_defs} [{ap_symbol, ap_vars, ap_expr }:gs] [ cons_arg_types : cons_types] goal_type used_cons_types (reqs, ts)
-			# (res_type, opt_expr_ptr, (reqs, ts)) 
-					= requirements ti ap_expr (reqs, { ts & ts_var_heap = makeBase ap_symbol.glob_object.ds_ident 1 ap_vars cons_arg_types ts.ts_var_heap})
-			  ts_expr_heap = storeAttribute opt_expr_ptr res_type.at_attribute ts.ts_expr_heap
-			= requirements_of_algebraic_patterns ti gs cons_types goal_type [ cons_arg_types : used_cons_types ]
-				({ reqs & req_type_coercions = [ { tc_demanded = goal_type, tc_offered = res_type, tc_position = CP_Expression ap_expr, tc_coercible = True } : reqs.req_type_coercions] },
-					  { 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)
 		requirements_of_algebraic_patterns ti [alg_pattern=:{ap_position}:alg_patterns] [ cons_arg_types : cons_types] 
@@ -1246,25 +1227,13 @@ where
 						reqs_ts
 					) 
 
-// MW4++..
 		requirements_of_algebraic_pattern ti {ap_symbol, ap_vars, ap_expr} cons_arg_types goal_type (reqs, ts)
 			# (res_type, opt_expr_ptr, (reqs, ts)) 
 					= requirements ti ap_expr (reqs, { ts & ts_var_heap = makeBase ap_symbol.glob_object.ds_ident 1 ap_vars cons_arg_types ts.ts_var_heap})
 			  ts_expr_heap = storeAttribute opt_expr_ptr res_type.at_attribute ts.ts_expr_heap
 			= ({ reqs & req_type_coercions = [ { tc_demanded = goal_type, tc_offered = res_type, tc_position = CP_Expression ap_expr, tc_coercible = True } : reqs.req_type_coercions] },
 					  { ts & ts_expr_heap = ts_expr_heap })
-// ..MW4
 	
-/*
-		requirements_of_basic_patterns _ [] goal_type reqs_ts
-			= reqs_ts
-		requirements_of_basic_patterns ti=:{ti_common_defs} [{bp_expr }:gs] goal_type reqs_ts
-		  	# (res_type, opt_expr_ptr, (reqs, ts)) = requirements ti bp_expr reqs_ts
-			  ts_expr_heap = storeAttribute opt_expr_ptr res_type.at_attribute ts.ts_expr_heap
-			= requirements_of_basic_patterns ti gs goal_type
-				({ reqs & req_type_coercions = [ { tc_demanded = goal_type, tc_offered = res_type, tc_position = CP_Expression bp_expr, tc_coercible = True } : reqs.req_type_coercions] },
-						 { ts & ts_expr_heap = ts_expr_heap })
-*/	
 		requirements_of_basic_patterns _ [] goal_type reqs_ts
 			= reqs_ts
 		requirements_of_basic_patterns ti [{bp_expr, bp_position}:gs] goal_type reqs_ts
@@ -1275,31 +1244,12 @@ where
 					reqs_ts
 				)
 
-// MW4++..
 		requirements_of_basic_pattern ti bp_expr goal_type reqs_ts
 		  	# (res_type, opt_expr_ptr, (reqs, ts)) = requirements ti bp_expr reqs_ts
 			  ts_expr_heap = storeAttribute opt_expr_ptr res_type.at_attribute ts.ts_expr_heap
 			= ({ reqs & req_type_coercions = [ { tc_demanded = goal_type, tc_offered = res_type, tc_position = CP_Expression bp_expr, tc_coercible = True } : reqs.req_type_coercions] },
 						 { ts & ts_expr_heap = ts_expr_heap })
-// ..MW4
-	
-/* MW4 was
-		requirements_of_dynamic_patterns ti goal_type [{dp_var={fv_info_ptr},dp_type,dp_rhs} : dps] used_dyn_types (reqs, ts=:{ts_expr_heap, ts_var_heap})
-			# (EI_TempDynamicPattern _ _ _ _ dyn_type dyn_context dyn_expr_ptr type_code_symbol, ts_expr_heap) = readPtr dp_type ts_expr_heap
-			  ts_var_heap = ts_var_heap <:= (fv_info_ptr, VI_Type dyn_type No)
-			  (dp_rhs_type, opt_expr_ptr, (reqs, ts)) = requirements ti dp_rhs (reqs, { ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap })
-			  ts_expr_heap = storeAttribute opt_expr_ptr dp_rhs_type.at_attribute ts.ts_expr_heap
-			  type_coercion = { tc_demanded = goal_type, tc_offered = dp_rhs_type, tc_position = CP_Expression dp_rhs, tc_coercible = True }
-			| isEmpty dyn_context
-				# reqs = {reqs & req_type_coercions = [ type_coercion : reqs.req_type_coercions]}
-				= requirements_of_dynamic_patterns ti goal_type dps [ [dyn_type] : used_dyn_types ] (reqs, { ts &  ts_expr_heap = ts_expr_heap })
-				# reqs = { reqs & req_type_coercions = [ type_coercion : reqs.req_type_coercions], req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls ]}
-				= requirements_of_dynamic_patterns ti goal_type dps [ [dyn_type] : used_dyn_types ] (reqs, { ts & ts_expr_heap = ts_expr_heap <:=
-						(dyn_expr_ptr,  EI_Overloaded {  oc_symbol = type_code_symbol, oc_context = dyn_context, oc_specials = [] }) })
-		requirements_of_dynamic_patterns ti goal_type [] used_dyn_types reqs_ts
-			= (used_dyn_types, reqs_ts)
-*/
-	
+
 		requirements_of_dynamic_patterns ti goal_type [] used_dyn_types reqs_ts
 			= (used_dyn_types, reqs_ts)
 		requirements_of_dynamic_patterns ti goal_type [dp=:{dp_position, dp_type} : dps] used_dyn_types (reqs, ts=:{ts_expr_heap})
@@ -1312,7 +1262,6 @@ where
 							(reqs, { ts & ts_expr_heap = ts_expr_heap})
 			= requirements_of_dynamic_patterns ti goal_type dps [ [dyn_type] : used_dyn_types ] reqs_ts
 	
-// MW4++..
 		requirements_of_dynamic_pattern dyn_type dyn_context dyn_expr_ptr type_code_symbol 
 										ti goal_type {dp_var={fv_info_ptr},dp_rhs} (reqs, ts=:{ts_expr_heap, ts_var_heap})
 			# ts_var_heap = ts_var_heap <:= (fv_info_ptr, VI_Type dyn_type No)
@@ -1325,18 +1274,8 @@ where
 				# reqs = { reqs & req_type_coercions = [ type_coercion : reqs.req_type_coercions], req_overloaded_calls = [dyn_expr_ptr : reqs.req_overloaded_calls ]}
 				= (reqs, { ts & ts_expr_heap = ts_expr_heap <:=
 						(dyn_expr_ptr,  EI_Overloaded {  oc_symbol = type_code_symbol, oc_context = dyn_context, oc_specials = [] }) })
-// ..MW4
 	
 	
-/* MW4 was:
-		requirements_of_default ti (Yes expr) goal_type reqs_ts
-			# (res_type, opt_expr_ptr, (reqs,  ts)) = requirements ti expr reqs_ts
-			  ts_expr_heap = storeAttribute opt_expr_ptr res_type.at_attribute ts.ts_expr_heap
-			= ({ reqs & req_type_coercions = [ { tc_demanded = goal_type, tc_offered = res_type, tc_position = CP_Expression expr, tc_coercible = True } : reqs.req_type_coercions] },
-					{ ts & ts_expr_heap = ts_expr_heap })
-		requirements_of_default ti No goal_type reqs_ts
-			= reqs_ts
-*/
 		requirements_of_default ti (Yes expr) case_default_pos goal_type reqs_ts
 	  		= possibly_accumulate_reqs_in_new_group
 	  				case_default_pos
@@ -1353,16 +1292,6 @@ where
 
 instance requirements Let
 where
-/* MW0 was
-	requirements ti {let_lazy_binds, let_strict_binds, let_expr, let_info_ptr} (reqs, ts)
-		# let_binds = let_strict_binds ++ let_lazy_binds
-		  (rev_var_types, ts) = make_base let_binds [] ts
-		  var_types = reverse rev_var_types
-		  (res_type, opt_expr_ptr, reqs_ts) = requirements ti let_expr (reqs, ts)
- 		  (reqs, ts) = requirements_of_binds ti let_binds var_types reqs_ts
-		  ts_expr_heap = writePtr let_info_ptr (EI_LetType var_types) ts.ts_expr_heap
-		= ( res_type, opt_expr_ptr, ({ reqs & req_case_and_let_exprs = [let_info_ptr : reqs.req_case_and_let_exprs]},{ ts & ts_expr_heap = ts_expr_heap }))
-*/
 	requirements ti {let_lazy_binds, let_strict_binds, let_expr, let_info_ptr, let_expr_position } (reqs, ts)
 		# let_binds = let_strict_binds ++ let_lazy_binds
 		  (rev_var_types, ts) = make_base let_binds [] ts
@@ -1373,26 +1302,15 @@ where
 		= ( res_type, opt_expr_ptr, ({ reqs & req_case_and_let_exprs = [let_info_ptr : reqs.req_case_and_let_exprs]},{ ts & ts_expr_heap = ts_expr_heap }))
 	where
 	
-// MW0		make_base [{bind_src, bind_dst={fv_name, fv_info_ptr}}:bs] var_types ts=:{ts_var_heap}
 		make_base [{lb_src, lb_dst={fv_name, fv_info_ptr}}:bs] var_types ts=:{ts_var_heap}
 			# (v, ts) = freshAttributedVariable ts
-// MW0			  optional_position = if (is_rare_name fv_name) (Yes (CP_Expression bind_src)) No
 			  optional_position = if (is_rare_name fv_name) (Yes (CP_Expression lb_src)) No
 			= make_base bs [v:var_types] { ts & ts_var_heap = writePtr fv_info_ptr (VI_Type v optional_position) ts.ts_var_heap }
 		make_base [] var_types ts
 			= (var_types, ts)
 	
-// MW0		requirements_of_binds _ [] _ reqs_ts
 		requirements_of_binds _ _ [] _ reqs_ts
 			= reqs_ts
-/* MW0
-		requirements_of_binds ti [{bind_src}:bs] [b_type:bts] reqs_ts
-			# (exp_type, opt_expr_ptr, (reqs, ts)) = requirements ti bind_src reqs_ts
-			  ts_expr_heap = storeAttribute opt_expr_ptr b_type.at_attribute ts.ts_expr_heap
-			  req_type_coercions = [ { tc_demanded = b_type, tc_offered = exp_type, tc_position = CP_Expression bind_src, tc_coercible = True }
-			  		: reqs.req_type_coercions ]
-			= requirements_of_binds ti bs bts ({ reqs & req_type_coercions = req_type_coercions }, { ts & ts_expr_heap = ts_expr_heap })
-*/
 		requirements_of_binds last_position ti [{lb_src, lb_position}:bs] [b_type:bts] reqs_ts
 			# position = if (is_a_new_position lb_position last_position) lb_position NoPos
 			  reqs_ts
@@ -1546,7 +1464,7 @@ where
 	requirements ti (TupleSelect tuple_symbol arg_nr expr) (reqs=:{req_attr_coercions}, ts)
 		# ({tst_args = [argtype:_], tst_result, tst_attr_env}, ts) = standardTupleSelectorType tuple_symbol arg_nr ti ts
 		  (e_type, opt_expr_ptr, (reqs, ts)) = requirements ti expr ({ reqs & req_attr_coercions = tst_attr_env ++ req_attr_coercions }, ts)
-		  (position, ts_var_heap) = getPositionOfExpr expr ts.ts_var_heap // MW3++
+		  (position, ts_var_heap) = getPositionOfExpr expr ts.ts_var_heap
 		  req_type_coercions = [{ tc_demanded = argtype, tc_offered = e_type, tc_position = position, tc_coercible = True } : reqs.req_type_coercions ]
 		  ts_expr_heap = storeAttribute opt_expr_ptr argtype.at_attribute ts.ts_expr_heap
 		= (tst_result, No, ({ reqs & req_type_coercions = req_type_coercions }, { ts & ts_expr_heap = ts_expr_heap, ts_var_heap = ts_var_heap }))
@@ -1636,7 +1554,6 @@ where
 						tc_position = CP_Expression elem_expr, tc_coercible = True } : reqs.req_type_coercions ]}
 		= (reqs, ts)
 
-// MW4..
 possibly_accumulate_reqs_in_new_group position state_transition reqs_ts
 	:== possibly_accumulate_reqs position reqs_ts
   where
@@ -1656,7 +1573,6 @@ possibly_accumulate_reqs_in_new_group position state_transition reqs_ts
 			  			req_type_coercions = old_req_type_coercions }
 		= (reqs_with_new_group, ts)
 
-// ..MW4
 makeBase _ _ [] [] ts_var_heap
 	= ts_var_heap
 makeBase fun_or_cons_ident arg_nr [{fv_name, fv_info_ptr}:vars] [type:types] ts_var_heap
@@ -1696,18 +1612,17 @@ where
 				{fun_symb, fun_type = Yes ft=:{st_arity,st_args,st_result,st_attr_vars,st_attr_env},fun_lifted,
 				 fun_info = {fi_dynamics}, fun_pos }
 				(pre_def_symbols, req_cons_variables, ts=:{ts_type_heaps,ts_expr_heap,ts_td_infos,ts_error})
-// MW32..
 		# fe_location = newPosition fun_symb fun_pos
 		  ts_error = setErrorAdmin fe_location ts_error
-// ..MW32
 		  (st_args, ps) = addPropagationAttributesToATypes common_defs st_args
 				{ prop_type_heaps = ts_type_heaps, prop_td_infos = ts_td_infos,
-				  prop_attr_vars = st_attr_vars, prop_attr_env = st_attr_env, prop_error = ts_error}
-		  (st_result, _, {prop_type_heaps,prop_td_infos,prop_attr_vars,prop_error,prop_attr_env}) = addPropagationAttributesToAType common_defs st_result ps
+				  prop_attr_vars = st_attr_vars, prop_attr_env = st_attr_env, prop_error = Yes ts_error}
+		  (st_result, _, {prop_type_heaps,prop_td_infos,prop_attr_vars,prop_error = Yes ts_error,prop_attr_env})
+		  		= addPropagationAttributesToAType common_defs st_result ps
 		  ft_with_prop = { ft & st_args = st_args, st_result = st_result, st_attr_vars = prop_attr_vars, st_attr_env = prop_attr_env }
 		  (th_vars, ts_expr_heap) = clear_dynamics fi_dynamics (prop_type_heaps.th_vars, ts.ts_expr_heap)
 		  (fresh_fun_type, cons_variables, ts) = freshSymbolType cWithoutFreshContextVars ft_with_prop common_defs { ts & ts_type_heaps = { prop_type_heaps & th_vars = th_vars }, ts_expr_heap = ts_expr_heap,
-		  		 ts_td_infos = prop_td_infos, ts_error = prop_error }
+		  		 ts_td_infos = prop_td_infos, ts_error = ts_error }
 		  (lifted_args, ts) = fresh_non_unique_type_variables fun_lifted [] ts
 		  (ts_var_store, ts_type_heaps, ts_var_heap, ts_expr_heap, pre_def_symbols)
 		  		= fresh_dynamics fi_dynamics (ts.ts_var_store, ts.ts_type_heaps, ts.ts_var_heap, ts.ts_expr_heap, pre_def_symbols)
@@ -1845,23 +1760,18 @@ where
 specification_error type err
 	# err = errorHeading "Type error" err
 	  format = { form_properties = cAttributed, form_attr_position = No}
-// MW4 was:	= { err & ea_file = err.ea_file <<< " specified type conflicts with derived type " <:: (format, type) <<< '\n' }
 	= { err & ea_file = err.ea_file <<< " specified type conflicts with derived type " 
 									<:: (format, type, Yes initialTypeVarBeautifulizer) <<< '\n' }
 
 
-// MW4 was:cleanUpAndCheckFunctionTypes [] _ _ start_index defs type_contexts coercion_env attr_partition type_var_env attr_var_env (fun_defs, ts)
 cleanUpAndCheckFunctionTypes [] _ _ start_index _ defs type_contexts coercion_env attr_partition type_var_env attr_var_env (fun_defs, ts)
 	= (fun_defs, ts)
-// MW4 was:cleanUpAndCheckFunctionTypes [fun : funs] [ {fe_requirements = {req_case_and_let_exprs}} : reqs] dict_types start_index defs type_contexts coercion_env
 cleanUpAndCheckFunctionTypes [fun : funs] [ {fe_requirements = {req_case_and_let_exprs}} : reqs] dict_types start_index list_inferred_types defs type_contexts coercion_env
 				attr_partition type_var_env attr_var_env (fun_defs, ts)
 	# (fd, fun_defs) = fun_defs![fun]
 	  dict_ptrs = get_dict_ptrs fun dict_types
-// MW4 was:	  (type_var_env, attr_var_env, ts) = clean_up_and_check_function_type fd fun (start_index == fun) defs type_contexts
 	  (type_var_env, attr_var_env, ts) = clean_up_and_check_function_type fd fun (start_index == fun) list_inferred_types defs type_contexts
 													(dict_ptrs ++ req_case_and_let_exprs) coercion_env attr_partition type_var_env attr_var_env ts
-// MW4 was:	= cleanUpAndCheckFunctionTypes funs reqs dict_types start_index defs type_contexts coercion_env attr_partition type_var_env attr_var_env (fun_defs, ts)
 	= cleanUpAndCheckFunctionTypes funs reqs dict_types start_index list_inferred_types defs type_contexts coercion_env attr_partition type_var_env attr_var_env (fun_defs, ts)
 where
 	get_dict_ptrs fun_index []
@@ -1871,7 +1781,6 @@ where
 			= ptrs
 			= get_dict_ptrs fun_index dict_types
 		
-// MW4 was:	clean_up_and_check_function_type {fun_symb,fun_pos,fun_type = opt_fun_type} fun is_start_rule defs type_contexts type_ptrs
 	clean_up_and_check_function_type {fun_symb,fun_pos,fun_type = opt_fun_type} fun is_start_rule list_inferred_types defs type_contexts type_ptrs
 					coercion_env attr_partition type_var_env attr_var_env ts
 		# (env_type, ts) = ts!ts_fun_env.[fun]
@@ -1890,7 +1799,6 @@ where
 				# (clean_fun_type, type_var_env, attr_var_env, ts_type_heaps, ts_var_heap, ts_expr_heap, ts_error)
 					= cleanUpSymbolType is_start_rule cDerivedType exp_fun_type type_contexts type_ptrs coercion_env
 										attr_partition type_var_env attr_var_env ts.ts_type_heaps ts.ts_var_heap ts.ts_expr_heap ts.ts_error
-// MW4..
 				  ts_out = ts.ts_out
 				  th_attrs = ts_type_heaps.th_attrs
 				  (ts_out, th_attrs)
@@ -1908,9 +1816,7 @@ where
 				  				  				-> (clean_fun_type, th_attrs)	
 				  				-> (ts_out <<< fun_symb <<< " :: " 
 				  						<:: (form, printable_type, Yes initialTypeVarBeautifulizer) <<< '\n', th_attrs)
-// ..MW4
 				  ts_fun_env = { ts.ts_fun_env & [fun] = CheckedType clean_fun_type }
-// MW4 was:				-> (type_var_env, attr_var_env, { ts & ts_type_heaps = ts_type_heaps, ts_var_heap = ts_var_heap, ts_expr_heap = ts_expr_heap, ts_fun_env = ts_fun_env, ts_error = ts_error })
 				-> (type_var_env, attr_var_env, { ts & ts_type_heaps = { ts_type_heaps & th_attrs = th_attrs }, ts_var_heap = ts_var_heap, ts_expr_heap = ts_expr_heap, ts_fun_env = ts_fun_env, ts_error = ts_error, ts_out = ts_out })
 
 	check_function_type fun_type tmp_fun_type=:{tst_lifted} clean_fun_type=:{st_arity, st_args, st_vars, st_attr_vars, st_context} type_ptrs
@@ -1943,7 +1849,7 @@ addLiftedArgumentsToSymbolType st=:{st_arity,st_args,st_vars,st_attr_vars,st_con
 	}
 
 typeProgram ::!{! Group} !Int !*{# FunDef} !IndexRange  !(Optional Bool) !CommonDefs ![Declaration] !{# DclModule} !NumberSet !*Heaps !*PredefinedSymbols !*File !*File
-	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !*Heaps, !*PredefinedSymbols, !*File, !*File)
+	-> (!Bool, !*{# FunDef}, !IndexRange, {! GlobalTCType}, !{# CommonDefs}, !{# {# FunType} }, !.TypeDefInfos, !*Heaps, !*PredefinedSymbols, !*File, !*File)
 typeProgram comps main_dcl_module_n fun_defs specials list_inferred_types icl_defs imports modules used_module_numbers heaps=:{hp_var_heap, hp_expression_heap, hp_type_heaps} predef_symbols file out
 	#! fun_env_size = size fun_defs
 	# ts_error = {ea_file = file, ea_loc = [], ea_ok = True }
@@ -1957,7 +1863,7 @@ typeProgram comps main_dcl_module_n fun_defs specials list_inferred_types icl_de
 	  (td_infos, hp_type_heaps, ts_error) = analTypeDefs ti_common_defs used_module_numbers hp_type_heaps ts_error
 
 	| not ts_error.ea_ok
-		= (ts_error.ea_ok, fun_defs, { ir_from = 0, ir_to = 0 }, {}, ti_common_defs, ti_functions,
+		= (ts_error.ea_ok, fun_defs, { ir_from = 0, ir_to = 0 }, {}, ti_common_defs, ti_functions, td_infos,
 			{ heaps & hp_type_heaps = hp_type_heaps }, predef_symbols, ts_error.ea_file, out)
 	# state = collect_imported_instances imports ti_common_defs {} ts_error class_instances hp_type_heaps.th_vars td_infos 
 	  (_, ts_error, class_instances, th_vars, td_infos) = collect_and_check_instances (size icl_defs.com_instance_defs) ti_common_defs state
@@ -1968,14 +1874,15 @@ typeProgram comps main_dcl_module_n fun_defs specials list_inferred_types icl_de
 	  special_instances = { si_next_array_member_index = fun_env_size, si_array_instances = [], si_next_TC_member_index = 0, si_TC_instances = [] }
 	# (type_error, fun_defs, predef_symbols, special_instances, ts) = type_components list_inferred_types 0 comps class_instances ti (False, fun_defs, predef_symbols, special_instances, ts)
 	  (fun_defs,ts_fun_env) = update_function_types 0 comps ts.ts_fun_env fun_defs
-	  (type_error, fun_defs, predef_symbols, special_instances, {ts_fun_env,ts_error,ts_var_heap, ts_expr_heap, ts_type_heaps, ts_out})
+	  (type_error, fun_defs, predef_symbols, special_instances, {ts_td_infos,ts_fun_env,ts_error,ts_var_heap, ts_expr_heap, ts_type_heaps, ts_out})
 			= type_instances list_inferred_types specials.ir_from specials.ir_to class_instances ti (type_error, fun_defs, predef_symbols, special_instances,
 							{ ts & ts_fun_env = ts_fun_env })
 	  {si_array_instances, si_next_array_member_index, si_next_TC_member_index, si_TC_instances}= special_instances
 	  (fun_defs, predef_symbols, ts_type_heaps) = convert_array_instances si_array_instances ti_common_defs fun_defs predef_symbols ts_type_heaps
 	  type_code_instances = {createArray si_next_TC_member_index GTT_Function & [gtci_index] = gtci_type \\ {gtci_index, gtci_type} <- si_TC_instances}
 	= (not type_error, fun_defs, { ir_from = fun_env_size, ir_to = si_next_array_member_index }, type_code_instances, ti_common_defs, ti_functions,
-			{hp_var_heap = ts_var_heap, hp_expression_heap = ts_expr_heap, hp_type_heaps = ts_type_heaps }, predef_symbols, ts_error.ea_file, ts_out)
+			ts_td_infos, {hp_var_heap = ts_var_heap, hp_expression_heap = ts_expr_heap, hp_type_heaps = ts_type_heaps },
+			predef_symbols, ts_error.ea_file, ts_out)
 //				---> ("typeProgram", array_inst_types)
 where
 	collect_imported_instances imports common_defs dummy error class_instances type_var_heap td_infos
@@ -2179,11 +2086,6 @@ where
 				-> (set_bit var_number bitvects, subst)	// ---> ("determine_cons_variable2", var_number)
 			_
 				-> (bitvects, subst)
-	where
-		set_bit var_number bitvects
-			# bit_index = BITINDEX var_number
-			  (prev_vect, bitvects) = bitvects![bit_index]
-			= { bitvects & [bit_index] = prev_vect bitor (1 << BITNUMBER var_number) }
 
 	build_coercion_env :: [.FunctionRequirements] v:{!Type} *Coercions {#CommonDefs} {#Int} *{#*{#TypeDefInfo}} *TypeHeaps !*ErrorAdmin -> (!w:{!Type},!.Coercions,!u:{#u:{#TypeDefInfo}},!.TypeHeaps,!.ErrorAdmin), [v <= w];
 	build_coercion_env [{fe_requirements={req_type_coercion_groups},fe_location={ip_ident}} : reqs_list] subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
@@ -2201,8 +2103,31 @@ where
 		= add_to_coercion_env tcg_type_coercions subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
 
 	add_to_coercion_env [{tc_offered,tc_demanded,tc_coercible,tc_position} : attr_coercions] subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
-		# (subst, coercion_env, type_signs, type_var_heap, error)
-				= determineAttributeCoercions tc_offered tc_demanded tc_coercible tc_position subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
+		# (opt_error_info, subst, coercion_env, type_signs, type_var_heap)
+				= determineAttributeCoercions tc_offered tc_demanded tc_coercible
+						subst coercion_env common_defs cons_var_vects type_signs
+						type_var_heap
+		  (coercion_env, error)
+			= case opt_error_info of
+				No
+					-> (coercion_env, error)
+				Yes (positions, exp_off_type)
+					# (error=:{ea_file})
+							= errorHeading "Uniqueness error" error
+					  (coercion_env, copy_coercion_env)
+					  		= uniqueCopy coercion_env
+					  format
+					  		= { form_properties = cMarkAttribute,
+					  			form_attr_position = Yes (reverse positions, copy_coercion_env) }			
+					  ea_file = 
+					  	case tc_position of
+					  		CP_FunArg _ _
+					  			-> ea_file <<< "\"" <<< tc_position <<< "\" "
+					  		_
+					  			-> ea_file
+					  ea_file = ea_file	<<< "attribute at indicated position could not be coerced "
+					  					 <:: (format, exp_off_type, Yes initialTypeVarBeautifulizer) <<< '\n'
+					-> (coercion_env, { error & ea_file = ea_file })
 		= add_to_coercion_env attr_coercions subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
 	add_to_coercion_env []  subst coercion_env common_defs cons_var_vects type_signs type_var_heap error
 		= (subst, coercion_env, type_signs, type_var_heap, error)
diff --git a/frontend/typesupport.dcl b/frontend/typesupport.dcl
index 8151d91..b36113b 100644
--- a/frontend/typesupport.dcl
+++ b/frontend/typesupport.dcl
@@ -44,6 +44,8 @@ expandTypeApplication :: ![ATypeVar] !TypeAttribute !Type ![AType] !TypeAttribut
 
 equivalent :: !SymbolType !TempSymbolType !Int !{# CommonDefs} !*AttributeEnv !*TypeHeaps -> (!Bool, !*AttributeEnv, !*TypeHeaps) 
 
+NewAttrVarId :: !Int -> Ident
+
 beautifulizeAttributes :: !SymbolType !*AttrVarHeap -> (!SymbolType, !.AttrVarHeap)
 
 ::	AttrCoercion =
@@ -68,15 +70,18 @@ updateExpressionTypes :: !SymbolType !SymbolType ![ExprInfoPtr] !*TypeHeaps !*Ex
 
 class substitute a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
 
-instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | substitute a
+instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | substitute a,
+			(a,b) | substitute a & substitute b
 
 instance <<< TempSymbolType
 
 removeInequality :: !Int !Int !*Coercions -> .Coercions
 flattenCoercionTree :: !u:CoercionTree -> (![Int], !u:CoercionTree)
+	// retrieve all numbers from a coercion tree
 assignNumbersToAttrVars :: !SymbolType !*AttrVarHeap -> (!Int, ![AttributeVar], !.AttrVarHeap)
+	// returns the number and a list of all attribute variables
 getImplicitAttrInequalities :: !SymbolType -> [AttrInequality]
-	// retrieve those inequalities  that are implied by propagation
+	// retrieve those inequalities that are implied by propagation
 emptyCoercions :: !Int -> .Coercions
 	// Int: nr of attribute variables
 addAttrEnvInequalities :: ![AttrInequality] !*Coercions !u:AttrVarHeap
@@ -85,6 +90,7 @@ addAttrEnvInequalities :: ![AttrInequality] !*Coercions !u:AttrVarHeap
 	// nr corresponds to the attribute variable
 optBeautifulizeIdent :: !String -> Optional (!String, !LineNr)
 	// convert something like "c;8;2" to Yes ("comprehension", 8)
+removeUnusedAttrVars :: !{!CoercionTree} ![Int] -> Coercions
 	
 //accCoercionTree :: !.(u:CoercionTree -> (.a,u:CoercionTree)) !Int !*{!u:CoercionTree} -> (!.a,!{!u:CoercionTree})
 accCoercionTree f i coercion_trees
@@ -103,3 +109,26 @@ appCoercionTree f i coercion_trees
 		# (coercion_tree, coercion_trees) = replace coercion_trees i CT_Empty
 		= snd (replace coercion_trees i (f coercion_tree))
 	
+class performOnTypeVars a :: !(TypeAttribute TypeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each type variable
+
+instance performOnTypeVars Type, AType, ConsVariable, [a] | performOnTypeVars a,
+		(a, b) | performOnTypeVars a & performOnTypeVars b
+
+getTypeVars :: !a !*TypeVarHeap -> (!.[TypeVar],!.TypeVarHeap) | performOnTypeVars a
+
+class performOnAttrVars a :: !(AttributeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each attribute variable
+
+getAttrVars :: !a !*AttrVarHeap -> (!.[AttributeVar],!.AttrVarHeap) | performOnAttrVars a
+
+instance performOnAttrVars Type, AType, [a] | performOnAttrVars a,
+		(a, b) | performOnAttrVars a & performOnAttrVars b
+
+initializeToTVI_Empty :: a !TypeVar !*TypeVarHeap -> .TypeVarHeap
+initializeToAVI_Empty :: !AttributeVar !*AttrVarHeap -> .AttrVarHeap
+
+appTypeVarHeap f type_heaps :== let th_vars = f type_heaps.th_vars in { type_heaps & th_vars = th_vars }
+accTypeVarHeap f type_heaps :== let (r, th_vars) = f type_heaps.th_vars in (r, { type_heaps & th_vars = th_vars })
+accAttrVarHeap f type_heaps :== let (r, th_attrs) = f type_heaps.th_attrs in (r, { type_heaps & th_attrs = th_attrs })
+	
diff --git a/frontend/typesupport.icl b/frontend/typesupport.icl
index 8d7588c..3da8390 100644
--- a/frontend/typesupport.icl
+++ b/frontend/typesupport.icl
@@ -493,20 +493,12 @@ where
 instance substitute TypeAttribute
 where
 	substitute (TA_Var {av_name, av_info_ptr}) heaps=:{th_attrs}
-/* 
-	This alternative's code can be replaced with the original again, when the fusion algorithm becomes able to
-    infer correct type attributes
-*/
 		#! av_info = sreadPtr av_info_ptr th_attrs
 		= case av_info of
 			AVI_Attr attr
 				-> (attr, heaps)
 			_
 				-> (TA_Multi, heaps)
-/* Sjaak ...				-> SwitchFusion
-						(TA_Multi, heaps)
-						(abort "compiler bug nr 7689 in module typesupport")
-... Sjaak */
 	substitute TA_None heaps
 		= (TA_Multi, heaps)
 	substitute attr heaps
@@ -540,7 +532,7 @@ substituteTypeVariable tv=:{tv_name,tv_info_ptr} heaps=:{th_vars}
 	  heaps = { heaps & th_vars = th_vars }
 	= case tv_info of
 		TVI_Type type
-			-> (type, heaps)
+				-> (type, heaps)
 		_
 			-> (TV tv, heaps)
 
@@ -548,16 +540,28 @@ instance substitute Type
 where
 	substitute (TV tv) heaps
 		= substituteTypeVariable tv heaps
-	substitute (arg_type --> res_type)  heaps
+	substitute (arg_type --> res_type) heaps
 		# ((arg_type, res_type), heaps) = substitute (arg_type, res_type) heaps
 		= (arg_type --> res_type, heaps)
-	substitute (TA cons_id cons_args)  heaps
+	substitute (TA cons_id cons_args) heaps
 		# (cons_args, heaps) = substitute cons_args heaps
 		= (TA cons_id cons_args,  heaps)
-	substitute (CV type_var :@: types)  heaps
+/* MW3 was
+	substitute (CV type_var :@: types) heaps
 		# (type, heaps) = substituteTypeVariable type_var heaps
 		  (types, heaps) = substitute types heaps
 		= (simplifyTypeApplication type types, heaps)
+*/
+	substitute (CV type_var :@: types) heaps=:{th_vars}
+		# (tv_info, th_vars) = readPtr type_var.tv_info_ptr th_vars
+		  heaps = { heaps & th_vars = th_vars }
+		  (types, heaps) = substitute types heaps
+		= case tv_info of
+			TVI_Type tv=:(TempV i)
+				-> (TempCV i :@: types, heaps)
+			_
+				# (type, heaps) = substituteTypeVariable type_var heaps
+				-> (simplifyTypeApplication type types, heaps)
 	substitute type heaps
 		= (type, heaps)
 
@@ -605,6 +609,7 @@ NewVarId var_store
 AttrVarIdTable :: {# String}
 AttrVarIdTable =: { "u", "v", "w", "x", "y", "z" }
 
+NewAttrVarId :: !Int -> Ident
 NewAttrVarId attr_var_store
 	| attr_var_store < size AttrVarIdTable
  		= newIdent AttrVarIdTable.[attr_var_store]
@@ -1295,41 +1300,34 @@ beautifulizeAttributes symbol_type th_attrs
 assignNumbersToAttrVars :: !SymbolType !*AttrVarHeap -> (!Int, ![AttributeVar], !.AttrVarHeap)
 assignNumbersToAttrVars {st_attr_vars, st_args, st_result, st_attr_env} th_attrs
 	# th_attrs
-			= foldSt initialise_to_AVI_Empty st_attr_vars th_attrs
-	  (next_number, numbered_vars_accu, th_attrs)
-	  		= foldSt assign_numbers_attr_ineq st_attr_env
-				(assign_numbers_atype st_result
-					(foldSt assign_numbers_atype st_args (0, [], th_attrs)))
-	= (next_number, reverse numbered_vars_accu, th_attrs)
+			= foldSt initializeToAVI_Empty st_attr_vars th_attrs
+	  (nr_of_attr_vars, attr_vars, th_attrs)
+	  		= performOnAttrVars assign_number_to_unencountered_attr_var (st_args, st_result)
+	  				(0, [], th_attrs)
+	| fst (foldSt hasnt_got_a_number st_attr_env (False, th_attrs))
+		= abort "sanity check nr 834 in module typesupport failed"
+ 	= (nr_of_attr_vars, attr_vars, th_attrs)
   where
-	assign_numbers_atype atype=:{at_attribute=TA_Var av=:{av_info_ptr}, at_type}
-						(next_number, numbered_vars_accu, th_attrs)
+	assign_number_to_unencountered_attr_var av=:{av_info_ptr} (next_number, attr_vars_accu, th_attrs)
 		# (avi, th_attrs) = readPtr av_info_ptr th_attrs
-		= assign_numbers_type at_type
-			(assign_number avi av (next_number, numbered_vars_accu, th_attrs))
-	assign_numbers_atype atype=:{at_type} assign_state
-		= assign_numbers_type at_type assign_state
-
-	assign_numbers_type (TA _ args) assign_state
-		= foldSt assign_numbers_atype args assign_state
-	assign_numbers_type (l --> r) assign_state
-		= assign_numbers_atype l (assign_numbers_atype r assign_state)
-	assign_numbers_type (_ :@: args) assign_state
-		= foldSt assign_numbers_atype args assign_state
-	assign_numbers_type _ assign_state
-		= assign_state
-
-	assign_numbers_attr_ineq {ai_offered, ai_demanded} (next_number, numbered_vars_accu, th_attrs)
-		# (avi_offered, th_attrs) = readPtr ai_offered.av_info_ptr th_attrs
-		  (avi_demanded, th_attrs) = readPtr ai_demanded.av_info_ptr th_attrs
-		= assign_number avi_offered ai_offered
-			(assign_number avi_demanded ai_demanded (next_number, numbered_vars_accu, th_attrs))
+		= case avi of
+			AVI_Empty
+				-> (next_number+1, [av:attr_vars_accu],
+					writePtr av_info_ptr (AVI_Attr (TA_TempVar next_number)) th_attrs)
+			_
+				-> (next_number, attr_vars_accu, th_attrs)
 	
-	assign_number AVI_Empty av=:{av_info_ptr} (next_number, numbered_vars_accu, th_attrs)
-		= (next_number+1, [av:numbered_vars_accu],
-			writePtr av_info_ptr (AVI_Attr (TA_TempVar next_number)) th_attrs)
-	assign_number _ _ assign_state
-		= assign_state
+	hasnt_got_a_number {ai_offered, ai_demanded} (or_of_all, th_attrs)
+		# hnn1 = has_no_number ai_offered th_attrs
+		  hnn2 = has_no_number ai_demanded th_attrs
+		= (hnn1 || hnn2 || or_of_all, th_attrs)
+		
+	has_no_number {av_info_ptr} th_attrs
+		= case sreadPtr av_info_ptr th_attrs of
+			AVI_Empty
+				-> True
+			_
+				-> False
 
 //accCoercionTree :: !.(u:CoercionTree -> (.a,u:CoercionTree)) !Int !*{!u:CoercionTree} -> (!.a,!{!u:CoercionTree})
 accCoercionTree f i coercion_trees
@@ -1351,12 +1349,12 @@ flattenCoercionTree :: !u:CoercionTree -> (![Int], !u:CoercionTree)
 flattenCoercionTree tree
 	= flatten_ct ([], tree)
   where
-	flatten_ct (accu, CT_Empty)
-		= (accu, CT_Empty)
 	flatten_ct (accu, CT_Node i left right)
 		# (accu, right) = flatten_ct (accu, right)
 		  (accu, left) = flatten_ct ([i:accu], left)
 		= (accu, CT_Node i left right)
+	flatten_ct (accu, _)
+		= (accu, CT_Empty)
 
 anonymizeAttrVars :: !SymbolType ![AttrInequality] !*AttrVarHeap -> (!SymbolType, !.AttrVarHeap)
 anonymizeAttrVars st=:{st_attr_vars, st_args, st_result, st_attr_env} implicit_inequalities th_attrs
@@ -1446,32 +1444,28 @@ anonymizeAttrVars st=:{st_attr_vars, st_args, st_result, st_attr_env} implicit_i
 			_
 				-> th_attrs
 				
-initialise_to_AVI_Empty {av_info_ptr} th_attrs
-	= writePtr av_info_ptr AVI_Empty th_attrs
-
 removeInequality :: !Int !Int !*Coercions -> .Coercions
 removeInequality offered demanded attr_env_coercions=:{coer_offered, coer_demanded}
 	# coer_offered = appCoercionTree (removeNode offered) demanded coer_offered
 	  coer_demanded = appCoercionTree (removeNode demanded) offered coer_demanded
 	= { attr_env_coercions & coer_demanded = coer_demanded, coer_offered = coer_offered }
-  where
-	removeNode :: !Int !*CoercionTree -> !.CoercionTree
-	removeNode i1 (CT_Node i2 left right)
-		| i1<i2
-			= CT_Node i2 (removeNode i1 left) right
-		| i1>i2
-			= CT_Node i2 left (removeNode i1 right)
-		= rightInsert left right
-	removeNode i1 CT_Empty
-		= CT_Empty
 
+removeNode :: !Int !*CoercionTree -> !.CoercionTree
+removeNode i1 (CT_Node i2 left right)
+	| i1<i2
+		= CT_Node i2 (removeNode i1 left) right
+	| i1>i2
+		= CT_Node i2 left (removeNode i1 right)
+	= rightInsert left right
+  where
 	rightInsert :: !*CoercionTree !*CoercionTree -> !.CoercionTree
 	rightInsert CT_Empty right
 		= right
 	rightInsert (CT_Node i left right2) right1
 		= CT_Node i left (rightInsert right2 right1)
+removeNode i1 CT_Empty
+	= CT_Empty
 
-			
 emptyCoercions :: !Int -> .Coercions
 emptyCoercions nr_of_attr_vars
 		= { coer_demanded = create_a_unique_array nr_of_attr_vars,
@@ -1523,3 +1517,152 @@ searchlArrElt p s i
 			= i
 		= searchl s (i+1)
 // ..MW4
+
+removeUnusedAttrVars :: !{!CoercionTree} ![Int] -> Coercions
+removeUnusedAttrVars demanded unused_attr_vars
+	# nr_of_attr_vars
+			= size demanded
+	  coercions
+			= emptyCoercions nr_of_attr_vars
+	  coercions
+	  		= iFoldSt (add_inequalities demanded) 0 nr_of_attr_vars coercions
+	= foldSt redirect_inequalities_that_contain_unused_attr_var unused_attr_vars coercions
+	  
+  where
+	add_inequalities :: !{!CoercionTree} !Int !*Coercions -> *Coercions
+	add_inequalities demanded i coercions	
+		= foldSt (\demanded coercions -> newInequality i demanded coercions)
+				(fst (flattenCoercionTree demanded.[i])) coercions
+	redirect_inequalities_that_contain_unused_attr_var :: !Int !*Coercions -> *Coercions
+	redirect_inequalities_that_contain_unused_attr_var unused_attr_var 
+				coercions=:{coer_offered, coer_demanded}
+		# (offered_attr_vars, coer_offered)
+				= accCoercionTree flattenCoercionTree unused_attr_var coer_offered
+		  (demanded_attr_vars, coer_demanded)
+				= accCoercionTree flattenCoercionTree unused_attr_var coer_demanded
+		  coer_offered = { coer_offered & [unused_attr_var] = CT_Empty }
+		  coer_offered = foldSt (appCoercionTree (removeNode unused_attr_var)) demanded_attr_vars coer_offered
+		  coer_demanded = { coer_demanded & [unused_attr_var] = CT_Empty }
+		  coer_demanded = foldSt (appCoercionTree (removeNode unused_attr_var)) offered_attr_vars coer_demanded
+		= foldSt (\(offered, demanded) coercions -> newInequality offered demanded coercions)
+				[(offered, demanded) \\ offered<-offered_attr_vars, demanded<-demanded_attr_vars]
+				{ coercions & coer_offered = coer_offered, coer_demanded = coer_demanded }
+	
+getTypeVars :: !a !*TypeVarHeap -> (!.[TypeVar],!.TypeVarHeap) | performOnTypeVars a
+getTypeVars type th_vars
+	# th_vars
+			= performOnTypeVars initializeToTVI_Empty type th_vars
+	= performOnTypeVars accum_unencountered_type_var type ([], th_vars)
+  where
+	accum_unencountered_type_var _ tv=:{tv_info_ptr} (type_var_accu, th_vars)
+		# (tvi, th_vars) = readPtr tv_info_ptr th_vars
+		= case tvi of
+			TVI_Empty
+				-> ([tv:type_var_accu], writePtr tv_info_ptr TVI_Used th_vars)
+			TVI_Used
+				-> (type_var_accu, th_vars)
+
+getAttrVars :: !a !*AttrVarHeap -> (!.[AttributeVar],!.AttrVarHeap) | performOnAttrVars a
+getAttrVars type th_attrs
+	# th_attrs
+			= performOnAttrVars initializeToAVI_Empty type th_attrs
+	= performOnAttrVars accum_unencountered_attr_var type ([], th_attrs)
+  where
+	accum_unencountered_attr_var av=:{av_info_ptr} (attr_var_accu, th_attrs)
+		# (avi, th_attrs) = readPtr av_info_ptr th_attrs
+		= case avi of
+			AVI_Empty
+				-> ([av:attr_var_accu], writePtr av_info_ptr AVI_Used th_attrs)
+			AVI_Used
+				-> (attr_var_accu, th_attrs)
+
+class performOnTypeVars a :: !(TypeAttribute TypeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each type variable
+
+instance performOnTypeVars Type
+  where
+	performOnTypeVars f (TA _ args) st
+		= performOnTypeVars f args st
+	performOnTypeVars f (at1 --> at2) st
+		= performOnTypeVars f at2 (performOnTypeVars f at1 st)
+	performOnTypeVars f (cv :@: at) st
+		= performOnTypeVars f cv (performOnTypeVars f at st)
+	performOnTypeVars f _ st
+		= st
+
+instance performOnTypeVars AType
+  where
+	performOnTypeVars f {at_attribute, at_type=TV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type=GTV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type=TQV type_var} st
+		= f at_attribute type_var st
+	performOnTypeVars f {at_attribute, at_type} st
+		= performOnTypeVars f at_type st
+
+instance performOnTypeVars ConsVariable
+  where
+	performOnTypeVars f (CV type_var) st
+		= f TA_Multi type_var st
+
+instance performOnTypeVars [a] | performOnTypeVars a
+  where
+	performOnTypeVars f [] st
+		= st
+	performOnTypeVars f [h:t] st
+		= performOnTypeVars f t (performOnTypeVars f h st)
+
+instance performOnTypeVars (a, b) | performOnTypeVars a & performOnTypeVars b
+  where
+	performOnTypeVars f (a, b) st
+		= performOnTypeVars f b (performOnTypeVars f a st)
+
+class performOnAttrVars a :: !(AttributeVar .st -> .st) !a !.st -> .st
+// run through a type and do something on each attribute variable
+
+instance performOnAttrVars Type
+  where
+	performOnAttrVars f (TA _ args) st
+		= performOnAttrVars f args st
+	performOnAttrVars f (at1 --> at2) st
+		= performOnAttrVars f at2 (performOnAttrVars f at1 st)
+	performOnAttrVars f (_ :@: at) st
+		= performOnAttrVars f at st
+	performOnAttrVars f _ st
+		= st
+
+instance performOnAttrVars AType
+  where
+	performOnAttrVars f {at_attribute=TA_Var attr_var, at_type} st
+		= performOnAttrVars f at_type (f attr_var st)
+	performOnAttrVars f {at_attribute=TA_RootVar attr_var, at_type} st
+		= performOnAttrVars f at_type (f attr_var st)
+	performOnAttrVars f {at_type} st
+		= performOnAttrVars f at_type st
+
+instance performOnAttrVars [a] | performOnAttrVars a
+  where
+	performOnAttrVars f [] st
+		= st
+	performOnAttrVars f [h:t] st
+		= performOnAttrVars f t (performOnAttrVars f h st)
+
+instance performOnAttrVars (a, b) | performOnAttrVars a & performOnAttrVars b
+  where
+	performOnAttrVars f (a, b) st
+		= performOnAttrVars f b (performOnAttrVars f a st)
+
+
+initializeToTVI_Empty :: a !TypeVar !*TypeVarHeap -> .TypeVarHeap
+initializeToTVI_Empty _ {tv_info_ptr} th_vars
+	= writePtr tv_info_ptr TVI_Empty th_vars
+
+initializeToAVI_Empty :: !AttributeVar !*AttrVarHeap -> .AttrVarHeap
+initializeToAVI_Empty {av_info_ptr} th_attrs
+	= writePtr av_info_ptr AVI_Empty th_attrs
+
+appTypeVarHeap f type_heaps :== let th_vars = f type_heaps.th_vars in { type_heaps & th_vars = th_vars }
+accTypeVarHeap f type_heaps :== let (r, th_vars) = f type_heaps.th_vars in (r, { type_heaps & th_vars = th_vars })
+accAttrVarHeap f type_heaps :== let (r, th_attrs) = f type_heaps.th_attrs in (r, { type_heaps & th_attrs = th_attrs })
+	
diff --git a/frontend/unitype.dcl b/frontend/unitype.dcl
index 0c4f726..636d0e1 100644
--- a/frontend/unitype.dcl
+++ b/frontend/unitype.dcl
@@ -3,11 +3,17 @@ definition module unitype
 import StdEnv
 import syntax, analunitypes
 
-/* MW3 moved to syntax:
-::	CoercionPosition =
-	{	cp_expression	:: !Expression
+::	CoercionState =
+	{	crc_type_heaps	:: !.TypeHeaps
+	,	crc_coercions	:: !.Coercions
+	,	crc_td_infos	:: !.TypeDefInfos
 	}
-*/
+
+class coerce a ::  !Sign !{# CommonDefs} !{# BOOLVECT} !TypePosition !a !a !*CoercionState -> (!Optional TypePosition, !*CoercionState)
+
+instance coerce AType
+
+::	TypePosition :== [Int]
 
 AttrUni			:== 0
 AttrMulti		:== 1
@@ -30,10 +36,11 @@ isUniqueAttribute		:: !Int !Coercions -> Bool
 
 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 !CoercionPosition !u:{! Type} !*Coercions !{# CommonDefs } 
-	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps !*ErrorAdmin
-		-> (!u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps, !*ErrorAdmin) 
+determineAttributeCoercions :: !AType !AType !Bool !u:{! Type} !*Coercions !{# CommonDefs } 
+	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps
+		-> (!Optional (TypePosition, AType), !u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps) 
 
 ::	AttributePartition	:== {# Int}
 
@@ -49,3 +56,11 @@ uniquenessError :: !CoercionPosition !String !*ErrorAdmin -> *ErrorAdmin
 
 liftSubstitution :: !*{! Type} !{# CommonDefs }!{# BOOLVECT } !Int !*TypeVarHeap !*TypeDefInfos -> (*{! Type}, !Int, !*TypeVarHeap, !*TypeDefInfos)
 
+::	ExpansionState = 
+	{	es_type_heaps	:: !.TypeHeaps
+	,	es_td_infos		:: !.TypeDefInfos
+	}
+
+class expandType a :: !{# CommonDefs } !{# BOOLVECT } !a !*(!u:{! Type}, !*ExpansionState) -> (!a, !*(!u:{! Type}, !*ExpansionState))
+
+instance expandType AType
diff --git a/frontend/unitype.icl b/frontend/unitype.icl
index f8219cb..1959938 100644
--- a/frontend/unitype.icl
+++ b/frontend/unitype.icl
@@ -6,12 +6,6 @@ import syntax, analunitypes, type, utilities, checktypes, RWSDebug
 
 import cheat
 
-/* MW3 moved to syntax:
-::	CoercionPosition =
-	{	cp_expression	:: !Expression
-	}
-*/
-
 AttrUni			:== 0
 AttrMulti		:== 1
 /*
@@ -49,36 +43,21 @@ isPositive :: !TempVarId !{# BOOLVECT } -> Bool
 isPositive var_id cons_vars
 	= cons_vars.[BITINDEX var_id] bitand (1 << BITNUMBER var_id) <> 0
 
-determineAttributeCoercions :: !AType !AType !Bool !CoercionPosition !u:{! Type} !*Coercions !{# CommonDefs } 
-	!{# BOOLVECT } !*TypeDefInfos !*TypeHeaps !*ErrorAdmin
-		-> (!u:{! Type}, !*Coercions, !*TypeDefInfos, !*TypeHeaps, !*ErrorAdmin) 
-determineAttributeCoercions off_type dem_type coercible position subst coercions defs cons_vars td_infos type_heaps error
+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
-		Yes positions
-			# (error=:{ea_file}) = errorHeading "Uniqueness error" error
-			  (crc_coercions, copy_crc_coercions) = uniqueCopy crc_coercions
-
-			  format = { form_properties = cMarkAttribute, form_attr_position = Yes (reverse positions, copy_crc_coercions) }			
-			  
-			  ea_file = 
-			  	case position of
-			  		CP_FunArg _ _
-			  			-> ea_file <<< "\"" <<< position <<< "\" "
-			  		_
-			  			-> ea_file
-			  ea_file = ea_file	<<< "attribute at indicated position could not be coerced "
-			  					 <:: (format, exp_off_type, Yes initialTypeVarBeautifulizer) <<< '\n'
-
-			-> (subst, crc_coercions, crc_td_infos, crc_type_heaps, { error & ea_file = ea_file })
-				
-		No
-			-> (subst, crc_coercions, crc_td_infos, crc_type_heaps, error)
-//					---> ("determineAttributeCoercions",position, (off_type, dem_type,exp_off_type,exp_dem_type))
-
+	  error_info
+	  	= case result of
+	  		No
+	  			-> No
+	  		Yes pos
+	  			-> Yes (pos, exp_off_type)
+	= (error_info, subst, crc_coercions, crc_td_infos, crc_type_heaps)
 
 NotChecked :== -1	
 DummyAttrNumber :== -1
@@ -841,7 +820,7 @@ where
 			# (succ, ct_greater) = insert new_attr ct_greater
 			= (succ, CT_Node this_attr ct_less ct_greater)
 			= (False, CT_Node this_attr ct_less ct_greater)
-	
+
 isNonUnique :: !CoercionTree -> Bool
 isNonUnique CT_NonUnique	= True
 isNonUnique _ 				= False
@@ -1050,3 +1029,9 @@ where
 	(<<<) file CT_Unique = file <<< "CT_Unique"
 	(<<<) file CT_NonUnique = file <<< "CT_NonUnique"
 	(<<<) file CT_Empty = file <<< "##"
+
+set_bit :: !Int !*{# BOOLVECT} -> .{# BOOLVECT}
+set_bit var_number bitvects
+	# bit_index = BITINDEX var_number
+	  (prev_vect, bitvects) = bitvects![bit_index]
+	= { bitvects & [bit_index] = prev_vect bitor (1 << BITNUMBER var_number) }