[m-dev.] diff: fix bug with existential types

[Fergus Henderson]

Estimated hours taken: 4

Fix a bug with existential types.  The compiler was reporting a
spurious mode error, due to the arity of the cons_id for a
typeclass_info structure not matching the actual number of arguments.
This caused a failure in merge_insts, because two typeclass_info
structures constructed in different branches of a disjunction had the
same cons_id but different arities.
There was special code in polymorphism.m to handle this case,
but now that mode analysis is run after polymorphism, we need to
special case it in mode analysis instead.

compiler/modecheck_unify.m:
	Check for unifications with functor `private_builtin:typeclass_info'
	or `private_builtin:type_info'.  For such unification,
	use the actual number of arguments for the cons_id arity in the inst,
	rather than using the original cons_id arity.

tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/existential_data_types_regr_test.m:
tests/hard_coded/typeclasses/existential_data_types_regr_test.exp:
	Regression test.

Workspace: /home/mercury0/fjh/mercury
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.40
diff -u -r1.40 modecheck_unify.m
--- modecheck_unify.m	1999/07/13 08:53:15	1.40
+++ modecheck_unify.m	1999/09/13 09:57:53
@@ -409,25 +409,46 @@
 	mode_info_get_how_to_check(ModeInfo0, HowToCheckGoal),
 
 	%
-	% fully module qualify all cons_ids
+	% Fully module qualify all cons_ids
 	% (except for builtins such as ints and characters).
 	%
 	(
-		ConsId0 = cons(Name, OrigArity),
+		ConsId0 = cons(Name0, OrigArity),
 		type_to_type_id(TypeOfX, TypeId, _),
 		TypeId = qualified(TypeModule, _) - _
 	->
-		unqualify_name(Name, UnqualName),
-		ConsId = cons(qualified(TypeModule, UnqualName), OrigArity)
+		unqualify_name(Name0, UnqualName),
+		Name = qualified(TypeModule, UnqualName),
+		ConsId = cons(Name, OrigArity),
+		%
+		% Fix up the cons_id arity for type(class)_info constructions.
+		% The cons_id for type(class)_info constructions always has
+		% arity 1, to match the arity in the declaration in
+		% library/private_builtin.m,
+		% but for the inst we need the arity of the cons_id
+		% to match the number of arguments.
+		%
+		(
+			mercury_private_builtin_module(TypeModule),
+			( UnqualName = "typeclass_info"
+			; UnqualName = "type_info"
+			)
+		->
+			list__length(ArgVars0, InstArity),
+			InstConsId = cons(Name, InstArity)
+		;
+			InstConsId = ConsId
+		)
 	;
-		ConsId = ConsId0
+		ConsId = ConsId0,
+		InstConsId = ConsId
 	),
 	mode_info_get_instmap(ModeInfo0, InstMap0),
 	instmap__lookup_var(InstMap0, X, InstOfX),
 	instmap__lookup_vars(ArgVars0, InstMap0, InstArgs),
 	mode_info_var_is_live(ModeInfo0, X, LiveX),
 	mode_info_var_list_is_live(ArgVars0, ModeInfo0, LiveArgs),
