HAK Note: This is, verbatim, reproduction of the earliest specification
motivating the need for and explaining the simple scheme of incremental
constraint inheritance that should have been implemented later in
WildLife but was not (!). It is taken from the original message send by
HAK to the prl.paradise list in PRL on Mon, 19 Aug 91.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

3) Number representation bug?

	> foo := I:int | write(I).
	*** Warning: overwriting old definition of type 'int'.
	*Ok.
	> encode?
	*** Encoding done, 14 types.

	*** Yes.
	--1> X:foo=2?
	foo
	*** Yes.
	X = foo:2.
	----2>

I expect '2' (or possibly 'foo:2') to be written rather than just 'foo'.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

4) In the example above, if I pursue the query at level 2 with:

	----2> X = foo?

I get:

	foo
	*** Yes
	X = foo:2.
	------3>

This is not what I expected: since X has already been proven to be a
'foo', there is no need (and indeed, no use) for re-proving its
definition's associated constraint.

In general, the inheritance of constraints must "memoize" (yes, no 'r')
the proven contraints, such that, if:

	a := b | pa.
	b := c | pb.
	c := d | pc.

and I query:

	X = c, X = b, X = a?

the first unification proves 'pc', the second proves 'pb' but not 'pc',
and the third proves 'pa' but neither 'pb' nor 'pc'.

A way to do that is to tag the constraints with the sort they have been
inherited from so that when the static propagation of constraints is
done for the sort definitions, this sort tag information will allow the
discriminating bevavior I expect.

For the above example, the static inheritance would yield, in the
current implementation:

	a := b | pa,pb,pc.
	b := c | pb,pc.
	c := d | pc.

But with tagged constraints:

	a := b | a#pa,b#pb,c#pc.
	b := c | b#pb,c#pc.
	c := d | c#pc.

so that when 'X = c' is invoked, c#pc is done. If we add 'X = b', then
the fact that X has already been porven to be a 'c' will not invoke 'c#pc'
but only 'b#pb', etc...

Note incidentally that this constraint-tagging scheme also allows
avoiding redundant constraints due to inheritance through multiple
paths. Clearly, The duplication is then easy to avoid at the static
inheritance phase.

(Of course, the above tags are only internal and invisible to the user
- -- at least in naive use mode.)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~