type.icl

implementation module type

import StdEnv
import syntax, typesupport, check, analtypes, overloading, unitype, refmark, predef, utilities, compare_constructor // , RWSDebug
import cheat, compilerSwitches
import generics // AA

::	TypeInput =
	{	ti_common_defs	:: !{# CommonDefs }
	,	ti_functions	:: !{# {# FunType }}
	,	ti_main_dcl_module_n :: !Int
	}

::	TypeState =
	{	ts_fun_env			:: !.{! FunctionType}
	,	ts_var_store		:: !TempVarId
	,	ts_attr_store		:: !TempAttrId
	,	ts_var_heap			:: !.VarHeap 
	,	ts_type_heaps		:: !.TypeHeaps
	,	ts_expr_heap		:: !.ExpressionHeap 
	,	ts_td_infos			:: !.TypeDefInfos
	,	ts_cons_variables	:: ![TempVarId]
	,	ts_exis_variables	:: ![(CoercionPosition, [TempAttrId])]
	,	ts_error			:: !.ErrorAdmin
	,	ts_out				:: !.File
	}

::	TypeCoercion =
	{	tc_demanded		:: !AType
	,	tc_offered		:: !AType
	,	tc_position		:: !CoercionPosition
	,	tc_coercible	:: !Bool
	}

::	SharedAttribute = 
	{	sa_attr_nr	:: !Int
	,	sa_position	:: !Expression
	}

::	Requirements =
	{	req_overloaded_calls	:: ![ExprInfoPtr]
	,	req_type_coercions		:: ![TypeCoercion]
	,	req_type_coercion_groups:: ![TypeCoercionGroup]
	,	req_attr_coercions		:: ![AttrCoercion]
	,	req_case_and_let_exprs	:: ![ExprInfoPtr]
	}

::	TypeCoercionGroup =
	{	tcg_type_coercions	:: ![TypeCoercion]
	,	tcg_position		:: !Position
	}

instance toString BoundVar
where
	toString varid = varid.var_name.id_name

class arraySubst type :: !type !u:{!Type} -> (!Bool,!type, !u:{! Type})

instance arraySubst AType
where
	arraySubst atype=:{at_type} subst
		# (changed, at_type, subst) = arraySubst at_type subst
		| changed
			= (True, { atype & at_type = at_type }, subst)
			= (False, atype, subst)
		
instance arraySubst Type
where
	arraySubst tv=:(TempV tv_number) subst
		#! type = subst.[tv_number]
		= case type of
			TE	-> (False,tv, subst)
			_
				# (_, type, subst) = arraySubst type subst
				-> (True, type, subst)
	arraySubst type=:(arg_type --> res_type) subst
		# (changed, (arg_type, res_type), subst) = arraySubst (arg_type, res_type) subst
		| changed
			= (changed, arg_type --> res_type, subst)
			= (False, type, subst)
	arraySubst type=:(TA cons_id cons_args) subst
		# (changed, cons_args, subst) = arraySubst cons_args subst
		| changed
			= (True, TA cons_id cons_args, subst) 
			= (False,type, subst) 
	arraySubst tcv=:(TempCV tv_number :@: types) subst
		#! type = subst.[tv_number]
		= case type of
			TE
				# (changed,types, subst) = arraySubst types subst
				| changed
					-> (True, TempCV tv_number :@: types, subst)
					-> (False, tcv, subst)
			_
				# (_, (type, types), subst) = arraySubst (type, types) subst
				  (ok, simplified_type) = simplifyTypeApplication type types
				| ok
					-> (True, simplified_type, subst)
					-> (False, tcv, subst)
//AA..					
	arraySubst type=:(TArrow1 arg_type) subst
		# (changed, arg_type, subst) = arraySubst arg_type subst
		| changed
			= (changed, TArrow1 arg_type, subst)
			= (False, type, subst)
//..AA					

	arraySubst tfa_type=:(TFA vars type) subst
		# (changed, type, subst) = arraySubst type subst
		| changed
			= (changed, TFA vars type, subst)
			= (False, tfa_type, subst)

	arraySubst type subst
		= (False, type, subst)

instance arraySubst (a,b) | arraySubst a & arraySubst b
where
	arraySubst (x,y) subst
		# (changed_x, x, subst) =  arraySubst x subst
		  (changed_y, y, subst) =  arraySubst y subst
		= (changed_x || changed_y, (x,y), subst)
		
instance arraySubst [a] | arraySubst a
where
	arraySubst [] subst
		= (False, [], subst)
	arraySubst t=:[type : types ] subst
		# (changed, (type, types), subst) = arraySubst (type, types) subst
		| changed
			= (True, [type : types ], subst)
			= (False, t, subst)
	
instance arraySubst TempSymbolType
where
	arraySubst tst=:{tst_args,tst_result,tst_context} subst
		# (changed, (tst_args, (tst_result, tst_context)), subst) = arraySubst (tst_args, (tst_result, tst_context)) subst
		| changed
			= (True, {tst & tst_args = tst_args, tst_result = tst_result, tst_context = tst_context}, subst)
			= (False, tst, subst)

instance arraySubst TypeContext
where
	arraySubst tc=:{tc_types} subst
		# (changed, tc_types, subst) = arraySubst tc_types subst
		| changed
			= (True,{ tc & tc_types = tc_types}, subst)
			= (False, tc, subst)

instance arraySubst CaseType
where
	arraySubst ct=:{ct_pattern_type, ct_result_type, ct_cons_types} subst
		# (changed, (ct_pattern_type, (ct_result_type, ct_cons_types)), subst) = arraySubst (ct_pattern_type, (ct_result_type, ct_cons_types)) subst
		| changed
			= (True,{ ct & ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, ct_cons_types = ct_cons_types }, subst)
			= (False, ct, subst)

class containsTypeVariable a :: !Int !a !{!Type} -> Bool

instance containsTypeVariable [a] | containsTypeVariable a
where
	containsTypeVariable var_id [elem:list] subst
		= containsTypeVariable var_id elem subst || containsTypeVariable var_id list subst
	containsTypeVariable var_id [] _
		= False

instance containsTypeVariable AType
where
	containsTypeVariable var_id {at_type} subst = containsTypeVariable var_id at_type subst

instance containsTypeVariable Type
where
	containsTypeVariable var_id (TempV tv_number) subst
		# type = subst.[tv_number]
		| isIndirection type
			= containsTypeVariable var_id type subst 
			= tv_number == var_id
	containsTypeVariable var_id (arg_type --> res_type) subst
		= containsTypeVariable var_id arg_type subst || containsTypeVariable var_id res_type subst
//AA..
	containsTypeVariable var_id (TArrow1 arg_type) subst
		= containsTypeVariable var_id arg_type subst
//..AA
	containsTypeVariable var_id (TA cons_id cons_args) subst
		= containsTypeVariable var_id cons_args subst
	containsTypeVariable var_id (type :@: types) subst
		= containsTypeVariable var_id type subst || containsTypeVariable var_id types subst
	containsTypeVariable _ _ _
		= False

instance containsTypeVariable ConsVariable
where
	containsTypeVariable var_id (TempCV tv_number) subst
		# type = subst.[tv_number]
		| isIndirection type
			= containsTypeVariable var_id type subst 
			= tv_number == var_id
	containsTypeVariable var_id _ _
		= False

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
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
			  err = errorHeading type_error err
			  err = popErrorAdmin err
//			-> { err & ea_file = err.ea_file <<< " cannot unify " <:: (type_error_format, t1, Yes initialTypeVarBeautifulizer) 
//											<<< " with " <:: (type_error_format, t2, Yes initialTypeVarBeautifulizer) <<< '\n' }
			-> { err & ea_file = err.ea_file <<< " cannot unify " <:: (type_error_format, t1, No) 
											<<< " with " <:: (type_error_format, t2, No) <<< '\n' }
		_
			-> cannot_unify t1 t2 position err 
cannotUnify t1 t2 position err 
	= cannot_unify t1 t2 position err 

cannot_unify t1 t2 position err
	# (err=:{ea_file}) = errorHeading type_error err
	  ea_file = case position of
				CP_FunArg _ _
					-> ea_file <<< "\"" <<< position <<< "\""
				_
					-> ea_file
	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, No) 
						<<< " with " <:: (type_error_format, t2, No)
//	  ea_file = ea_file <<< " cannot unify " <:: (type_error_format, t1, Yes initialTypeVarBeautifulizer) 
//						<<< " with " <:: (type_error_format, t2, Yes initialTypeVarBeautifulizer)
	  ea_file = case position of
	  			CP_FunArg _ _
	  				-> ea_file
  				_
	  				-> ea_file <<< " near " <<< position
	= { err & ea_file = ea_file <<< '\n' }


existentialError position=:(CP_Expression expr) err=:{ea_loc=[ip:_]} 
	= case tryToOptimizePosition expr of
		Yes (id_name, line)
			# err = pushErrorAdmin { ip & ip_ident.id_name = id_name, ip_line = line } err
			  err = errorHeading type_error err
			  err = popErrorAdmin err
			-> { err & ea_file = err.ea_file <<< " attribute variable could not be universally quantified"<<< '\n' }
		_
			# err = errorHeading type_error err
			-> { err & ea_file = err.ea_file <<< " attribute variable could not be universally quantified"<<< '\n' }
			

tryToOptimizePosition (Case {case_ident=Yes {id_name}})
	= optBeautifulizeIdent id_name
tryToOptimizePosition (App {app_symb={symb_name}})
	= optBeautifulizeIdent symb_name.id_name
tryToOptimizePosition (fun @ _)
	= tryToOptimizePosition fun
tryToOptimizePosition _
	= No

isIndirection TE	= False
isIndirection type	= True

class unify a :: !a !a !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)

