From b7c4bcf42e0354ac2908c04f3b581e8c85f4e4d7 Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Fri, 17 May 2024 10:46:18 -0700
Subject: [PATCH] [BoS] Fix description of subtyping (#54)

Stack types are contravariant in all their parameters, including the return
stack reference.
---
 proposals/bag-o-stacks/Explainer.md | 32 +++++++++--------------------
 1 file changed, 10 insertions(+), 22 deletions(-)

diff --git a/proposals/bag-o-stacks/Explainer.md b/proposals/bag-o-stacks/Explainer.md
index 9f8d311b0e..24e1b65af2 100644
--- a/proposals/bag-o-stacks/Explainer.md
+++ b/proposals/bag-o-stacks/Explainer.md
@@ -114,36 +114,24 @@ In order for a switch between coroutines to be valid, the type of the target sta
 
 Given this, we can statically verify that WebAssembly programs that switch between coroutines are guaranteed to observe type safety during the switch.
 
-#### Subtype relations between `stack` types
+#### Subtyping
 
-Like function types, two stack types
+Like function types, stack types are contravariant in their parameters.
 
-```wasm
-(stack (param P1*) (ref $c1))
-```
-
-and
-
-```wasm
-(stack (param P2*) (ref $c2))
+```pseudo
+C |- stack t_1* rt_1 <: stack t_2* rt_2
+-- C |- t_2* rt_2 <: t_1* rt_1
 ```
 
-are in a subtype relationship if the `P1*` vector is a vector subtype of `P2*` and the type referenced in `$c2` is a subtype of $c1. I.e., covariant in the result types but contravariant in the parameter types. This is directly analogous to function subtyping.
+`stack t_1 rt_1` is a subtype of `stack t_2* rt_2` iff:
+ - `t_2* rt_2` is a subtype of `t_1* rt_1`.
 
-The top type for stack references is simply:
+The top type for stack references is `stack` and the bottom type is `nostack`. Like other bottom types, the nostack type is uninhabited.
 
-```wasm
-stack
-```
-
-and the bottom type is `nostack` which results in a new extension to the heap type hierarchy:
-
-```wasm
-heaptype ::= ... | stack | nostack
+```pseudo
+absheaptype ::= ... | stack | nostack
 ```
 
-Like other bottom types, the nostack type is uninhabited.
-
 ### Life-cycle of a coroutine
 
 A coroutine is started using the `stack.new_switch` instruction. This performs the equivalent of a function call – on a new stack resource. In addition to the arguments normally expected in a function call, an additional argument is provided that is a stack reference to the caller code -- the caller is suspended as a result of the `stack.new_switch` instruction.