obj Elem;
obj Stack =  e:Elem*;
-- obj IntStack < Stack where: Elem = IntElem; end;
-- Next def replaces preceding to give semantics of not-yet-implemented generic
-- instantiation.
obj IntStack =  e:IntElem* and;(*< Stack where: Elem = IntElem; end;*)
obj IntElem < Elem =  integer;
obj StrStack < Stack where: Elem = StrElem; end;
obj StrElem < Elem =  string;


op Push(Stack,Elem)->Stack;
op Push(IntStack,IntElem)->IntStack;
op Push(StrStack,StrElem)->IntStack;
op Pop(Stack)->Elem;
op Pop(ist:IntStack)->IntElem = ist.e[1];
op Pop(StrStack)->StrElem;

op main(s:Stack,ist:IntStack,i:integer,ie:IntElem,se:StrElem) = (
    Push(s, i);		(* ERROR, since int !< Elem, and T={T} cant help *)
    Push(ist,se);	(* ERROR, per new superflash rule. *)

    Push(ist,i);	(* Works by T = {T} rule. *)
    Push(ist,10);	(* Ibid. *)
    Push(s,ie);		(* Works, since IntElem < Elem *)
);


(*
 * The superflash above effectively trashes the entire discussion that follows
 * (starting in the next comment block).  We'll leave the discussion for
 * posterity.  With the new rule that generic instantiations are not subtypes,
 * the potentially problematic line just above, viz.  Push(ist,StrElem("abc")),
 * will no longer type check.  The reason it type checks without this new rule
 * is that IntStack is still < Stack, so that when the resolution to
 * Push_IntStack_IntElem fails, we can look at Push_Stack_Elem, via subtype
 * poly.  HOWEVER, the new rule says that subtype poly is out now.  Hence,
 * since there is no explicit def of Push(IntStack, StrElem) or Push(IntStack,
 * Elem), there can be no resolution of the problematic call.  Bitchin again.
 *
 * One way to look at the new rule (gen instantiations are not subtypes) is
 * that it implements automatically, and in the right places, the notion of
 * strict inheritance introduced below, but below required invention of a new
 * operator.  Can I have one more bitchin, please?
 *)


(*
 *
 * TRASHED DISCUSSION FOLLOWS.
 *
 * Here's an interesting position we might be finding ourselves in.  If both
 * int and string are subtypes of Elem, then we get in the situation where the
 * following might be type safe, even though we dont want it to be:
 *
 *     Push(IntStack(nil), "abc")
 *
 * The reason it might be type safe is as follows: since IntStack<Stack, the
 * preceding call could resolve to Push_Stack_Elem, after it fails to resolve
 * to Push_IntStack_IntElem.  We're saved here, since "abc" is a string lit
 * that wont bind directly to an Elem, so we can't reslove to Push_Stack_Elem.
 *
 * However, consider
 *
 *     Push(IntStack(nil), StrElem("abc"))
 *
 * Here, since StrElem<Elem, StrElem("abc") will bind to Elem.  So, when this
 * call fails to resolve to Push_IntStack_IntElem, it can now safely resolve to
 * Push_Stack_Elem.  The result is that we get a StrElem pushed onto an
 * IntStack, which may not be what we want if we had a homogeneous IntStack in
 * mind.
 *
 * So, the $64K question here is, can we get a truely homogeneous IntStack at
 * all in RSL, without having to hand duplicate all of the ops?  I.e., we want
 * to use inheritance-based generic instantiaion, but still get a homogeneous
 * IntStack.  The answer seems to be no in 3.1.
 *
 * One thing we might say is that we really don't care about this seemingly
 * unwanted heterogeneity, since we couldn't ever get strings directly off of
 * an IntStack, even though we could put them there.  This is because the only
 * non-generic selector we have for an IntStack returns an int, not a string.
 * Reasoning things out, consider the following example:
 *)

op main(s:Stack,ist:IntStack,ss:StrStack,i:integer,ie:IntElem,str:string) = (
    str = Pop(ss);
    i = Pop(ist);
    str = Pop(ist)	(* ERROR, since there's no Pop_IntStack->StrElem *)
);


(*
 * But, if we really want to solve the problem "properly", it's on to 4.0, in
 * which, among other things, we'll have the notion of strict inheritance, with
 * a new symbol to boot.  Here's the deal ... .  Normally, if T1 < T2, then
 * values of type T1 can be bound to vars of T2, but not vice versa (of
 * course).  With strict inheritance, which we'll denote T1 <!= T2 (verbosely
 * "T1 strict extends T2", where, we hope, the symbol '<!=' has the
 * mnemonic suggestion of "less than but not equal to"), the normal rule of
 * subtype binding does not apply.  Viz., if T1 <!= T2, values of type T1
 * canNOT be bound to vars of type T2.
 *
 * This acutally seems pretty cute, and even orthogonal  It will solve the
 * IntStack homogeneity problem (example below).  It would be nice if we could
 * find some other useful example(s) where it was helpful as well.
 *
 * What we should do here to cap off this disucssion, in addition to finding
 * some additional useful examples for strict inheritance, with a discussion of
 * why this particular problem seems not to show up in C++, at least not in
 * exactly the same way.  One reason is probably because ops *belong to*
 * objects, and all that biz.  Also, templates will figure in, since we're
 * talking about that kind of generics here.
 *)

-- obj StrictlyIntStack < Stack
--    where: Elem = IntElem;
-- end;
-- Next def replaces preceding to give semantics of not-yet-implemented generic
-- instantiation.
obj StrictlyIntStack =  e:IntElem* and;
op Push(StrictlyIntStack,IntElem)->StrictlyIntStack;
    (* This op should be automatically def'd by generic instantiation. *)

op main1(s:Stack,ist:StrictlyIntStack,i:integer,ie:IntElem,se:StrElem) = (
    Push(ist,i);
    Push(s,ie);
    Push(ist,10);
    Push(ist,se)	(* Should be ERROR because of strict inheritance. *)
);