instance unify (a, b) | unify a & unify b
where
	unify (t1x, t1y) (t2x, t2y) modules subst heaps
		# (succ, subst, heaps) =  unify t1y t2y modules subst heaps
		| succ
	      = unify t1x t2x modules subst heaps
	      = (False, subst, heaps)

instance unify [a] | unify a
where
	unify [t1 : ts1] [t2 : ts2] modules subst heaps
		= unify (t1,ts1) (t2,ts2) modules subst heaps
	unify [] [] modules subst heaps
		= (True, subst, heaps)
	unify _ _ modules subst heaps
		= (False, subst, heaps)

instance unify AType
where
	unify t1 t2 modules subst heaps = unifyTypes t1.at_type t1.at_attribute t2.at_type t2.at_attribute modules subst heaps

unifyTypes :: !Type !TypeAttribute !Type !TypeAttribute !TypeInput !*{! Type} !*TypeHeaps -> (!Bool, !*{! Type}, !*TypeHeaps)
unifyTypes tv=:(TempV tv_number) attr1 type2 attr2 modules subst heaps
	# (type1, subst) = subst![tv_number]
	| isIndirection type1
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		# (succ, subst) = unify_variable_with_type tv_number type2 subst
		= (succ, subst, heaps)
	where	
		unify_variable_with_type tv_number1 tv=:(TempV tv_number2) subst
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				= unify_variable_with_type tv_number type2 subst
			| tv_number1 == tv_number2
				= (True, subst)
				= (True, { subst & [tv_number1] = tv})
		unify_variable_with_type tv_number type subst
			| containsTypeVariable tv_number type subst
				= (False, subst)
//					---> "unify_variable_with_type"
				= (True, { subst & [tv_number] = type})
unifyTypes type attr1 tv=:(TempV _) attr2 modules subst heaps
	= unifyTypes tv attr2 type attr1 modules subst heaps
unifyTypes t1=:(TB tb1) attr1 t2=:(TB tb2) attr2 modules subst heaps
	| tb1 == tb2
		= (True, subst, heaps)
		= (False, subst, heaps)
unifyTypes (arg_type1 --> res_type1) attr1 (arg_type2 --> res_type2) attr2 modules subst heaps
	= unify (arg_type1,res_type1) (arg_type2,res_type2) modules subst heaps
//AA..	
unifyTypes TArrow attr1 TArrow attr2 modules subst heaps
	= (True, subst, heaps)	
unifyTypes (TArrow1 t1) attr1 (TArrow1 t2) attr2 modules subst heaps
	= unify t1 t2 modules subst heaps	
//..AA
unifyTypes t1=:(TA cons_id1 cons_args1) attr1 t2=:(TA cons_id2 cons_args2) attr2 modules subst heaps
	| cons_id1 == cons_id2
		= unify cons_args1 cons_args2 modules subst heaps
		# (succ1, t1, heaps) = tryToExpand t1 attr1 modules.ti_common_defs heaps
		  (succ2, t2, heaps) = tryToExpand t2 attr2 modules.ti_common_defs heaps
		| succ1 || succ2
			= unifyTypes t1 attr1 t2 attr2 modules subst heaps
			= (False, subst, heaps)
//				---> "unifyTypes1"
unifyTypes (cons_var :@: types) attr1 type2 attr2 modules subst heaps
	# (_, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr1 types type2 attr2 modules subst heaps
unifyTypes type1 attr1 (cons_var :@: types) attr2 modules subst heaps
	# (_, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	= unifyTypeApplications cons_var attr2 types type1 attr1 modules subst heaps
unifyTypes t1=:(TempQV qv_number1) attr1 t2=:(TempQV qv_number2) attr2 modules subst heaps
	= (qv_number1 == qv_number2, subst, heaps)
unifyTypes (TempQV qv_number) attr1 type attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type attr1 (TempQV qv_number1) attr2 modules subst heaps
	= (False, subst, heaps)
unifyTypes type1 attr1 type2 attr2 modules subst heaps
	# (succ1, type1, heaps) = tryToExpand type1 attr1 modules.ti_common_defs heaps
	  (succ2, type2, heaps) = tryToExpand type2 attr2 modules.ti_common_defs heaps
	| succ1 || succ2
		= unifyTypes type1 attr1 type2 attr2 modules subst heaps
		= (False, subst, heaps)

