[m-rev.] for review: Clearly explain what part of partial instantiation isn't supported.

[Paul Bone]

For review by anyone, this should be considered rather than my previous
patch on the same topic.

---

Clearly explain what part of partial instantiation isn't supported.

In (at least) two places we say that partial instantiation doesn't work or
isn't supported.  This has raised confusion so this patch attempts to
explain what exactly is unsupported and why.

doc/reference_manual.texi:
library/list.m:
LIMITATIONS:
    As above.

library/list.m:
    Delete deprecated modes.

    Move partial instantiation states and modes into a private interface
    section.  Note all of the instantiation states are partial, some can be
    safely used for subtyping so I've left those where they are.

LIMITATIONS:
    Include Zoltan's explanation of why this doesn't work for our future
    selves and others.
---
 LIMITATIONS               | 26 ++++++++++++++++---
 doc/reference_manual.texi |  8 +++---
 library/list.m            | 63 +++++++++++++++++++++++++++++++----------------
 3 files changed, 69 insertions(+), 28 deletions(-)

diff --git a/LIMITATIONS b/LIMITATIONS
index 7ae3d9d..3ec6600 100644
--- a/LIMITATIONS
+++ b/LIMITATIONS
@@ -3,16 +3,34 @@ The current implementation does not yet completely implement the
 Mercury language.  The main limitations of the current implementation
 are the following:
 
-* We do not allow definite aliasing in the mode system.
-  Without this, partially instantiated modes are unusable, 
-  and so are nested unique modes :-(
+* We do not allow definite aliasing in the mode system.  Without this,
+  partially instantiated modes are unusable, and so are nested unique modes
+  :-(  When partial instantiation appears to work it is only by chance.  The
+  detailed explanation is:
+
+    If you unify a variable and an argument of a term, then when either the
+    variable or the argument is bound, the other should be bound to the same
+    thing. In the absence of alias tracking, this won't happen. The only
+    situation in which this is ok is if "the other" does not exist anymore,
+    which the current compiler can be sure about only if its scope is
+    restricted to the unification.
+
+    Even for code in which a free variable's scope is confined to its
+    unification with a free variable in a term, the code generators are
+    not guaranteed to handle the resulting partially instantiated terms
+    correctly, simply because they weren't *designed* to. Mantis bug 311
+    shows this very clearly. Though I can imagine the different backends
+    misbehaving differently on such code. Some may even generate correct
+    code by accident :-)
+
+  This does not affect support for instantiation state subtyping.
 
 * The compiler does not yet use structure reuse or compile-time
   garbage collection to exploit unique modes :-(
 
 * Type inference and mode inference are a bit imperfect.
 
-We are working on eliminating all of these problems. 
+We hope to eliminate all of these problems.
 
 In addition, design decisions in this implementation have imposed the
 following fixed limits:
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index a7a34b2..fc6bbfc 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -2540,9 +2540,11 @@ can do so by simply defining them using a mode declaration:
 These two modes are enough for most functions and predicates.
 Nevertheless, Mercury's mode system is sufficiently
 expressive to handle more complex data-flow patterns,
-including those involving partially instantiated data structures.  
-(The current implementation does not handle
-partially instantiated data structures yet.)
+including those involving partially instantiated data structures, data
+structures with ``free'' @emph{holes} in them.
+(In the current implementation, partially instantiated data structures are
+unsupported due to a lack of alias tracking in the mode system.  For more
+information please see the @file{LIMITATIONS} file distributed with Mercury.)
 
 For example, consider an
 interface to a database that associates data with keys, and provides
diff --git a/library/list.m b/library/list.m
index 102edb6..91d25fc 100644
--- a/library/list.m
+++ b/library/list.m
@@ -34,32 +34,23 @@
 
 %-----------------------------------------------------------------------------%
 
-    % Some declarations for complicated modes using lists.
-    % (Note that partial instantiation is not currently supported.)
-
+    % These instantiation states and modes can be used for instantiation
+    % state subtyping.
+    %
+    % They could also be used for partial instantiation but partial
+    % instantiation does not work completely.  Mercury's mode system does
+    % not attempt to perform alias tracking.  Therefore filling in the
+    % 'holes' of a partially instantiated data structure may not work as
+    % expected, when this appears to work it is only by chance.  Furthermore
+    % partial instantiations are not supported on the Erlang backend at all.
+    % Additionally most existing code is not instantiation state polymorphic
+    % (for example the standard library itself).
+    %
 :- inst list_skel(I) ---> [] ; [I | list_skel(I)].
-:- inst list_skel == list_skel(free).
 :- inst list(I) == list_skel(I).
 
 :- inst non_empty_list ---> [ground | ground].
 
-:- mode in_list_skel  == list_skel >> list_skel.
-:- mode out_list_skel == free >> list_skel.
-:- mode list_skel_out == list_skel >> ground.
-
-    % These more verbose versions are deprecated.
-    % They exist only for backwards compatibility,
-    % and will be removed in a future release.
-:- mode input_list_skel  == in_list_skel.
-:- mode output_list_skel == out_list_skel.
-:- mode list_skel_output == list_skel_out.
-
-    % These modes are particularly useful for passing around lists
-    % of higher order terms, since they have complicated insts
-    % which are not correctly approximated by "ground".
-:- mode list_skel_in(I)  == list_skel(I) >> list_skel(I).
-:- mode list_skel_out(I) == free >> list_skel(I).
-
 %-----------------------------------------------------------------------------%
 
 :- pred list.is_empty(list(T)::in) is semidet.
@@ -3305,5 +3296,35 @@ public static List_1 det_tail(List_1 lst)
 ").
 
 %-----------------------------------------------------------------------------%
+
+%
+% Private interface for definitions that are available but hidden from
+% documentation.
+%
+
+:- interface.
+
+    % Some declarations for complicated modes using lists.
+    %
+    % See our comment above regarding incomplete  support for partial
+    % instantiation.
+
+:- inst list_skel == list_skel(free).
+
+:- mode in_list_skel  == list_skel >> list_skel.
+:- mode out_list_skel == free >> list_skel.
+:- mode list_skel_out == list_skel >> ground.
+
+    % These modes are useful for passing around lists of higher order terms,
+    % since they have complicated insts which are not correctly approximated
+    % by "ground".
+    %
+    % These could be made public (not deprecated) however I prefer to
+    % encourage the in(list_skel(I)) and out(list_skel(I)) style syntax.
+    %
+:- mode list_skel_in(I)  == list_skel(I) >> list_skel(I).
+:- mode list_skel_out(I) == free >> list_skel(I).
+
+%-----------------------------------------------------------------------------%
 :- end_module list.
 %-----------------------------------------------------------------------------%
-- 
1.9.0