-	InstOfY = bound(unique, [functor(ConsId, InstArgs)]),
+	InstOfY = bound(unique, [functor(InstConsId, InstArgs)]),
 	(
 		% The occur check: X = f(X) is considered a mode error
 		% unless X is ground.  (Actually it wouldn't be that
@@ -440,7 +461,7 @@
 	->
 		set__list_to_set([X], WaitingVars),
 		mode_info_error(WaitingVars,
-			mode_error_unify_var_functor(X, ConsId, ArgVars0,
+			mode_error_unify_var_functor(X, InstConsId, ArgVars0,
 							InstOfX, InstArgs),
 			ModeInfo0, ModeInfo1
 		),
@@ -465,7 +486,7 @@
 		ArgVars = ArgVars0,
 		ExtraGoals = no_extra_goals
 	;
-		abstractly_unify_inst_functor(LiveX, InstOfX, ConsId,
+		abstractly_unify_inst_functor(LiveX, InstOfX, InstConsId,
 			InstArgs, LiveArgs, real_unify, ModuleInfo0,
 			UnifyInst, Det1, ModuleInfo1)
 	->
@@ -483,7 +504,7 @@
 		(
 			inst_expand(ModuleInfo1, InstOfX, InstOfX1),
 			list__length(ArgVars0, Arity),
-			get_arg_insts(InstOfX1, ConsId, Arity, InstOfXArgs),
+			get_arg_insts(InstOfX1, InstConsId, Arity, InstOfXArgs),
 			get_mode_of_args(Inst, InstOfXArgs, ModeOfXArgs0)
 		->
 			ModeOfXArgs = ModeOfXArgs0
@@ -507,7 +528,7 @@
 	;
 		set__list_to_set([X | ArgVars0], WaitingVars), % conservative
 		mode_info_error(WaitingVars,
-			mode_error_unify_var_functor(X, ConsId, ArgVars0,
+			mode_error_unify_var_functor(X, InstConsId, ArgVars0,
 							InstOfX, InstArgs),
 			ModeInfo0, ModeInfo1
 		),
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.19
diff -u -r1.19 Mmakefile
--- Mmakefile	1999/08/13 01:43:50	1.19
+++ Mmakefile	1999/09/13 10:00:42
@@ -11,6 +11,7 @@
 	extract_typeinfo \
 	existential_type_classes \
 	existential_data_types \
+	existential_data_types_regr_test \
 	extra_typeinfo \
 	func_default_mode_bug \
 	ho_map \
Index: tests/hard_coded/typeclasses/existential_data_types_regr_test.exp
===================================================================
RCS file: existential_data_types_regr_test.exp
diff -N existential_data_types_regr_test.exp
--- /dev/null	Mon Sep 13 20:05:00 1999
+++ existential_data_types_regr_test.exp	Mon Sep 13 19:59:45 1999
@@ -0,0 +1 @@
+3
Index: tests/hard_coded/typeclasses/existential_data_types_regr_test.m
===================================================================
RCS file: existential_data_types_regr_test.m
diff -N existential_data_types_regr_test.m
--- /dev/null	Mon Sep 13 20:05:00 1999
+++ existential_data_types_regr_test.m	Mon Sep 13 20:02:53 1999
@@ -0,0 +1,58 @@
+% This is a regression test.  The Mercury compiler of 12 Sept 199
+% reported a spurious mode error for this test case.
+
+:- module existential_data_types_regr_test.
+%------------------------------------------------------------
+:- interface.
+:- import_module io.
+
+:- pred main( state, state).
+:- mode main( di,    uo   ) is det.
+
+%------------------------------------------------------------
+:- implementation.
+:- import_module int.
+:- use_module require.
+
+:- typeclass int_singleton(T) where [
+       func value(T) = int
+   ].
+
+:- type zero ---> zero.
+
+:- instance int_singleton(zero) where [
+       func(value/1) is zero_value
+   ].
+
+:- type succ(N) ---> succ(N).
+
+:- instance int_singleton(succ(N)) <= int_singleton(N) where [
+       func(value/1) is succ_value
+   ].
+
+:- func zero_value(zero) = int.
+zero_value(_) = 0.
+
+:- func succ_value(succ(N)) = int <= int_singleton(N).
+succ_value(succ(N)) = value(N)+1.
+
+:- type natural_number ---> some [N] (nat(N) => int_singleton(N)).
+
+:- func to_natural_number(int) = natural_number.
+to_natural_number(I) = Result :-
+    ( I=0 ->
+        Result = 'new nat'(zero)
+    ; I>0 ->
+        nat(N1) = to_natural_number(I-1),
+        Result = 'new nat'(succ(N1))
+    ; % I<0,
+        require__error("to_natural_number: cannot convert negative integer")
+    ).
+
+main -->
+    { nat(N) = to_natural_number(3) },
+    print(value(N)),
+    nl.
+
+%------------------------------------------------------------
+:- end_module existential_data_types_regr_test.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------