tryToExpand :: !Type !TypeAttribute !{# CommonDefs} !*TypeHeaps -> (!Bool, !Type, !*TypeHeaps)
tryToExpand type=:(TA {type_index={glob_object,glob_module}} type_args) type_attr ti_common_defs type_heaps
	#! type_def = ti_common_defs.[glob_module].com_type_defs.[glob_object]
	= case type_def.td_rhs of
		SynType {at_type}
			# (_, expanded_type, type_heaps) = substituteType type_def.td_attribute type_attr type_def.td_args type_args at_type type_heaps
			-> (True, expanded_type, type_heaps)
		_
			-> (False, type, type_heaps)
tryToExpand type type_attr modules type_heaps
	= (False, type, type_heaps)

toTV is_exist temp_var_id
	| is_exist
		= TempQV temp_var_id
		= TempV temp_var_id

toCV is_exist temp_var_id
	| is_exist
		= TempQCV temp_var_id
		= TempCV temp_var_id

simplifyTypeApplication :: !Type ![AType] -> (!Bool, !Type)
simplifyTypeApplication (TA type_cons=:{type_arity} cons_args) type_args
	= (True, TA { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args))
simplifyTypeApplication (cons_var :@: types) type_args
	= (True, cons_var :@: (types ++ type_args))
simplifyTypeApplication (TempV tv_number) type_args
	= (True, TempCV tv_number :@: type_args)
simplifyTypeApplication (TempQV tv_number) type_args
	= (True, TempQCV tv_number :@: type_args)
//AA..
simplifyTypeApplication TArrow [type1, type2] 
	= (True, type1 --> type2)
simplifyTypeApplication TArrow [type] 
	= (True, TArrow1 type)
simplifyTypeApplication (TArrow1 type1) [type2] 
	= (True, type1 --> type2)
//..AA
simplifyTypeApplication type type_args
	= (False, type)

unifyTypeApplications (TempCV tv_number) attr1 type_args type2 attr2 modules subst heaps
	# (type1, subst) = subst![tv_number]
	| isIndirection type1
		# (ok, simplified_type) = simplifyTypeApplication type1 type_args
		| ok
			= unifyTypes simplified_type attr1 type2 attr2 modules subst heaps
			= (False, subst, heaps)
		= unifyCVwithType False tv_number type_args type2 modules subst heaps
unifyTypeApplications (TempQCV tv_number) attr1 type_args type2 attr2 modules subst heaps
	= unifyCVwithType True tv_number type_args type2 modules subst heaps
		
unifyCVwithType is_exist tv_number1 type_args1 type=:(cv :@: type_args2) modules subst heaps
	= case cv of
		TempCV tv_number2
			# (type2, subst) = subst![tv_number2]
			| isIndirection type2
				# (ok, simplified_type) = simplifyTypeApplication type2 type_args2
				| ok
					-> unifyCVwithType is_exist tv_number1 type_args1 simplified_type modules subst heaps
					-> (False, subst, heaps)
				-> unifyCVApplicationwithCVApplication is_exist tv_number1 type_args1 False tv_number2 type_args2 modules subst heaps
		TempQCV tv_number2
				-> unifyCVApplicationwithCVApplication is_exist tv_number1 type_args1 True tv_number2 type_args2 modules subst heaps

unifyCVwithType is_exist tv_number type_args type=:(TA type_cons cons_args) modules subst heaps
	# diff = type_cons.type_arity - length type_args
	| diff >= 0 
		# (succ, subst, heaps) = unify type_args (drop diff cons_args) modules subst heaps
		| succ
			= unifyTypes (toTV is_exist tv_number) TA_Multi (TA { type_cons & type_arity = diff } (take diff cons_args)) TA_Multi modules subst heaps
		    = (False, subst, heaps)
		= (False, subst, heaps)

// AA..
unifyCVwithType is_exist tv_number [type_arg1, type_arg2] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify (type_arg1, type_arg2) (atype1, atype2) modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)		
unifyCVwithType is_exist tv_number [type_arg] type=:(atype1 --> atype2) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype2 modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi (TArrow1 atype1) TA_Multi modules subst heaps
		= (False, subst, heaps)
unifyCVwithType is_exist tv_number [] type=:(atype1 --> atype2) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps
		
unifyCVwithType is_exist tv_number [type_arg] type=:(TArrow1 atype) modules subst heaps
	# (succ, subst, heaps) = unify type_arg atype modules subst heaps
	| succ
		= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
		= (False, subst, heaps)
unifyCVwithType is_exist tv_number [] type=:(TArrow1 atype) modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi type TA_Multi modules subst heaps

unifyCVwithType is_exist tv_number [] TArrow modules subst heaps
	= unifyTypes (toTV is_exist tv_number) TA_Multi TArrow TA_Multi modules subst heaps
// ..AA 		

unifyCVwithType is_exist tv_number type_args type modules subst heaps
	= (False, subst, heaps)

unifyCVApplicationwithCVApplication is_exist1 tv_number1 type_args1 is_exist2 tv_number2 type_args2 modules subst heaps
	# arity1 = length type_args1
	  arity2 = length type_args2
	  diff = arity1 - arity2
	| diff == 0
		# (succ, subst) = unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
		| succ
		    = unify type_args1 type_args2 modules subst heaps
			= (False, subst, heaps)
	| diff < 0
		# diff = 0 - diff
		  (succ, subst, heaps) = unifyTypes (toTV is_exist1 tv_number1) TA_Multi (toCV is_exist2 tv_number2 :@: take diff type_args2) TA_Multi modules subst heaps
		| succ
		    = unify type_args1 (drop diff type_args2) modules subst heaps
			= (False, subst, heaps)
//	| otherwise
		# (succ, subst, heaps) = unifyTypes (toCV is_exist1 tv_number1 :@: take diff type_args1) TA_Multi (toTV is_exist2 tv_number2) TA_Multi modules subst heaps
		| succ
		    = unify (drop diff type_args1) type_args2 modules subst heaps
			= (False, subst, heaps)
	where
		unify_cv_with_cv is_exist1 tv_number1 is_exist2 tv_number2 subst
			| tv_number1 == tv_number2
				= (True, subst)
			| is_exist1
				| is_exist2
					= (False, subst)
					= (True, { subst & [tv_number2] = TempQV tv_number1})
				| is_exist2
					= (True, { subst & [tv_number1] = TempQV tv_number2})
					= (True, { subst & [tv_number1] = TempV tv_number2})
		
	
instance fromInt TypeAttribute
where
	fromInt AttrUni		= TA_Unique
	fromInt AttrMulti	= TA_Multi
	fromInt av_number	= TA_TempVar av_number

class freshCopy a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)

instance freshCopy [a] | freshCopy a
where
	freshCopy l ls = mapSt freshCopy l ls

freshCopyOfAttributeVar {av_name,av_info_ptr} attr_var_heap
	# (av_info, attr_var_heap) = readPtr av_info_ptr attr_var_heap
	= case av_info of
		AVI_Attr attr
			-> (attr, attr_var_heap)
		_
			-> abort ("freshCopyOfAttributeVar (type,icl)" ---> av_name)


freshCopyOfTypeAttribute (TA_Var avar) attr_var_heap
	= freshCopyOfAttributeVar avar attr_var_heap

/* A temporary hack to handle the new Object IO lib */
/* Should be removed !!!!!!!!!! */

freshCopyOfTypeAttribute (TA_RootVar avar) attr_var_heap
	= PA_BUG (TA_PA_BUG, attr_var_heap) (freshCopyOfAttributeVar avar attr_var_heap)
