[mercury-users] type error with existentially typed data structure

[Peter Ross]

With the attached file I get the following type error, and I am a bit
lost as to why it occurs.

petri.m:125: In clause for predicate `petri:bind_env/4':
petri.m:125:   in unification of variable `Env'
petri.m:125:   and term `BindEnv(Token)':
petri.m:125:   type error in argument(s) of higher-order term (with arity 1).
petri.m:125:   Functor (BindEnv) has type `((func T) = int)',
petri.m:125:   expected type was `((func V_9) = int)';
petri.m:125:   argument 1 (Token) has type `T',
petri.m:125:   expected type was `V_9'.
For more information, try recompiling with `-E'.
-------------- next part --------------
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
%
% Module: petri
% Author: petdr at miscrit.be
%
% This module represents a petri net.
%
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- module petri.

:- interface.

:- import_module set.

:- type petri.

:- type place(T).

:- type ref(T).

	% A new petri net.
:- func init = petri.

:- func new_place(string, set(T)) = place(T).

:- pred insert_place(place(T)::in, ref(place(T))::out,
		petri::in, petri::out) is det.

:- func get_place(petri, ref(place(T))) = place(T).

%-----------------------------------------------------------------------------%

:- implementation.

:- import_module int, list, map, set, std_util.

	% A petri net.
:- type petri
	--->	petri(
			next_id	:: int,
			map	:: map(int, univ)
		).

:- type tokens(T) == set(T).

:- type ref(T) ---> ref(int).

	% A single place in the petri net where tokens at this place
	% have a type T.
	%
:- type place(T)
	--->	place(
			name		:: string,
			tokens		:: tokens(T)
		).

	% An arc from a place to a transition, where we use bind to bind
	% the type T to some environment.
	%
:- type arc_place_transition
	--->	some [T] arc_place_transition(
			bind		:: bind(T),
			from		:: ref(place(T))
		).

	% An arc from a transition to a place where the type of the
	% resulting tokens, as computed by the arc expression, is T.
	%
:- type arc_transition_place
	--->	some [T] arc_transition_place(
			expression	:: expression(T),
			to		:: ref(place(T))
		).

	% A transition has a set of incoming arcs which are used to bind
	% the environment.  This environment is then used by the outgoing
	% arcs to decide whether or not to place tokens in the output
	% petri net.
	%
:- type transition
	--->	transition(
			ingoing  :: list(arc_place_transition),
			outgoing :: list(arc_transition_place)
		).

	% An expression is a user defined function which maps the
	% enviroment bound by all the incoming arcs to the set of
	% tokens which should be placed into the destination place.  It
	% is possibly because we may not want to create a token at all.
	%
	% XXX Maybe at some later date we will also probably want to
	% paramaterise the environment, so as to avoid more bugs!
	%
:- type expression(T) == (func(environment) = set(T)).
	
:- type bind(T) == (func(T) = environment).

:- type environment == int.

%-----------------------------------------------------------------------------%

init = petri(0, map__init).

new_place(Name, Tokens) = place(Name, Tokens).

insert_place(Place, ref(Id), petri(Id, Map0), petri(Id + 1, Map)) :-
	map__det_insert(Map0, Id, univ(Place), Map).

get_place(petri(_NextId, Map), ref(Id)) = Place :-
	map__lookup(Map, Id, UnivPlace),
	det_univ_to_type(UnivPlace, Place).

%-----------------------------------------------------------------------------%

:- pred bind_env(arc_place_transition::in, environment::out,
		petri::in, petri::out) is nondet.

bind_env(ArcPlaceTransition, Env, Petri0, Petri) :-
	Place = get_place(Petri0, ArcPlaceTransition ^ from),
	BindEnv = ArcPlaceTransition ^ bind,
	set__member(Token, Place ^ tokens),
	Env = BindEnv(Token),
	Petri = Petri0.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

/*
:- inst bind == (func(ground >> ground) = (free >> ground) is det).
:- inst arc_place_transition == bound(arc_place_transition(ground, bind)).
:- inst bind_list == list_skel(pair(ground, bind)).

:- pred find_environment(list(pair(place(T), bind(T)))::in(bind_list),
		environment::out) is cc_nondet.

find_environment([], _) :-
	error("find_environment called with an empty list []").
find_environment([Place - Bind | Rest], Env) :-
	bind(Place, Bind, _Token, InitialEnv),
	find_environment_2(Rest, InitialEnv, Env).

:- pred find_environment_2(list(pair(place(T), bind(T)))::in(bind_list),
		environment::in, environment::out) is cc_nondet.

find_environment_2([], Env, Env).
find_environment_2([Place - Bind | Rest], InitialEnv, Env) :-
	bind(Place, Bind, _Token, BoundEnv),
	compatible_environments(InitialEnv, BoundEnv, Env0),
	find_environment_2(Rest, Env0, Env).

:- pred compatible_environments(environment::in, environment::in,
		environment::out) is semidet.

compatible_environments(Env, Env, Env).

	% Given one place and a function to bind a token at that place
	% with an enviroment, do it.
:- pred bind(place(T)::in, bind(T)::in, T::out, environment::out) is nondet.

bind(Place, Bind, Token, Env) :-
	set__member(Token, Place ^ tokens),
	Env = Bind(Token).
*/
	
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%