only allow universal quantifiers at the root of a function argument type,

constructor argument type or field type

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

1 files changed, 106 insertions, 78 deletions

diff --git a/frontend/checktypes.icl b/frontend/checktypes.icl
index a81e44c..e680a55 100644
--- a/frontend/checktypes.icl
+++ b/frontend/checktypes.icl
@@ -24,60 +24,76 @@ from explicitimports import search_qualified_ident,::NameSpaceN,TypeNameSpaceN,C
 	,	cti_lhs_attribute	:: !TypeAttribute
 	}
 
+bindArgAType :: !CurrentTypeInfo !AType !(!*TypeSymbols, !*TypeInfo, !*CheckState)
+			-> (!AType, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
+bindArgAType cti {at_attribute,at_type=TFA vars type} (ts, ti=:{ti_type_heaps}, cs)
+	# (type_vars, (_, ti_type_heaps, cs)) = addTypeVariablesToSymbolTable cRankTwoScope vars [] ti_type_heaps cs
+	  (type, _, (ts, ti, cs)) = bindTypes cti type (ts, {ti & ti_type_heaps = ti_type_heaps}, cs)
+	  cs & cs_symbol_table = removeAttributedTypeVarsFromSymbolTable cRankTwoScope type_vars cs.cs_symbol_table
+	  at_type = TFA type_vars type
+	= bindAttributes TA_Multi cti at_attribute at_type (ts, ti, cs)
+bindArgAType cti {at_attribute,at_type} ts_ti_cs
+	# (at_type, type_attr, ts_ti_cs) = bindTypes cti at_type ts_ti_cs
+	= bindAttributes type_attr cti at_attribute at_type ts_ti_cs
+
 class bindTypes type :: !CurrentTypeInfo !type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
-	-> (!type, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
+					-> (!type, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
 
 instance bindTypes AType
 where
-	bindTypes cti atype=:{at_attribute,at_type} ts_ti_cs
-		# (at_type, type_attr, (ts, ti, cs)) = bindTypes cti at_type ts_ti_cs
-		  cs_error = check_attr_of_type_var at_attribute at_type cs.cs_error
-		  (combined_attribute, cs_error) = check_type_attribute at_attribute type_attr cti.cti_lhs_attribute cs_error
-		= ({ atype & at_attribute = combined_attribute, at_type = at_type }, combined_attribute, (ts, ti, { cs & cs_error = cs_error }))
+	bindTypes cti {at_attribute,at_type} ts_ti_cs
+		# (at_type, type_attr, ts_ti_cs) = bindTypes cti at_type ts_ti_cs
+		= bindAttributes type_attr cti at_attribute at_type ts_ti_cs
+
+bindAttributes :: !TypeAttribute !CurrentTypeInfo !TypeAttribute !Type !(!*TypeSymbols, !*TypeInfo, !*CheckState)
+										   -> (!AType, !TypeAttribute, !(!*TypeSymbols, !*TypeInfo, !*CheckState))
+bindAttributes type_attr cti at_attribute at_type (ts, ti, cs)
+	# cs_error = check_attr_of_type_var at_attribute at_type cs.cs_error
+	  (combined_attribute, cs_error) = check_type_attribute at_attribute type_attr cti.cti_lhs_attribute cs_error
+	= ({ at_attribute = combined_attribute, at_type = at_type }, combined_attribute, (ts, ti, { cs & cs_error = cs_error }))
+where
+	check_type_attribute :: !TypeAttribute !TypeAttribute !TypeAttribute !*ErrorAdmin -> (!TypeAttribute,!*ErrorAdmin)
+	check_type_attribute TA_Anonymous type_attr root_attr error
+		| try_to_combine_attributes type_attr root_attr
+			= (to_root_attr root_attr, error)
+			= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
 	where
-		check_type_attribute :: !TypeAttribute !TypeAttribute !TypeAttribute !*ErrorAdmin -> (!TypeAttribute,!*ErrorAdmin)
-		check_type_attribute TA_Anonymous type_attr root_attr error
-			| try_to_combine_attributes type_attr root_attr
-				= (to_root_attr root_attr, error)
-//				= (root_attr, error)
-				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
-		check_type_attribute TA_Unique type_attr root_attr error
-			| try_to_combine_attributes TA_Unique type_attr || try_to_combine_attributes TA_Unique root_attr
-				= (TA_Unique, error)
-				= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
-		check_type_attribute (TA_Var var) _ _ error
-			= (TA_Multi, checkError var "attribute variable not allowed" error)
-		check_type_attribute (TA_RootVar var) _ _ error
-			= (TA_Multi, checkError var "attribute variable not allowed" error)
-		check_type_attribute _ type_attr root_attr error
-			= (type_attr, error)
-
-		try_to_combine_attributes :: !TypeAttribute !TypeAttribute -> Bool
-		try_to_combine_attributes TA_Multi _
-			= True
-		try_to_combine_attributes (TA_Var attr_var1) (TA_Var attr_var2)
-			= attr_var1.av_ident == attr_var2.av_ident
-		try_to_combine_attributes TA_Unique TA_Unique
-			= True
-		try_to_combine_attributes TA_Unique TA_Multi
-			= True
-		try_to_combine_attributes _ _
-			= False
-
-		check_attr_of_type_var :: !TypeAttribute !Type !*ErrorAdmin -> .ErrorAdmin 
-		check_attr_of_type_var TA_Unique (TV var) error
-			// the case "TA_Var" is catched by check_type_attribute
-			= checkError var "uniqueness attribute not allowed" error
-		check_attr_of_type_var TA_Anonymous (CV tv :@: types) error
-			= checkError tv "attribute variable not allowed" error
-		check_attr_of_type_var attr _ error
-			= error
-
 		to_root_attr (TA_Var var)
 			= TA_RootVar var
 		to_root_attr attr
 			= attr
-					
+	check_type_attribute TA_Unique type_attr root_attr error
+		| try_to_combine_attributes TA_Unique type_attr || try_to_combine_attributes TA_Unique root_attr
+			= (TA_Unique, error)
+			= (TA_Multi, checkError "conflicting attribution of type definition" "" error)
+	check_type_attribute (TA_Var var) _ _ error
+		= (TA_Multi, checkError var "attribute variable not allowed" error)
+	check_type_attribute (TA_RootVar var) _ _ error
+		= (TA_Multi, checkError var "attribute variable not allowed" error)
+	check_type_attribute _ type_attr root_attr error
+		= (type_attr, error)
+
+	try_to_combine_attributes :: !TypeAttribute !TypeAttribute -> Bool
+	try_to_combine_attributes TA_Multi _
+		= True
+	try_to_combine_attributes (TA_Var attr_var1) (TA_Var attr_var2)
+		= attr_var1.av_ident == attr_var2.av_ident
+	try_to_combine_attributes TA_Unique TA_Unique
+		= True
+	try_to_combine_attributes TA_Unique TA_Multi
+		= True
+	try_to_combine_attributes _ _
+		= False
+
+	check_attr_of_type_var :: !TypeAttribute !Type !*ErrorAdmin -> .ErrorAdmin 
+	check_attr_of_type_var TA_Unique (TV var) error
+		// the case "TA_Var" is catched by check_type_attribute
+		= checkError var "uniqueness attribute not allowed" error
+	check_attr_of_type_var TA_Anonymous (CV tv :@: types) error
+		= checkError tv "attribute variable not allowed" error
+	check_attr_of_type_var attr _ error
+		= error
+				
 instance bindTypes TypeVar
 where
 	bindTypes cti tv=:{tv_ident=var_id=:{id_info}} (ts, ti, cs=:{cs_symbol_table})
@@ -239,9 +255,17 @@ where
 					= qualified_type_occurs next_kind ste_index type_module type_index
 			qualified_type_occurs _ _ _ _
 				= False
+	bindTypes cti type=:(TFA vars _) (ts, ti, cs)
+		# cs = universal_quantifier_error vars cs
+		= (type, TA_Multi, (ts, ti, cs))
 	bindTypes cti type ts_ti_cs
 		= (type, TA_Multi, ts_ti_cs)
 
+universal_quantifier_error [{atv_variable={tv_ident}}:_] cs
+	= {cs & cs_error = checkError tv_ident "universally quantified type variable not allowed here" cs.cs_error}
+universal_quantifier_error _ cs
+	= {cs & cs_error = checkError "" "universal quantifier not allowed here" cs.cs_error}
+
 addToAttributeEnviron :: !TypeAttribute !TypeAttribute ![AttrInequality] !*ErrorAdmin -> (![AttrInequality],!*ErrorAdmin)
 addToAttributeEnviron TA_Multi _ attr_env error
 	= (attr_env, error)
@@ -387,7 +411,7 @@ where
 		bind_types_of_cons [type : types] cti free_vars attr_env ts_ti_cs
 			# (types, attr_env, ts_ti_cs)
 					= bind_types_of_cons types cti free_vars attr_env ts_ti_cs
-			  (type, type_attr, (ts, ti, cs)) = bindTypes cti type ts_ti_cs
+			  (type, type_attr, (ts, ti, cs)) = bindArgAType cti type ts_ti_cs
 			  (attr_env, cs_error) = addToAttributeEnviron type_attr cti.cti_lhs_attribute attr_env cs.cs_error
 			= ([type : types], attr_env, (ts, ti , { cs & cs_error = cs_error }))
 
@@ -612,7 +636,6 @@ where
 			= (TA_Multi, error)
 		determine_attribute var_ident dem_attr new_attr error
 			= (new_attr, error)
-
 	check_attribute var_ident dem_attr _ this_attr oti cs
 		= (TA_Multi, oti, cs)
 
@@ -632,8 +655,34 @@ new_demanded_attribute _ TA_Unique
 new_demanded_attribute dem_attr_kind _
 	= DAK_None /* dem_attr_kind */
 
+checkOpenArgAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
+												   -> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
+checkOpenArgAType mod_index scope dem_attr atype=:{at_type = TFA vars type, at_attribute} (ots, oti, cs)
+	# (vars, (oti, cs)) = mapSt add_universal_var vars  (oti, cs) 
+	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr { atype & at_type = type } (ots, oti, cs)
+	  cs = { cs & cs_symbol_table = foldSt remove_universal_var vars cs.cs_symbol_table }
+	= ( { checked_type & at_type = TFA vars checked_type.at_type }, (ots, oti, cs))
+where
+	add_universal_var atv=:{atv_variable = tv=:{tv_ident={id_name,id_info}}, atv_attribute} (oti, cs=:{cs_symbol_table,cs_error})
+		# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
+		| ste_kind == STE_Empty || ste_def_level < cRankTwoScope
+			# (new_attr, oti=:{oti_heaps}, cs) = newAttribute DAK_None id_name atv_attribute oti { cs & cs_symbol_table = cs_symbol_table }
+			  (new_var_ptr, th_vars) = newPtr (TVI_AttrAndRefCount new_attr 1) oti_heaps.th_vars
+			= ({atv & atv_variable = { tv & tv_info_ptr = new_var_ptr}, atv_attribute = new_attr }, 
+					({ oti & oti_heaps = { oti_heaps & th_vars = th_vars }}, { cs & cs_symbol_table =
+							cs.cs_symbol_table <:= (id_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable new_var_ptr,
+									ste_def_level = cRankTwoScope, ste_previous = entry })}))
+			= (atv, (oti, { cs & cs_error = checkError id_name "type variable already undefined" cs_error, cs_symbol_table = cs_symbol_table }))
+
+	remove_universal_var {atv_variable = {tv_ident}, atv_attribute = TA_Var {av_ident}} cs_symbol_table
+		= removeDefinitionFromSymbolTable cGlobalScope av_ident (removeDefinitionFromSymbolTable cRankTwoScope tv_ident cs_symbol_table)
+	remove_universal_var {atv_variable = {tv_ident}} cs_symbol_table
+		= removeDefinitionFromSymbolTable cRankTwoScope tv_ident cs_symbol_table
+checkOpenArgAType mod_index scope dem_attr type ots_oti_cs
+	= checkOpenAType mod_index scope dem_attr type ots_oti_cs
+
 checkOpenAType :: !Index !Int !DemandedAttributeKind !AType !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState)
-	-> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
+												-> (!AType, !(!u:OpenTypeSymbols, !*OpenTypeInfo, !*CheckState))
 checkOpenAType mod_index scope dem_attr type=:{at_type = TV tv, at_attribute} (ots, oti, cs)
 	# (tv, at_attribute, (oti, cs)) = checkTypeVar scope dem_attr tv at_attribute (oti, cs) 
 	= ({ type & at_type = TV tv, at_attribute = at_attribute }, (ots, oti, cs))
@@ -662,7 +711,6 @@ where
 							-> (var, global_vars, var_heap, entry)
 			# (var, global_vars, var_heap, ste_previous) = retrieve_global_variable var ste_previous global_vars var_heap
 			= (var, global_vars, var_heap, { entry & ste_previous = ste_previous })
-//
 checkOpenAType mod_index scope dem_attr_kind type=:{ at_type=TA type_cons=:{type_ident=type_ident=:{id_name,id_info}} types, at_attribute}
 		(ots=:{ots_type_defs,ots_modules}, oti, cs=:{cs_symbol_table,cs_x={x_check_dynamic_types}})
 	# (entry, cs_symbol_table) = readPtr id_info cs_symbol_table
@@ -715,28 +763,6 @@ checkOpenAType mod_index scope dem_attr type=:{at_type = CV tv :@: types, at_att
 	# (cons_var, var_attr, (oti, cs)) = checkTypeVar scope dem_attr tv at_attribute (oti, cs)
 	  (types, (ots, oti, cs)) = mapSt (checkOpenAType mod_index scope DAK_None) types (ots, oti, cs)
 	= ({ type & at_type = CV cons_var :@: types, at_attribute = var_attr }, (ots, oti, cs))
-checkOpenAType mod_index scope dem_attr atype=:{at_type = TFA vars type, at_attribute} (ots, oti, cs)
-	# (vars, (oti, cs)) = mapSt add_universal_var vars  (oti, cs) 
-	  (checked_type, (ots, oti, cs)) = checkOpenAType mod_index cRankTwoScope dem_attr { atype & at_type = type } (ots, oti, cs)
-	  cs = { cs & cs_symbol_table = foldSt remove_universal_var vars cs.cs_symbol_table }
-	= ( { checked_type & at_type = TFA vars checked_type.at_type }, (ots, oti, cs))
-where
-	add_universal_var atv=:{atv_variable = tv=:{tv_ident={id_name,id_info}}, atv_attribute} (oti, cs=:{cs_symbol_table,cs_error})
-		# (entry=:{ste_kind,ste_def_level},cs_symbol_table) = readPtr id_info cs_symbol_table
-		| ste_kind == STE_Empty || ste_def_level < cRankTwoScope
-			# (new_attr, oti=:{oti_heaps}, cs) = newAttribute DAK_None id_name atv_attribute oti { cs & cs_symbol_table = cs_symbol_table }
-			  (new_var_ptr, th_vars) = newPtr (TVI_AttrAndRefCount new_attr 1) oti_heaps.th_vars
-			= ({atv & atv_variable = { tv & tv_info_ptr = new_var_ptr}, atv_attribute = new_attr }, 
-					({ oti & oti_heaps = { oti_heaps & th_vars = th_vars }}, { cs & cs_symbol_table =
-							cs.cs_symbol_table <:= (id_info, {ste_index = NoIndex, ste_kind = STE_TypeVariable new_var_ptr,
-									ste_def_level = cRankTwoScope, ste_previous = entry })}))
-			= (atv, (oti, { cs & cs_error = checkError id_name "type variable already undefined" cs_error, cs_symbol_table = cs_symbol_table }))
-
-	remove_universal_var {atv_variable = {tv_ident}, atv_attribute = TA_Var {av_ident}} cs_symbol_table
-		= removeDefinitionFromSymbolTable cGlobalScope av_ident (removeDefinitionFromSymbolTable cRankTwoScope tv_ident cs_symbol_table)
-	remove_universal_var {atv_variable = {tv_ident}} cs_symbol_table
-		= removeDefinitionFromSymbolTable cRankTwoScope tv_ident cs_symbol_table
-
 checkOpenAType mod_index scope dem_attr_kind type=:{ at_type=TQualifiedIdent module_id type_name types, at_attribute}
 		(ots=:{ots_type_defs,ots_modules}, oti, cs=:{cs_symbol_table,cs_x={x_check_dynamic_types}})
 	# (found,{decl_kind,decl_ident=type_ident,decl_index=type_index},cs) = search_qualified_ident module_id type_name TypeNameSpaceN cs
@@ -758,6 +784,9 @@ checkOpenAType mod_index scope dem_attr_kind type=:{ at_type=TQualifiedIdent mod
 					-> (type, (ots, oti, {cs & cs_error = checkError type_ident "used with wrong arity" cs.cs_error}))
 			_
 				-> (type, (ots, oti, {cs & cs_error = checkError (module_id.id_name+++"@"+++type_name) "not imported" cs.cs_error}))
+checkOpenAType mod_index scope dem_attr atype=:{at_type = TFA vars type} (ots, oti, cs)
+	# cs = universal_quantifier_error vars cs
+	= (atype, (ots, oti, cs))
 checkOpenAType mod_index scope dem_attr type=:{at_attribute} (ots, oti, cs)
 	# (new_attr, oti, cs) = newAttribute dem_attr "." at_attribute oti cs
 	= ({ type & at_attribute = new_attr}, (ots, oti, cs))
@@ -768,9 +797,9 @@ checkOpenTypes mod_index scope dem_attr types cot_state
 checkOpenType mod_index scope dem_attr type cot_state
 	# ({at_type}, cot_state) = checkOpenAType mod_index scope dem_attr { at_type = type, at_attribute = TA_Multi } cot_state
 	= (at_type, cot_state)
-	
-checkOpenATypes mod_index scope types cot_state
-	= mapSt (checkOpenAType mod_index scope DAK_None) types cot_state
+
+checkOpenArgATypes mod_index scope types cot_state
+	= mapSt (checkOpenArgAType mod_index scope DAK_None) types cot_state
 
 checkInstanceType :: !Index !GlobalIndex !ClassIdent !InstanceType !Specials !u:{# CheckedTypeDef} !v:{# ClassDef} !u:{# DclModule} !*TypeHeaps !*CheckState
 												 -> (!InstanceType,!Specials,!u:{# CheckedTypeDef},!v:{# ClassDef},!u:{# DclModule},!*TypeHeaps,!*CheckState)
@@ -860,7 +889,7 @@ checkSymbolType :: !Bool !Index !SymbolType !FunSpecials !u:{#CheckedTypeDef} !v
 checkSymbolType is_function mod_index st=:{st_args,st_result,st_context,st_attr_env} specials type_defs class_defs modules heaps cs
 	# ots = { ots_type_defs = type_defs, ots_modules = modules }
 	  oti = { oti_heaps = heaps, oti_all_vars = [], oti_all_attrs = [], oti_global_vars= [] }
-	  (st_args, cot_state) = checkOpenATypes mod_index cGlobalScope st_args (ots, oti, cs)
+	  (st_args, cot_state) = checkOpenArgATypes mod_index cGlobalScope st_args (ots, oti, cs)
 	  (st_result, (ots, oti=:{oti_all_vars = st_vars,oti_all_attrs = st_attr_vars,oti_global_vars}, cs))
 	  	= checkOpenAType mod_index cGlobalScope DAK_None st_result cot_state	  
 	  oti = { oti &  oti_all_vars = [], oti_all_attrs = [] }
@@ -897,10 +926,9 @@ where
 		 	= checkTypeContexts st_context mod_index class_defs ots oti cs
 			= check_member_contexts st_context mod_index class_defs ots oti cs
 
-// AA.. generic members do not have a context at the moment of checking
+	// AA generic members do not have a context at the moment of checking
 	check_member_contexts [] mod_index class_defs ots oti cs
 		= checkTypeContexts [] mod_index class_defs ots oti cs
-// ..AA
 	check_member_contexts [tc : tcs] mod_index class_defs ots oti cs
 		# (tc, (class_defs, ots, oti, cs)) = checkTypeContext mod_index tc  (class_defs, ots, oti, cs)
 		  cs_symbol_table = removeVariablesFromSymbolTable cGlobalScope [ tv \\ (TV tv) <- tc.tc_types] cs.cs_symbol_table
@@ -1074,7 +1102,7 @@ where
 				| entry.ste_kind == STE_Empty
 					= symbol_table
 					= symbol_table <:= (id_info, entry.ste_previous)
-				 
+
 checkDynamicTypes mod_index dyn_type_ptrs (Yes {st_vars}) type_defs modules type_heaps expr_heap cs=:{cs_symbol_table}
 	# (th_vars, cs_symbol_table) = foldSt add_type_variable_to_symbol_table st_vars (type_heaps.th_vars, cs_symbol_table)
 	  (type_defs, modules, heaps, expr_heap, cs) = checkDynamics mod_index (inc cModuleScope) dyn_type_ptrs type_defs modules