freshCopyOfTypeAttribute TA_None attr_var_heap
	= (TA_Multi, attr_var_heap)
freshCopyOfTypeAttribute TA_Unique attr_var_heap
	= (TA_Unique, attr_var_heap)
freshCopyOfTypeAttribute attr attr_var_heap
	= (attr, attr_var_heap)


cIsExistential 		:== True
cIsNotExistential	:== False

freshCopyOfTypeVariable {tv_name,tv_info_ptr} type_heaps=:{th_vars}
	# (TVI_Type fresh_var, th_vars)	= readPtr tv_info_ptr th_vars
	= (fresh_var, { type_heaps & th_vars = th_vars })

freshConsVariable {tv_info_ptr} type_var_heap
	# (tv_info, type_var_heap) = readPtr tv_info_ptr type_var_heap
	= (to_constructor_variable tv_info, type_var_heap)
	where
		to_constructor_variable (TVI_Type (TempV temp_var_id))
			= TempCV temp_var_id
		to_constructor_variable (TVI_Type (TempQV temp_var_id))
			= TempQCV temp_var_id

instance freshCopy AType
where 	
	freshCopy type=:{at_type = cv :@: types, at_attribute} type_heaps=:{th_attrs}
		# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute th_attrs
		# (fresh_types, type_heaps)		= freshCopy types { type_heaps & th_attrs = th_attrs }
		= case cv of
			CV tv
				# (fresh_cons_var, th_vars)	= freshConsVariable tv type_heaps.th_vars
				-> ({type & at_type = fresh_cons_var :@: fresh_types, at_attribute = fresh_attribute }, { type_heaps & th_vars = th_vars })
			_
				-> ({type & at_type = cv :@: fresh_types, at_attribute = fresh_attribute}, type_heaps)
	freshCopy type=:{at_type, at_attribute} type_heaps=:{th_attrs}
		# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute th_attrs
		  (fresh_type, type_heaps)		= freshCopy at_type { type_heaps & th_attrs = th_attrs }
		= ({ type & at_type = fresh_type, at_attribute = fresh_attribute }, type_heaps)

instance freshCopy Type
where
	freshCopy (TV tv) type_heaps
		= freshCopyOfTypeVariable tv type_heaps
	freshCopy (TA cons_id=:{type_index={glob_object,glob_module}} cons_args)  type_heaps
		# (cons_args, type_heaps) = freshCopy cons_args type_heaps
		= (TA cons_id cons_args, type_heaps)
	freshCopy (arg_type --> res_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		  (res_type, type_heaps) = freshCopy res_type type_heaps
		= (arg_type --> res_type, type_heaps)
//AA..
	freshCopy (TArrow1 arg_type) type_heaps
		# (arg_type, type_heaps) = freshCopy arg_type type_heaps
		= (TArrow1 arg_type, type_heaps)
//..AA		
	freshCopy (TFA vars type) type_heaps
		# type_heaps = foldSt bind_var_and_attr vars type_heaps
		  (type, type_heaps) = freshCopy type type_heaps
		# type_heaps = clearBindings vars type_heaps
		= (TFA vars type, type_heaps)
	where
		bind_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
			= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = bind_attr atv_attribute th_attrs }
		where
			bind_attr var=:(TA_Var {av_info_ptr}) attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Attr var)
			bind_attr attr attr_heap
				= attr_heap
	freshCopy type type_heaps
		= (type, type_heaps)

freshExistentialVariables type_variables state
	= foldSt fresh_existential_variable type_variables state 
where
	fresh_existential_variable {atv_variable={tv_info_ptr}} (var_heap, var_store)
		= (var_heap <:= (tv_info_ptr, TVI_Type (TempQV var_store)), inc var_store)

fresh_type_variables :: [ATypeVar] *(*Heap TypeVarInfo,Int) -> *(!*Heap TypeVarInfo,!Int);
fresh_type_variables type_variables state
	= foldSt (\{atv_variable={tv_info_ptr}} (var_heap, var_store) -> (var_heap <:= (tv_info_ptr, TVI_Type (TempV var_store)), inc var_store))
				type_variables state

fresh_attributes :: [AttributeVar] *(*Heap AttrVarInfo,Int) -> *(!*Heap AttrVarInfo,!Int);
fresh_attributes attributes state
	= foldSt (\{av_info_ptr} (attr_heap, attr_store) -> (attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)), inc attr_store))
		attributes state

fresh_environment :: [AttrInequality] [AttrCoercion] *(Heap AttrVarInfo) -> *(![AttrCoercion],!*Heap AttrVarInfo);
fresh_environment inequalities attr_env attr_heap
	= foldSt fresh_inequality inequalities (attr_env, attr_heap)
	where
		fresh_inequality {ai_demanded,ai_offered} (attr_env, attr_heap)
			# (AVI_Attr dem_temp_attr, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
			  (AVI_Attr off_temp_attr, attr_heap) = readPtr ai_offered.av_info_ptr attr_heap
			= case dem_temp_attr of
				TA_TempVar dem_attr_var
					-> case off_temp_attr of
						TA_TempVar off_attr_var
							| is_new_ineqality  dem_attr_var off_attr_var attr_env
								-> ([{ac_demanded = dem_attr_var, ac_offered = off_attr_var} : attr_env ], attr_heap)
								-> (attr_env, attr_heap)
						_
							-> (attr_env, attr_heap)
				_
					-> (attr_env, attr_heap)
			
		is_new_ineqality dem_attr_var off_attr_var [{ac_demanded, ac_offered} : attr_env]
			= (dem_attr_var <> ac_demanded || off_attr_var <> ac_offered) && is_new_ineqality dem_attr_var off_attr_var  attr_env
		is_new_ineqality dem_attr_var off_attr_var []
			= True

fresh_symbol_types [{ap_symbol={glob_object}}] cons_defs var_store type_heaps
	# {cons_type = {st_args,st_attr_env,st_result}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
	  (th_vars, var_store)		= freshExistentialVariables  cons_exi_vars (type_heaps.th_vars, var_store)
  	  (attr_env, th_attrs) 		= fresh_environment st_attr_env [] type_heaps.th_attrs
  	  (result_type, type_heaps)	= freshCopy st_result { type_heaps & th_attrs = th_attrs, th_vars = th_vars }
  	  (fresh_args, type_heaps)	= freshCopy st_args type_heaps
	= ([fresh_args], result_type, var_store, attr_env, type_heaps)
fresh_symbol_types [{ap_symbol={glob_object}} : patterns] cons_defs var_store type_heaps
	# (cons_types, result_type, var_store, attr_env, type_heaps)
			= fresh_symbol_types patterns cons_defs var_store type_heaps
	  {cons_type = {st_args,st_attr_env}, cons_index, cons_exi_vars} = cons_defs.[glob_object.ds_index]
	  (th_vars, var_store)		= freshExistentialVariables cons_exi_vars (type_heaps.th_vars, var_store)
	  (attr_env, th_attrs) 		= fresh_environment st_attr_env attr_env type_heaps.th_attrs
  	  (fresh_args, type_heaps) 	= freshCopy st_args { type_heaps & th_attrs = th_attrs, th_vars = th_vars }
	= ([fresh_args : cons_types], result_type, var_store, attr_env, type_heaps)

