removed boolean result from substituteType and substitute: they

could only fail in case of a kind error which is already detected
elsewhere

frontend/analtypes.icl

@@ -117,11 +117,8 @@ where
 			# (used_td=:{td_rhs}, type_defs) = type_defs![glob_module, glob_object]
 			= case td_rhs of
 				SynType {at_type}
-					# (ok, subst_rhs, type_heaps) = substituteType used_td.td_attribute attribute used_td.td_args types at_type type_heaps
-					| ok
-						-> (Yes {type & at_type = subst_rhs }, type_defs, type_heaps, error)
-					  	# error = popErrorAdmin (typeSynonymError used_td.td_ident "kind conflict in argument of type synonym" (pushErrorAdmin pos error))
-						-> (No, type_defs, type_heaps, error)
+					# ( subst_rhs, type_heaps) = substituteType used_td.td_attribute attribute used_td.td_args types at_type type_heaps
+					-> (Yes {type & at_type = subst_rhs }, type_defs, type_heaps, error)
 				_
 					-> (No, type_defs, type_heaps, error)
 

frontend/check.icl

@@ -614,22 +614,16 @@ instantiateTypes old_type_vars old_attr_vars types type_contexts attr_env {ss_en
 	  (new_attr_vars, th_attrs) = foldSt build_attr_var_subst ss_attrs ([], th_attrs)
 
 	  type_heaps = foldSt build_type_subst ss_environ { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
-	  (ok1, new_ss_context, type_heaps) = substitute ss_context type_heaps
+	  (new_ss_context, type_heaps) = substitute ss_context type_heaps
 
 	  (inst_vars, th_vars)			= foldSt determine_free_var old_type_vars (new_type_vars, type_heaps.th_vars) 
 	  (inst_attr_vars, th_attrs)	= foldSt build_attr_var_subst old_attr_vars (new_attr_vars, type_heaps.th_attrs)
 
 	  (inst_types, (ok2, type_heaps))	= mapSt substitue_arg_type types (True, { type_heaps & th_vars = th_vars, th_attrs = th_attrs })
 //	  (ok2, inst_types, type_heaps)		= substitute types { type_heaps & th_vars = th_vars, th_attrs = th_attrs }
-	  (ok3, inst_contexts, type_heaps)	= substitute type_contexts type_heaps
-	  (ok4, inst_attr_env, type_heaps)	= substitute attr_env type_heaps
+	  (inst_contexts, type_heaps)	= substitute type_contexts type_heaps
+	  (inst_attr_env, type_heaps)	= substitute attr_env type_heaps
 	  (special_subst_list, th_vars) 	= mapSt adjust_special_subst special_subst_list type_heaps.th_vars
-	  error = case ok1 && ok2 && ok3 && ok4 of
-	  				True
-	  					-> error
-	  				False
-	  					-> checkError "instance type incompatible with class type" "" error
-
 	= (inst_vars, inst_attr_vars, inst_types, new_ss_context ++ inst_contexts, inst_attr_env, special_subst_list, { type_heaps & th_vars = th_vars }, error)
 where
 	clear_vars type_vars type_var_heap = foldSt (\tv -> writePtr tv.tv_info_ptr TVI_Empty) type_vars type_var_heap
@@ -643,7 +637,7 @@ where
 				-> (free_vars, type_var_heap)
 
 	build_type_subst {bind_src,bind_dst} type_heaps
-		# (_, bind_src, type_heaps) = substitute bind_src type_heaps
+		# (bind_src, type_heaps) = substitute bind_src type_heaps
 // RWS ...
 /*
 	FIXME: this is a patch for the following incorrect function type (in a dcl module)
@@ -664,11 +658,11 @@ where
 
 	substitue_arg_type at=:{at_type = TFA type_vars type} (was_ok, type_heaps)
 		# (fresh_type_vars, type_heaps) = foldSt build_avar_subst type_vars ([], type_heaps)
-		  (ok, new_at, type_heaps) = substitute {at & at_type = type} type_heaps
-		= ({ new_at & at_type = TFA fresh_type_vars new_at.at_type}, (was_ok && ok, type_heaps))
+		  (new_at, type_heaps) = substitute {at & at_type = type} type_heaps
+		= ({ new_at & at_type = TFA fresh_type_vars new_at.at_type}, (was_ok, type_heaps))
 	substitue_arg_type type (was_ok, type_heaps)
-		# (ok, type, type_heaps) = substitute type type_heaps
-		= (type, (was_ok && ok, type_heaps))
+		# (type, type_heaps) = substitute type type_heaps
+		= (type, (was_ok, type_heaps))
 		
 	build_var_subst var (free_vars, type_var_heap)
 		# (new_info_ptr, type_var_heap) = newPtr TVI_Empty type_var_heap

frontend/overloading.icl

@@ -388,7 +388,7 @@ where
 	where
 		fresh_context :: !TypeContext !*(.a,*TypeHeaps) -> (TypeContext,(.a,*TypeHeaps))
 		fresh_context tc=:{tc_types} (var_heap, type_heaps)
-			# (_, tc_types, type_heaps) = substitute tc_types type_heaps
+			# (tc_types, type_heaps) = substitute tc_types type_heaps
 //			  (tc_var, var_heap) = newPtr VI_Empty var_heap
 //			= ({ tc & tc_types = tc_types, tc_var = tc_var }, (var_heap, type_heaps))
 			= ({ tc & tc_types = tc_types }, (var_heap, type_heaps))
@@ -496,7 +496,7 @@ where
 					   is_predefined_symbol glob_module glob_object PD_UnboxedArrayType predef_symbols
 				-> (unboxable, No, (predef_symbols, type_heaps))
 			SynType {at_type}
-				# (_, expanded_type, type_heaps) = substituteType td_attribute TA_Multi td_args type_args at_type type_heaps
+				# (expanded_type, type_heaps) = substituteType td_attribute TA_Multi td_args type_args at_type type_heaps
 				-> try_to_unbox expanded_type defs (predef_symbols, type_heaps)
 			_
 				-> (False, No, (predef_symbols, type_heaps))				
@@ -593,7 +593,7 @@ tryToExpandTypeSyn defs type cons_id=:{type_ident,type_index={glob_object,glob_m
 	# {td_ident,td_rhs,td_args,td_attribute} = defs.[glob_module].com_type_defs.[glob_object]
 	= case td_rhs of
 		SynType {at_type}
-			# (_, expanded_type, type_heaps) = substituteType td_attribute TA_Multi td_args type_args at_type type_heaps
+			# (expanded_type, type_heaps) = substituteType td_attribute TA_Multi td_args type_args at_type type_heaps
 			-> (True, expanded_type, type_heaps) 
 		_
 			-> (False, type, type_heaps)
@@ -835,7 +835,7 @@ where
 			= type_var_heap <:= (tv_info_ptr, TVI_Type type)
 		  
 		subst_context_and_generate_super_classes class_context (super_classes, type_heaps)
-			# (_, super_class, type_heaps) = substitute class_context type_heaps
+			# (super_class, type_heaps) = substitute class_context type_heaps
 			| containsContext super_class super_classes
 				= (super_classes, type_heaps)
 				= generate_super_classes super_class ([super_class : super_classes], type_heaps) 
@@ -1057,7 +1057,7 @@ where
 			# {tc_class=TCClass {glob_object={ds_index},glob_module}} = tc2
 			  {class_args,class_members,class_context,class_dictionary} = defs.[glob_module].com_class_defs.[ds_index]
 			  th_vars = foldr2 (\{tv_info_ptr} type -> writePtr tv_info_ptr (TVI_Type type)) th_vars class_args tc2.tc_types
-			  (_, super_instances, type_heaps) = substitute class_context { type_heaps & th_vars = th_vars } 
+			  (super_instances, type_heaps) = substitute class_context { type_heaps & th_vars = th_vars } 
 			= find_super_instance tc1 super_instances (size class_members) address glob_module class_dictionary.ds_index defs type_heaps
 	where
 		find_super_instance :: !TypeContext ![TypeContext] !Index ![(Int, Global DefinedSymbol)] !Index !Index !{#CommonDefs} !*TypeHeaps

frontend/trans.icl

@@ -978,8 +978,8 @@ where
 		  (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
 		  ti_type_heaps							= { ti_type_heaps & th_vars = th_vars }
-		  (_, fresh_arg_types, ti_type_heaps)	= substitute arg_types ti_type_heaps
-		  (_, fresh_result_type, ti_type_heaps)	= substitute ct_result_type ti_type_heaps
+		  (fresh_arg_types, ti_type_heaps)	= substitute arg_types ti_type_heaps
+		  (fresh_result_type, ti_type_heaps)	= substitute ct_result_type ti_type_heaps
 		  fun_type =
 		  			{ st_vars					= fresh_type_vars
 		  			, st_args					= fresh_arg_types
@@ -1349,7 +1349,7 @@ generateFunction app_symb fd=:{fun_body = TransformedBody {tb_args,tb_rhs},fun_i
 	  ti_type_heaps
 	  		= { ti_type_heaps & th_attrs = th_attrs, th_vars = th_vars }
 //	| False-!->("before substitute", st_args, "->", st_result)		= undef
-	# (_, (st_args,st_result), ti_type_heaps)
+	# ((st_args,st_result), ti_type_heaps)
 	  		= substitute (st_args,st_result) ti_type_heaps
 //	| False-!->("after substitute", st_args, "->", st_result)		= undef
 // determine args...
@@ -1686,9 +1686,9 @@ where
 				= 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)
+		  ([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)
+		  (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)
@@ -1907,7 +1907,7 @@ determine_arg (PR_Class class_app free_vars_and_types class_type) _ {fv_info_ptr
 			= das_arg_types![prod_index]
 	# {ats_types=[arg_type:_]}
 	  		= ws_arg_type
-	  (_, int_class_type, das_type_heaps)
+	  (int_class_type, das_type_heaps)
 	  		= substitute class_type das_type_heaps
 	  class_atype
 	  		= { empty_atype & at_type = int_class_type }
@@ -1941,7 +1941,7 @@ determine_arg (PR_Class class_app free_vars_and_types class_type) _ {fv_info_ptr
 	# (free_vars_and_types,das_type_heaps) = mapSt subFVT free_vars_and_types das_type_heaps
 		with
 			subFVT (fv,ty) th
-				# (_,ty`,th`)		= substitute ty th
+				# (ty`,th`)		= substitute ty th
 				= ((fv,ty`),th`)
 
 	# ws_ats_types = [ { empty_atype & at_type = at_type } \\ (_, at_type) <- free_vars_and_types]
@@ -1977,7 +1977,7 @@ determine_arg producer (Yes {st_args, st_args_strictness, st_result, st_attr_var
 	  (das_next_attr_nr, th_attrs)
 	  		= foldSt bind_to_temp_attr_var st_attr_vars (das_next_attr_nr, th_attrs)
 	  		// prepare for substitute calls
-	  (_, (st_args, st_result), das_type_heaps)
+	  ((st_args, st_result), das_type_heaps)
 	  		= substitute (st_args, st_result) { das_type_heaps & th_vars = th_vars, th_attrs = th_attrs }
 	  nr_of_applied_args
 			= symbol_arity
@@ -3924,7 +3924,7 @@ where
 	bind_and_substitute_before_expand types td_args td_attribute rhs_type rem_annots attribute ets_type_heaps
 		# ets_type_heaps = bind_attr td_attribute attribute ets_type_heaps
 		  ets_type_heaps = (fold2St bind_var_and_attr td_args types ets_type_heaps)
-		  (_, type, ets_type_heaps) = substitute_rhs rem_annots rhs_type.at_type ets_type_heaps
+		  (type, ets_type_heaps) = substitute_rhs rem_annots rhs_type.at_type ets_type_heaps
 		= (type, ets_type_heaps)
 		where
 			bind_var_and_attr {	atv_attribute = TA_Var {av_info_ptr},  atv_variable = {tv_info_ptr} } {at_attribute,at_type} type_heaps=:{th_vars,th_attrs}

frontend/transform.icl

@@ -353,7 +353,7 @@ unfoldVariable var=:{var_ident,var_info_ptr} ui us
 	substitute_class_types class_types No
 		= (class_types, No)
 	substitute_class_types class_types (Yes type_heaps)
-		# (_,new_class_types, type_heaps) = substitute class_types type_heaps
+		# (new_class_types, type_heaps) = substitute class_types type_heaps
 		= (new_class_types, Yes type_heaps)
 
 readVarInfo var_info_ptr us
@@ -549,7 +549,7 @@ where
 					-> unfold_function_app app ui us
 
 		substitute_EI_DictionaryType (EI_DictionaryType class_type) (Yes type_heaps)
-			# (_,new_class_type, type_heaps) = substitute class_type type_heaps
+			# (new_class_type, type_heaps) = substitute class_type type_heaps
 			= (EI_DictionaryType new_class_type, Yes type_heaps)
 		substitute_EI_DictionaryType x opt_type_heaps
 			= (x, opt_type_heaps)
@@ -662,10 +662,10 @@ substitute_let_or_case_type	(EI_Extended extensions expr_info) yes_type_heaps
 	# (new_expr_info, yes_type_heaps) = substitute_let_or_case_type expr_info yes_type_heaps
 	= (EI_Extended extensions new_expr_info, yes_type_heaps)
 substitute_let_or_case_type	(EI_CaseType case_type) (Yes type_heaps)
-	# (_,new_case_type, type_heaps) = substitute case_type type_heaps
+	# (new_case_type, type_heaps) = substitute case_type type_heaps
 	= (EI_CaseType new_case_type, Yes type_heaps)
 substitute_let_or_case_type	(EI_LetType let_type) (Yes type_heaps)
-	# (_,new_let_type, type_heaps) = substitute let_type type_heaps
+	# (new_let_type, type_heaps) = substitute let_type type_heaps
 	= (EI_LetType new_let_type, Yes type_heaps)
 
 instance unfold CasePatterns

frontend/type.icl

@@ -371,7 +371,7 @@ tryToExpand type=:(TA {type_index={glob_object,glob_module}} type_args) type_att
 	#! 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
+			# (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)
@@ -379,7 +379,7 @@ tryToExpand type=:(TAS {type_index={glob_object,glob_module}} type_args _) type_
 	#! 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
+			# (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)

frontend/typesupport.dcl

@@ -71,12 +71,12 @@ beautifulizeAttributes :: !SymbolType !*AttrVarHeap -> (!SymbolType, !.AttrVarHe
 
 updateExpressionTypes :: !SymbolType !SymbolType ![ExprInfoPtr] !*TypeHeaps !*ExpressionHeap -> (!*TypeHeaps, !*ExpressionHeap)
 
-class substitute a :: !a !*TypeHeaps -> (!Bool, !a, !*TypeHeaps)
+class substitute a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
 
 instance substitute AType, Type, TypeContext, AttrInequality, CaseType, [a] | substitute a,
 			(a,b) | substitute a & substitute b
 
-substituteType :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !Type !*TypeHeaps -> (!Bool, !Type, !*TypeHeaps)
+substituteType :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !Type !*TypeHeaps -> (!Type, !*TypeHeaps)
 
 bindTypeVarsAndAttributes :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !*TypeHeaps -> *TypeHeaps;
 clearBindingsOfTypeVarsAndAttributes :: !TypeAttribute ![ATypeVar] !*TypeHeaps -> *TypeHeaps;

frontend/typesupport.icl

@@ -24,29 +24,33 @@ import genericsupport
 				 | UncheckedType !TempSymbolType | ExpandedType !SymbolType !TempSymbolType !TempSymbolType  | EmptyFunctionType
 
 
-simplifyTypeApplication :: !Type ![AType] -> (!Bool, !Type)
-simplifyTypeApplication (TA type_cons=:{type_arity} cons_args) type_args
+simplifyTypeApplication :: !Type ![AType] -> Type
+simplifyTypeApplication type type_args
+	# (ok, type)
+		=	simplifyAndCheckTypeApplication type type_args
+	| not ok
+		=	abort "typesupport.simplifyTypeApplication: unexpected error"
+	=	type
+
+simplifyAndCheckTypeApplication :: !Type ![AType] -> (!Bool, !Type)
+simplifyAndCheckTypeApplication (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 (TAS type_cons=:{type_arity} cons_args strictness) type_args
+simplifyAndCheckTypeApplication (TAS type_cons=:{type_arity} cons_args strictness) type_args
 	= (True, TAS { type_cons & type_arity = type_arity + length type_args } (cons_args ++ type_args) strictness)
-simplifyTypeApplication (CV tv :@: type_args1) type_args2
+simplifyAndCheckTypeApplication (CV tv :@: type_args1) type_args2
 	= (True, CV tv :@: (type_args1 ++ type_args2))
-simplifyTypeApplication TArrow [type1, type2] 
+simplifyAndCheckTypeApplication TArrow [type1, type2] 
 	= (True, type1 --> type2)
-simplifyTypeApplication TArrow [type] 
+simplifyAndCheckTypeApplication TArrow [type] 
 	= (True, TArrow1 type)
-simplifyTypeApplication (TArrow1 type1) [type2] 
+simplifyAndCheckTypeApplication (TArrow1 type1) [type2] 
 	= (True, type1 --> type2)
-simplifyTypeApplication (TV tv) type_args
+simplifyAndCheckTypeApplication (TV tv) type_args
 	= (True, CV tv :@: type_args)
-simplifyTypeApplication (TB _) _
-	= (False, TE)
-simplifyTypeApplication (TArrow1 _) _ 
-	= (False, TE)
-simplifyTypeApplication (_ --> _ ) _ 
-	= (False, TE)
-	
-	
+simplifyAndCheckTypeApplication (TempV i) type_args
+	= (True, TempCV i :@: type_args)
+simplifyAndCheckTypeApplication type type_args
+	= (False, type)
 
 ::	AttributeEnv	:== {! TypeAttribute }
 ::	VarEnv 			:== {! Type }
@@ -163,7 +167,7 @@ where
 		# (type, cus) = cus!cus_var_env.[tempvar]
 		# (type, cus) = cleanUpVariable cui.cui_top_level type tempvar cus
 		  (types, cus) = clean_up cui types cus
-		= (snd (simplifyTypeApplication type types), cus)
+		= (simplifyTypeApplication type types, cus)
 	clean_up cui (TempQCV tempvar :@: types) cus
 		# (type, cus) = cus!cus_var_env.[tempvar]
 		# (TV tv, cus) = cleanUpVariable cui.cui_top_level type tempvar cus
@@ -257,7 +261,7 @@ where
 		| checkCleanUpResult cur1 cUndefinedVar
 			= (cur1, TempCV tv_number :@: types, env)
 			# (cur2, types, env) = cleanUpClosed types env
-            = (combineCleanUpResults cur1 cur2, snd (simplifyTypeApplication type types), env)
+            = (combineCleanUpResults cur1 cur2, simplifyTypeApplication type types, env)
 	cleanUpClosed t env
 		= (cClosed, t, env)
 
@@ -583,13 +587,13 @@ where
 		# (info, expr_heap) = readPtr expr_ptr expr_heap
 		= case info of
 			EI_CaseType case_type
-				# (_, case_type, type_heaps) = substitute case_type type_heaps
+				# (case_type, type_heaps) = substitute case_type type_heaps
 				-> (type_heaps, expr_heap <:= (expr_ptr, EI_CaseType case_type))
 			EI_LetType let_type
-				# (_, let_type, type_heaps) = substitute let_type type_heaps
+				# (let_type, type_heaps) = substitute let_type type_heaps
 				-> (type_heaps, expr_heap <:= (expr_ptr, EI_LetType let_type))
 			EI_DictionaryType dict_type
-				# (_, dict_type, type_heaps) = substitute dict_type type_heaps
+				# (dict_type, type_heaps) = substitute dict_type type_heaps
 				-> (type_heaps, expr_heap <:= (expr_ptr, EI_DictionaryType dict_type))
 
 
@@ -637,12 +641,11 @@ instance bindInstances AType
 	bindInstances {at_type=t1} {at_type=t2} type_var_heap
 			= bindInstances t1 t2 type_var_heap
 
-substituteType :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !Type !*TypeHeaps -> (!Bool, !Type, !*TypeHeaps)
+substituteType :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !Type !*TypeHeaps -> (!Type, !*TypeHeaps)
 substituteType form_root_attribute act_root_attribute form_type_args act_type_args orig_type type_heaps
 	# type_heaps = bindTypeVarsAndAttributes form_root_attribute act_root_attribute form_type_args act_type_args type_heaps
-	  (ok, expanded_type, type_heaps) = substitute orig_type type_heaps
-	= (ok, expanded_type, clearBindingsOfTypeVarsAndAttributes form_root_attribute form_type_args type_heaps)
-
+	  (expanded_type, type_heaps) = substitute orig_type type_heaps
+	= (expanded_type, clearBindingsOfTypeVarsAndAttributes form_root_attribute form_type_args type_heaps)
 
 bindTypeVarsAndAttributes :: !TypeAttribute !TypeAttribute ![ATypeVar] ![AType] !*TypeHeaps -> *TypeHeaps
 bindTypeVarsAndAttributes form_root_attribute act_root_attribute form_type_args act_type_args type_heaps
@@ -671,13 +674,13 @@ where
 	clear_attribute _ th_attrs
 		= th_attrs
 
-class substitute a :: !a !*TypeHeaps -> (!Bool, !a, !*TypeHeaps)
+class substitute a :: !a !*TypeHeaps -> (!a, !*TypeHeaps)
 
 instance substitute AType
 where
 	substitute atype=:{at_attribute,at_type} heaps
-		# (ok, (at_attribute,at_type), heaps)  = substitute (at_attribute,at_type) heaps
-		= (ok, { atype & at_attribute = at_attribute, at_type = at_type }, heaps)
+		# ((at_attribute,at_type), heaps)  = substitute (at_attribute,at_type) heaps
+		= ({ atype & at_attribute = at_attribute, at_type = at_type }, heaps)
 
 instance substitute TypeAttribute
 where
@@ -685,35 +688,35 @@ where
 		#! av_info = sreadPtr av_info_ptr th_attrs
 		= case av_info of
 			AVI_Attr attr
-				-> (True, attr, heaps)
+				-> (attr, heaps)
 			_
-				-> (True, TA_Multi, heaps)
+				-> (TA_Multi, heaps)
 	substitute TA_None heaps
-		= (True, TA_Multi, heaps)
+		= (TA_Multi, heaps)
 	substitute attr heaps
-		= (True, attr, heaps)
+		= (attr, heaps)
 
 instance substitute (a,b) | substitute a & substitute b
 where
 	substitute (x,y) heaps
-		# (ok_x, x, heaps) = substitute x heaps
-		  (ok_y, y, heaps) = substitute y heaps
-		= (ok_x && ok_y, (x,y), heaps)
+		# (x, heaps) = substitute x heaps
+		  (y, heaps) = substitute y heaps
+		= ((x,y), heaps)
 	
 instance substitute [a] | substitute a
 where
 	substitute [] heaps
-		= (True, [], heaps)
+		= ( [], heaps)
 	substitute [t:ts] heaps
-		# (ok_t, t, heaps) = substitute t heaps
-		  (ok_ts, ts, heaps) = substitute ts heaps
-		= (ok_t && ok_ts, [t:ts], heaps)
+		# (t, heaps) = substitute t heaps
+		  ( ts, heaps) = substitute ts heaps
+		= ([t:ts], heaps)
 
 instance substitute TypeContext
 where
 	substitute tc=:{tc_types} heaps
-		# (ok, tc_types, heaps) = substitute tc_types heaps
-		= (ok, { tc & tc_types = tc_types }, heaps)
+		# (tc_types, heaps) = substitute tc_types heaps
+		= ({ tc & tc_types = tc_types }, heaps)
 
 instance substitute Type
 where
@@ -722,37 +725,36 @@ where
 		  heaps = { heaps & th_vars = th_vars }
 		= case tv_info of
 			TVI_Type type
-				-> (True, type, heaps)
+				-> (type, heaps)
 			_
-				-> (True, tv, heaps)
+				-> (tv, heaps)
 	substitute (arg_type --> res_type) heaps
-		# (ok, (arg_type, res_type), heaps) = substitute (arg_type, res_type) heaps
-		= (ok, arg_type --> res_type, heaps)
+		# ((arg_type, res_type), heaps) = substitute (arg_type, res_type) heaps
+		= (arg_type --> res_type, heaps)
 	substitute (TArrow1 arg_type) heaps
-		# (ok, arg_type, heaps) = substitute arg_type heaps
-		= (ok, TArrow1 arg_type, heaps)
+		# (arg_type, heaps) = substitute arg_type heaps
+		= (TArrow1 arg_type, heaps)
 	substitute (TA cons_id cons_args) heaps
-		# (ok, cons_args, heaps) = substitute cons_args heaps
-		= (ok, TA cons_id cons_args,  heaps)
+		# (cons_args, heaps) = substitute cons_args heaps
+		= (TA cons_id cons_args,  heaps)
 	substitute (TAS cons_id cons_args strictness) heaps
-		# (ok, cons_args, heaps) = substitute cons_args heaps
-		= (ok, TAS cons_id cons_args strictness,  heaps)
+		# (cons_args, heaps) = substitute cons_args heaps
+		= (TAS cons_id cons_args strictness,  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 }
-		  (ok_types, types, heaps) = substitute types heaps
+		  (types, heaps) = substitute types heaps
 		= case tv_info of
 			TVI_Type type
-				-> case type of
-					TempV i
-						-> (ok_types, TempCV i :@: types, heaps)
-					_
-						#  (ok_type, simplified_type) = simplifyTypeApplication type types
-						-> (ok_type && ok_types, simplified_type, heaps)
-			_
-				-> 	(ok_types, CV type_var :@: types, heaps)
+				#  (ok, simplified_type) = simplifyAndCheckTypeApplication type types
+				| ok
+					-> (simplified_type, heaps)
+				// otherwise
+					// this will lead to a kind check error later on
+					-> 	(CV type_var :@: types, heaps)
+			-> 	(CV type_var :@: types, heaps)
 	substitute type heaps
-		= (True, type, heaps)
+		= (type, heaps)
 
 instance substitute AttributeVar
 where
@@ -760,23 +762,23 @@ where
 		#! av_info = sreadPtr av_info_ptr th_attrs
 		= case av_info of
 			AVI_Attr (TA_Var attr_var)
-				-> (True, attr_var, heaps)
+				-> (attr_var, heaps)
 			_
-				-> (True, av, heaps)
+				-> (av, heaps)
 
 instance substitute AttrInequality
 where
 	substitute {ai_demanded,ai_offered} heaps
-		# (ok, (ai_demanded, ai_offered), heaps) = substitute (ai_demanded, ai_offered) heaps
-		= (ok, {ai_demanded = ai_demanded, ai_offered = ai_offered}, heaps)
+		# ((ai_demanded, ai_offered), heaps) = substitute (ai_demanded, ai_offered) heaps
+		= ({ai_demanded = ai_demanded, ai_offered = ai_offered}, heaps)
 
 instance substitute CaseType
 where
 	substitute {ct_pattern_type, ct_result_type, ct_cons_types} heaps 
-		# (ok1, ct_pattern_type, heaps) = substitute ct_pattern_type heaps
-		  (ok2, ct_result_type, heaps) = substitute ct_result_type heaps
-		  (ok3, ct_cons_types, heaps) = substitute ct_cons_types heaps
-		= (ok1 && ok2 && ok3, {ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, 
+		# (ct_pattern_type, heaps) = substitute ct_pattern_type heaps
+		  (ct_result_type, heaps) = substitute ct_result_type heaps
+		  (ct_cons_types, heaps) = substitute ct_cons_types heaps
+		= ({ct_pattern_type = ct_pattern_type, ct_result_type = ct_result_type, 
 								ct_cons_types = ct_cons_types}, heaps)
 
 class removeAnnotations a :: !a  -> (!Bool, !a)