freshUniversalVariables type_variables state
	= foldSt fresh_universal_variable type_variables state 
where
	fresh_universal_variable {atv_variable={tv_info_ptr}} (var_heap, var_store)
		= (var_heap <:= (tv_info_ptr, TVI_Type (TempQV var_store)), inc var_store)

freshAlgebraicType :: !(Global Int) ![AlgebraicPattern] !{#CommonDefs} !*TypeState -> (![[AType]],!AType,![AttrCoercion],!*TypeState)
freshAlgebraicType {glob_module, glob_object} patterns common_defs ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_td_infos}
	# {td_rhs,td_args,td_attrs,td_name,td_attribute} = common_defs.[glob_module].com_type_defs.[glob_object]
	# (th_vars, ts_var_store)		= fresh_type_variables td_args (ts_type_heaps.th_vars, ts_var_store)
	  (th_attrs, ts_attr_store)		= fresh_attributes td_attrs (ts_type_heaps.th_attrs, ts_attr_store)
	  type_heaps					= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (cons_types, alg_type, ts_var_store, attr_env, type_heaps)
	  		= fresh_symbol_types patterns common_defs.[glob_module].com_cons_defs ts_var_store type_heaps
	= (cons_types, alg_type, attr_env, { ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps })
//		---> ("freshAlgebraicType", alg_type, cons_types)

fresh_overloaded_list_type [{ap_symbol}:patterns] pd_cons_symbol pd_nil_symbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
	| ap_symbol.glob_module==cPredefinedModuleIndex
		| ap_symbol.glob_object.ds_index==pd_cons_symbol-FirstConstructorPredefinedSymbolIndex
			# (argument_types,result_type,tst_context,tst_attr_env,ts) = make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			= case patterns of
				[]
					-> ([argument_types],result_type,tst_context,tst_attr_env,ts)
				[pattern=:{ap_symbol}]
					| ap_symbol.glob_module==cPredefinedModuleIndex && ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
						-> ([argument_types,[]],result_type,tst_context,tst_attr_env,ts)
		| ap_symbol.glob_object.ds_index==pd_nil_symbol-FirstConstructorPredefinedSymbolIndex
			= case patterns of
				[]
					# {ft_type,ft_symb,ft_type_ptr,ft_specials} = functions.[stdStrictLists_index].[nil_u_index]
					# (fun_type_copy, ts) = determineSymbolTypeOfFunction pos ft_symb 0/*symb_arity*/ ft_type ft_type_ptr common_defs ts
					  {tst_args,tst_result,tst_context,tst_attr_env}=fun_type_copy
					-> ([tst_args],tst_result,tst_context,tst_attr_env,ts)
				[pattern=:{ap_symbol}]
					| ap_symbol.glob_module==cPredefinedModuleIndex && ap_symbol.glob_object.ds_index==pd_cons_symbol-FirstConstructorPredefinedSymbolIndex
						# (argument_types,result_type,tst_context,tst_attr_env,ts) = make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
						-> ([[],argument_types],result_type,tst_context,tst_attr_env,ts)
			= abort "fresh_overloaded_list_type"
	where
		make_cons_type_from_decons_type stdStrictLists_index decons_u_index common_defs ts
			# {me_symb,me_type,me_type_ptr} = common_defs.[stdStrictLists_index].com_member_defs.[decons_u_index]
			  (fun_type_copy,ts) = determineSymbolTypeOfFunction pos me_symb 1/*symb_arity*/ me_type me_type_ptr common_defs ts
			  {tst_args,tst_arity,tst_lifted,tst_result,tst_context,tst_attr_env}=fun_type_copy						  
			# result_type = case tst_args of [t] -> t
			# argument_types = case tst_result.at_type of (TA _ args=:[arg1,arg2]) ->args
			= (argument_types,result_type,tst_context,tst_attr_env,ts)

freshOverloadedListType :: !OverloadedListType !CoercionPosition ![AlgebraicPattern] !{#CommonDefs} !{#{#FunType }} !*TypeState -> (![[AType]],!AType,![TypeContext],![AttrCoercion],!*TypeState)
freshOverloadedListType (UnboxedList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_UnboxedConsSymbol PD_UnboxedNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
freshOverloadedListType (UnboxedTailStrictList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_UnboxedTailStrictConsSymbol PD_UnboxedTailStrictNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts
freshOverloadedListType (OverloadedList _ stdStrictLists_index decons_u_index nil_u_index) pos patterns common_defs functions ts
	= fresh_overloaded_list_type patterns PD_OverloadedConsSymbol PD_OverloadedNilSymbol decons_u_index nil_u_index stdStrictLists_index pos functions common_defs ts

cWithFreshContextVars 		:== True
cWithoutFreshContextVars 	:== False

freshSymbolType :: !(Optional CoercionPosition) !Bool !SymbolType {#u:CommonDefs} !*TypeState -> (!TempSymbolType,!*TypeState)
freshSymbolType is_appl fresh_context_vars st=:{st_vars,st_args,st_result,st_context,st_attr_vars,st_attr_env,st_arity} common_defs
				ts=:{ts_var_store,ts_attr_store,ts_type_heaps,ts_td_infos,ts_var_heap,ts_cons_variables,ts_exis_variables}
	# (th_vars, ts_var_store)	= fresh_type_variables st_vars (ts_type_heaps.th_vars, ts_var_store)
	  (th_attrs, ts_attr_store)	= fresh_attributes st_attr_vars (ts_type_heaps.th_attrs, ts_attr_store)
	  (attr_env, th_attrs)		= freshEnvironment st_attr_env th_attrs 
	  type_heaps 				= { ts_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
	  (tst_args, (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps))
	  							= fresh_arg_types is_appl st_args (ts_var_store, ts_attr_store, ts_exis_variables, type_heaps)
	  (tst_result, type_heaps)	= freshCopy st_result type_heaps
	  (tst_context, (type_heaps, ts_var_heap)) 	= freshTypeContexts fresh_context_vars st_context (type_heaps, ts_var_heap)
	  cons_variables			= foldSt (collect_cons_variables_in_tc common_defs) tst_context [] 
	= ({ tst_args = tst_args, tst_result = tst_result, tst_context = tst_context, tst_attr_env = attr_env, tst_arity = st_arity, tst_lifted = 0 },
	   { ts & ts_var_store = ts_var_store, ts_attr_store = ts_attr_store, ts_type_heaps = type_heaps, ts_var_heap = ts_var_heap,
	   				ts_cons_variables = cons_variables ++ ts_cons_variables, ts_exis_variables = ts_exis_variables })
		//---> ("freshSymbolType", st, tst_args, tst_result, tst_context)
	where
		fresh_type_variables :: .[TypeVar] *(*Heap TypeVarInfo,.Int) -> (!.Heap TypeVarInfo,!Int);
		fresh_type_variables type_variables state
			= foldr (\{tv_info_ptr} (var_heap, var_store) -> (writePtr tv_info_ptr (TVI_Type (TempV var_store)) var_heap, inc var_store))
							state type_variables

		fresh_attributes :: .[AttributeVar] *(*Heap AttrVarInfo,.Int) -> (!.Heap AttrVarInfo,!Int);
		fresh_attributes attributes state
			= foldr (\{av_info_ptr} (attr_heap, attr_store) -> (writePtr av_info_ptr (AVI_Attr (TA_TempVar attr_store)) attr_heap, inc attr_store))
							state attributes

		collect_cons_variables_in_tc common_defs tc=:{tc_class={glob_module,glob_object={ds_index}}, tc_types} collected_cons_vars
			# {class_cons_vars} = common_defs.[glob_module].com_class_defs.[ds_index]
			= collect_cons_variables tc_types class_cons_vars collected_cons_vars
		
		collect_cons_variables [] class_cons_vars collected_cons_vars
			= collected_cons_vars
		collect_cons_variables [type : tc_types] class_cons_vars collected_cons_vars
			| class_cons_vars bitand 1 == 0
				= collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
				= case type of
					TempV temp_var_id 
						-> collect_cons_variables tc_types (class_cons_vars >> 1) (add_variable temp_var_id collected_cons_vars)
//							---> ("collect_cons_variables", temp_var_id)
					_
						-> collect_cons_variables tc_types (class_cons_vars >> 1) collected_cons_vars
						
		add_variable new_var_id []
			= [new_var_id]
		add_variable new_var_id vars=:[var_id : var_ids]
			| new_var_id == var_id
				= vars
				= [var_id : add_variable new_var_id var_ids]
				
		fresh_arg_types No arg_types (var_store, attr_store, exis_variables, type_heaps)
			# (arg_types, type_heaps) = freshArgumentsOfSymbolType arg_types type_heaps
			= (arg_types, (var_store, attr_store, exis_variables, type_heaps))
		fresh_arg_types (Yes pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
			= mapSt (fresh_arg_type pos) arg_types (var_store, attr_store, exis_variables, type_heaps)
		where
			fresh_arg_type pos at=:{at_attribute, at_type = TFA vars type} (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_attribute, th_attrs)	= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
				# (var_store, attr_store, new_exis_variables, type_heaps)
						= foldSt fresh_var_and_attr vars (var_store, attr_store, [], { type_heaps & th_attrs = th_attrs })
				  (fresh_type, type_heaps)				= freshCopy type type_heaps
				  type_heaps							= clearBindings vars type_heaps
				= ({ at &  at_attribute = fresh_attribute, at_type = fresh_type },
						(var_store, attr_store, add_exis_variables pos new_exis_variables exis_variables, type_heaps))
			fresh_arg_type _ at (var_store, attr_store, exis_variables, type_heaps)
				# (fresh_at, type_heaps) = freshCopy at type_heaps
				= (fresh_at, (var_store, attr_store, exis_variables, type_heaps))

			fresh_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} (var_store, attr_store, exis_variables, type_heaps)
				# (attr_store, exis_variables, th_attrs) = fresh_attr atv_attribute (attr_store, exis_variables, type_heaps.th_attrs)
				= (inc var_store,  attr_store, exis_variables, { type_heaps & th_vars = type_heaps.th_vars <:= (tv_info_ptr, TVI_Type (TempQV var_store)), th_attrs = th_attrs })
			where
				fresh_attr var=:(TA_Var {av_info_ptr}) (attr_store, exis_variables, attr_heap)
					= (inc attr_store, [attr_store : exis_variables], attr_heap <:= (av_info_ptr, AVI_Attr (TA_TempVar attr_store)))
				fresh_attr attr state
					= state
			
			add_exis_variables pos [] exis_variables
				= exis_variables
			add_exis_variables pos new_exis_variables exis_variables
				= [(pos, new_exis_variables) : exis_variables]

freshArgumentsOfSymbolType :: ![AType] !*TypeHeaps -> (![AType], !*TypeHeaps)
freshArgumentsOfSymbolType atypes type_heaps = mapSt fresh_arg_type atypes type_heaps
where
	fresh_arg_type at=:{at_attribute, at_type = TFA vars type} type_heaps
		# (fresh_attribute, th_attrs)			= freshCopyOfTypeAttribute at_attribute type_heaps.th_attrs
		# type_heaps							= foldSt bind_var_and_attr vars { type_heaps & th_attrs = th_attrs }
		  (fresh_type, type_heaps)				= freshCopy type type_heaps
		  type_heaps							= clearBindings vars type_heaps
		= ({ at &  at_attribute = fresh_attribute, at_type = TFA vars fresh_type }, type_heaps)
	where
		bind_var_and_attr {atv_attribute, atv_variable = tv=:{tv_info_ptr}} type_heaps=:{th_vars,th_attrs}
			= { type_heaps & th_vars = th_vars <:= (tv_info_ptr, TVI_Type (TV tv)), th_attrs = bind_attr atv_attribute th_attrs }
		where
			bind_attr var=:(TA_Var {av_info_ptr}) attr_heap
				= attr_heap <:= (av_info_ptr, AVI_Attr var)
			bind_attr attr attr_heap
				= attr_heap
	fresh_arg_type at type_heaps
		= freshCopy at type_heaps
	
freshInequality :: AttrInequality *(Heap AttrVarInfo) -> (!AttrCoercion,!.Heap AttrVarInfo);
freshInequality {ai_demanded,ai_offered} attr_heap
	# (av_dem_info, attr_heap) = readPtr ai_demanded.av_info_ptr attr_heap
	  (av_off_info, attr_heap) = readPtr ai_offered.av_info_ptr attr_heap
	  (AVI_Attr (TA_TempVar dem_attr_var)) = av_dem_info
	  (AVI_Attr (TA_TempVar off_attr_var)) = av_off_info
	= ({ac_demanded = dem_attr_var, ac_offered = off_attr_var}, attr_heap) // <<- (av_dem_info,av_off_info)
	
freshEnvironment [ineq : ineqs] attr_heap
	# (fresh_ineq, attr_heap) = freshInequality ineq attr_heap
	  (fresh_env, attr_heap) = freshEnvironment ineqs attr_heap
	= ([fresh_ineq : fresh_env], attr_heap)
freshEnvironment [] attr_heap
	= ([], attr_heap)

freshTypeContexts fresh_context_vars tcs cs_and_var_heap
	= mapSt (fresh_type_context fresh_context_vars) tcs cs_and_var_heap
where	
	fresh_type_context fresh_context_vars tc=:{tc_types} (type_heaps, var_heap)
		# (tc_types, type_heaps) = mapSt fresh_context_type tc_types type_heaps
		| fresh_context_vars
			# (new_info_ptr, var_heap) = newPtr VI_Empty var_heap
			= ({ tc & tc_types = tc_types, tc_var = new_info_ptr }, (type_heaps, var_heap))
			= ({ tc & tc_types = tc_types}, (type_heaps, var_heap))

	fresh_context_type (CV tv :@: types) type_heaps=:{th_vars}
		# (fresh_cons_var, th_vars)		= freshConsVariable tv th_vars
		  (types, type_heaps) = freshCopy types { type_heaps & th_vars = th_vars }
		= (fresh_cons_var :@: types, type_heaps)
	fresh_context_type type type_heaps
		= freshCopy type type_heaps

freshAttributedVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshAttributedVariable ts=:{ts_var_store,ts_attr_store}
	= ({ at_attribute = TA_TempVar ts_attr_store, at_annotation = AN_None, at_type = TempV ts_var_store },
	     {ts & ts_var_store = inc ts_var_store, ts_attr_store = inc ts_attr_store})

freshNonUniqueVariable :: !u:TypeState -> (!AType, !u:TypeState)
freshNonUniqueVariable ts=:{ts_var_store}
	= ({ at_attribute = TA_Multi, at_annotation = AN_None, at_type = TempV ts_var_store },
	     {ts & ts_var_store = inc ts_var_store})

freshAttribute :: !u:TypeState -> (!TypeAttribute, !u:TypeState)
freshAttribute ts=:{ts_attr_store}
	= (TA_TempVar ts_attr_store, {ts & ts_attr_store = inc ts_attr_store})


::	PropState =
	{	prop_type_heaps	:: !.TypeHeaps
	,	prop_td_infos	:: !.TypeDefInfos
	,	prop_attr_vars	:: ![AttributeVar]
	,	prop_attr_env	:: ![AttrInequality]
	,	prop_error		:: !.Optional .ErrorAdmin
	}

attribute_error type_attr No
	= No // XXX abort ("sanity check nr 723 failed in module type"--->("type_attr", type_attr))
attribute_error type_attr (Yes err)
	# err = errorHeading "Type error" err
	= 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},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
	= ({ 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 })
	where
		add_propagation_attributes_to_atypes modules [] ps
			= ([], [], ps) 
		add_propagation_attributes_to_atypes modules [atype : atypes] ps
			# (atype, prop_class, ps) = addPropagationAttributesToAType modules atype ps
			  (atypes, prop_classes, ps) = add_propagation_attributes_to_atypes modules atypes ps
			= ([atype : atypes], [prop_class : prop_classes], ps)
	
		determine_attribute_of_cons modules TA_Unique cons_args prop_class attr_var_heap attr_vars attr_env ps_error
			= (TA_Unique, prop_class >> length cons_args, attr_var_heap, attr_vars, attr_env, ps_error)
		determine_attribute_of_cons modules cons_attr cons_args prop_class attr_var_heap attr_vars attr_env ps_error
			# (cumm_attr, prop_attrs, prop_class) = determine_cummulative_attribute cons_args TA_Multi [] prop_class
			  (comb_attr, attr_var_heap, attr_vars, attr_env, ps_error)
			  		= combine_attributes cons_attr cumm_attr prop_attrs attr_var_heap attr_vars attr_env ps_error
			= (comb_attr, prop_class, attr_var_heap, attr_vars, attr_env, ps_error)
			  
		determine_cummulative_attribute [] cumm_attr attr_vars prop_class
			= (cumm_attr, attr_vars, prop_class)
		determine_cummulative_attribute [{at_attribute} : types ] cumm_attr attr_vars prop_class
			| prop_class bitand 1 == 0
				= determine_cummulative_attribute types cumm_attr attr_vars (prop_class >> 1)
				= case at_attribute of
					TA_Unique
						-> (TA_Unique, [], prop_class >> length types)
					TA_Multi
						-> 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
				TA_Unique
					-> (TA_Unique, attr_var_heap, attr_vars, attr_env, attribute_error attr_var ps_error)
				
				TA_Multi
					-> (TA_Var attr_var, attr_var_heap, attr_vars, attr_env, ps_error)
				TA_Var _
					-> (TA_Var attr_var, attr_var_heap, attr_vars, foldSt (new_inequality attr_var) prop_vars attr_env, ps_error)
		where
			new_inequality off_attr_var dem_attr_var [] 
				= [{ ai_demanded = dem_attr_var, ai_offered = off_attr_var }]
			new_inequality off_attr_var dem_attr_var ins=:[ inequal : iequals ]
				 | dem_attr_var.av_info_ptr == inequal.ai_demanded.av_info_ptr && off_attr_var.av_info_ptr == inequal.ai_offered.av_info_ptr
				 	= ins
				 	= [ inequal : new_inequality off_attr_var dem_attr_var iequals ]
	
		combine_attributes _ (TA_Var var) prop_vars attr_var_heap attr_vars attr_env ps_error
			# (new_attr_ptr, attr_var_heap) = newPtr AVI_Empty attr_var_heap
			  new_attr_var = { var & av_info_ptr = new_attr_ptr }
			= (TA_Var new_attr_var, attr_var_heap, [new_attr_var : attr_vars],
					mapAppend (\ai_demanded -> { ai_demanded = ai_demanded, ai_offered = new_attr_var }) prop_vars attr_env, ps_error)
		combine_attributes cons_attr TA_Unique _ attr_var_heap attr_vars attr_env ps_error
			= (TA_Unique, attr_var_heap, attr_vars, attr_env, ps_error)
		combine_attributes cons_attr _ _ attr_var_heap attr_vars attr_env ps_error
			= (cons_attr, attr_var_heap, attr_vars, attr_env, ps_error)

addPropagationAttributesToAType modules type=:{at_type} ps
	# (at_type, ps) = addPropagationAttributesToType modules at_type ps
	= ({ type & at_type = at_type }, NoPropClass, ps)

addPropagationAttributesToType modules (arg_type --> res_type) ps
	# (arg_type, prop_class, ps) = addPropagationAttributesToAType modules arg_type ps
	  (res_type, prop_class, ps) = addPropagationAttributesToAType modules res_type ps
	= (arg_type --> res_type, ps)
addPropagationAttributesToType modules (type_var :@: types) ps
	# (types, ps) = addPropagationAttributesToATypes modules types ps
	= (type_var :@: types, ps)
//AA..
addPropagationAttributesToType modules (TArrow1 arg_type) ps
	# (arg_type, prop_class, ps) = addPropagationAttributesToAType modules arg_type ps
	= (TArrow1 arg_type, ps)
//..AA
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
	add_propagation_attributes_to_atype modules type ps
		# (type, prop_class, ps) = addPropagationAttributesToAType modules type ps
		= (type, ps)

:: Base :== {! AType}

currySymbolType st=:{tst_args,tst_arity,tst_result,tst_attr_env} req_arity ts=:{ts_attr_store}
	| tst_arity == req_arity
		= (st, ts)
	# (tst_args, rest_args, is_unique) = split_args req_arity tst_args 
	| is_unique
		# (type, _, _) = buildCurriedType rest_args tst_result TA_Unique [] 0
		= ({ st & tst_args = tst_args, tst_arity = req_arity, tst_result = type }, ts)
		# (type, tst_attr_env, ts_attr_store) = buildCurriedType rest_args tst_result (TA_TempVar ts_attr_store)
		  		(build_attr_env ts_attr_store tst_args tst_attr_env) (inc ts_attr_store)
		= ({ st & tst_args = tst_args, tst_arity = req_arity, tst_result = type, tst_attr_env = tst_attr_env }, { ts & ts_attr_store = ts_attr_store })
where
	split_args 0 args = ([], args, False)
	split_args n [atype=:{at_attribute} : args]
		# (left, right, is_unique) = split_args (dec n) args
		= ([ atype : left ], right, is_unique || attr_is_unique at_attribute)
	
	attr_is_unique TA_Unique = True
	attr_is_unique _ = False
	
	build_attr_env cum_attr_var [] attr_env
		= attr_env
	build_attr_env cum_attr_var [{at_attribute=(TA_TempVar attr_var)} : args] attr_env
		= build_attr_env cum_attr_var args [{ ac_demanded = attr_var, ac_offered = cum_attr_var } : attr_env]
	build_attr_env cum_attr_var [_ : args] attr_env
		= build_attr_env cum_attr_var args attr_env


emptyIdent =: { id_name = "", id_info = nilPtr }

buildCurriedType [] type cum_attr attr_env attr_store
	= (type, attr_env, attr_store)
buildCurriedType [at=:{at_attribute}:ats] type cum_attr attr_env attr_store
	# (next_cum_attr, attr_env, attr_store) = combine_attributes at_attribute cum_attr attr_env attr_store
	  (res_type, attr_env, attr_store) = buildCurriedType ats type next_cum_attr attr_env attr_store
	= ({at_annotation = AN_None, at_attribute = cum_attr , at_type = at --> res_type }, attr_env, attr_store)
where
	combine_attributes TA_Unique cum_attr attr_env attr_store
		= (TA_Unique, attr_env, attr_store)
	combine_attributes (TA_TempVar attr_var) (TA_TempVar cum_attr_var) attr_env attr_store
		= (TA_TempVar attr_store, [{ ac_demanded = cum_attr_var,ac_offered = attr_store },{ ac_demanded = attr_var,ac_offered = attr_store }:attr_env], inc attr_store)
	combine_attributes (TA_TempVar _) cum_attr attr_env attr_store
		= (cum_attr, attr_env, attr_store)
	combine_attributes _ (TA_TempVar cum_attr_var) attr_env attr_store
		= (TA_TempVar attr_store, [{ ac_demanded = cum_attr_var,ac_offered = attr_store }:attr_env], inc attr_store)
	combine_attributes _ cum_attr attr_env attr_store
		= (cum_attr, attr_env, attr_store)

determineSymbolTypeOfFunction :: CoercionPosition Ident Int SymbolType (Ptr VarInfo) {#CommonDefs} *TypeState -> *(!TempSymbolType,!*TypeState);
determineSymbolTypeOfFunction pos ident act_arity st=:{st_args,st_result,st_attr_vars,st_attr_env} type_ptr common_defs ts=:{ts_var_heap}
	# (type_info, ts_var_heap) = readPtr type_ptr ts_var_heap
	  ts = { ts & ts_var_heap = ts_var_heap }
	= case type_info of
		VI_PropagationType symb_type
	   		# (copy_symb_type, ts) = freshSymbolType (Yes pos) cWithFreshContextVars symb_type common_defs ts 
			-> currySymbolType copy_symb_type act_arity ts
		_	
			# (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 = 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, ts) = freshSymbolType (Yes pos) cWithFreshContextVars st common_defs { ts &
	   										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) }
			-> currySymbolType copy_symb_type act_arity ts

standardFieldSelectorType pos {glob_object={ds_ident,ds_index},glob_module} {ti_common_defs} ts=:{ts_var_store,ts_type_heaps}
	#! {sd_type,sd_exi_vars} = ti_common_defs.[glob_module].com_selector_defs.[ds_index]
	# (th_vars, ts_var_store) = freshExistentialVariables sd_exi_vars (ts_type_heaps.th_vars, ts_var_store)
	= freshSymbolType (Yes pos) cWithFreshContextVars sd_type ti_common_defs { ts & ts_type_heaps = { ts_type_heaps & th_vars = th_vars }, ts_var_store = ts_var_store }
//		 ---> ("standardFieldSelectorType", ds_ident, inst)

standardTupleSelectorType pos {ds_index} arg_nr {ti_common_defs} ts
	#! {cons_type} = ti_common_defs.[cPredefinedModuleIndex].com_cons_defs.[ds_index]
	= freshSymbolType (Yes pos) cWithFreshContextVars { cons_type & st_args = [cons_type.st_result], st_result = cons_type.st_args !! arg_nr } ti_common_defs ts

standardRhsConstructorType pos index mod arity {ti_common_defs} ts
	#! {cons_symb, cons_type, cons_exi_vars } = ti_common_defs.[mod].com_cons_defs.[index]
	# cons_type = { cons_type & st_vars = mapAppend (\{atv_variable} -> atv_variable) cons_exi_vars cons_type.st_vars }
	  (fresh_type, ts) = freshSymbolType (Yes pos) cWithFreshContextVars cons_type ti_common_defs ts
	= currySymbolType fresh_type arity ts
//		 ---> ("standardRhsConstructorType", cons_symb, fresh_type)

standardLhsConstructorType index mod arity {ti_common_defs} ts=:{ts_var_store,ts_type_heaps}
	#! {cons_symb, cons_type, cons_exi_vars } = ti_common_defs.[mod].com_cons_defs.[index]
	# (th_vars, ts_var_store) = freshExistentialVariables cons_exi_vars (ts_type_heaps.th_vars, ts_var_store)
	= freshSymbolType No cWithFreshContextVars cons_type ti_common_defs { ts & ts_type_heaps = { ts_type_heaps & th_vars = th_vars }, ts_var_store = ts_var_store }
//		 ---> ("standardLhsConstructorType", cons_symb, fresh_type)

:: ReferenceMarking :== Bool

cIsRecursive :== True
cIsNotRecursive :== False

storeAttribute (Yes expt_ptr) type_attribute symbol_heap
	= symbol_heap <:=  (expt_ptr, EI_Attribute (toInt type_attribute))
storeAttribute No type_attribute symbol_heap
	= symbol_heap

getSymbolType :: CoercionPosition TypeInput SymbIdent *TypeState -> *(!TempSymbolType,![Special],!*TypeState);
getSymbolType pos ti=:{ti_functions,ti_common_defs,ti_main_dcl_module_n} {symb_kind = SK_Function {glob_module,glob_object}, symb_arity, symb_name} ts
	| glob_module == ti_main_dcl_module_n
		| glob_object>=size ts.ts_fun_env
			= abort symb_name.id_name;
		# (fun_type, ts) = ts!ts_fun_env.[glob_object]
		= case fun_type of
			UncheckedType fun_type
				# (fun_type_copy, ts) = currySymbolType fun_type symb_arity ts
				-> (fun_type_copy, [], ts)
			SpecifiedType fun_type lifted_arg_types _ 
				# (fun_type_copy=:{tst_args,tst_arity}, ts) = freshSymbolType (Yes pos) cWithoutFreshContextVars fun_type ti_common_defs ts
				  (fun_type_copy, ts) = currySymbolType { fun_type_copy & tst_args = lifted_arg_types ++ fun_type_copy.tst_args,
				  										  tst_arity = tst_arity + length lifted_arg_types } symb_arity ts
				-> (fun_type_copy, [], ts)
			CheckedType fun_type
				# (fun_type_copy, ts) = freshSymbolType (Yes pos) cWithFreshContextVars fun_type ti_common_defs ts
				  (fun_type_copy,ts) =</