diff --git a/scripts/test/fuzzing.py b/scripts/test/fuzzing.py
index a41a638683c..4926f908bc9 100644
--- a/scripts/test/fuzzing.py
+++ b/scripts/test/fuzzing.py
@@ -22,6 +22,7 @@
     'strings.wast',
     'simplify-locals-strings.wast',
     'string-lowering-instructions.wast',
+    'type-generalizing-strings.wast',
     # TODO: fuzzer and interpreter support for extern conversions
     'extern-conversions.wast',
     # ignore DWARF because it is incompatible with multivalue atm
diff --git a/src/ir/child-typer.h b/src/ir/child-typer.h
index 1e121cedce2..29ec1f4e8c8 100644
--- a/src/ir/child-typer.h
+++ b/src/ir/child-typer.h
@@ -862,7 +862,9 @@ template<typename Subtype> struct ChildTyper : OverriddenVisitor<Subtype> {
   void visitRefI31(RefI31* curr) { note(&curr->value, Type::i32); }
 
   void visitI31Get(I31Get* curr) {
-    note(&curr->i31, Type(HeapType::i31, Nullable));
+    // Polymorphic over sharedness.
+    note(&curr->i31,
+         VarRef{Nullable, VarAbsHeapType{VarSharedness{0u}, HeapType::i31}});
   }
 
   void visitCallRef(CallRef* curr, std::optional<HeapType> ht = std::nullopt) {
@@ -973,7 +975,7 @@ template<typename Subtype> struct ChildTyper : OverriddenVisitor<Subtype> {
       }
     }
     if (auto desc = curr->type.getHeapType().getDescriptorType()) {
-      note(&curr->desc, Type(*desc, NonNullable, Exact));
+      note(&curr->desc, Type(*desc, Nullable, Exact));
     }
   }
 
@@ -1167,7 +1169,9 @@ template<typename Subtype> struct ChildTyper : OverriddenVisitor<Subtype> {
   }
 
   void visitArrayLen(ArrayLen* curr) {
-    note(&curr->ref, Type(HeapType::array, Nullable));
+    // Polymorphic over sharedness.
+    note(&curr->ref,
+         VarRef{Nullable, VarAbsHeapType{VarSharedness{0u}, HeapType::array}});
   }
 
   void visitArrayCopy(ArrayCopy* curr,
diff --git a/src/passes/OptimizeInstructions.cpp b/src/passes/OptimizeInstructions.cpp
index cfeb478acaa..c55321b4651 100644
--- a/src/passes/OptimizeInstructions.cpp
+++ b/src/passes/OptimizeInstructions.cpp
@@ -1576,6 +1576,9 @@ struct OptimizeInstructions
   //    Given the large amount of potential benefit we can get from a successful
   //    optimization in GUFA, any reduction there may be a bad idea, so we
   //    should be very careful and probably *not* remove such casts.
+  //
+  // The only case where we are always ok to remove such casts is when lastOpts
+  // is true, because nothing significant runs after us that can be harmed.
 
   // If an instruction traps on a null input, there is no need for a
   // ref.as_non_null on that input: we will trap either way (and the binaryen
diff --git a/src/passes/TypeGeneralizing.cpp b/src/passes/TypeGeneralizing.cpp
index e907c2c4c8a..09c1ed15bb2 100644
--- a/src/passes/TypeGeneralizing.cpp
+++ b/src/passes/TypeGeneralizing.cpp
@@ -14,905 +14,520 @@
  * limitations under the License.
  */
 
-#include "analysis/cfg.h"
-#include "analysis/lattices/inverted.h"
-#include "analysis/lattices/shared.h"
-#include "analysis/lattices/stack.h"
-#include "analysis/lattices/tuple.h"
-#include "analysis/lattices/valtype.h"
-#include "analysis/lattices/vector.h"
-#include "analysis/monotone-analyzer.h"
+//
+// Generalize the types of locals as much as possible, both to eliminate
+// unnecessarily refined types from the type section and (TODO) to weaken casts
+// that cast to unnecessarily refined types. If the casts are weakened enough,
+// they will be able to be removed by OptimizeInstructions/StripRefiningCasts.
+//
+
+#include <optional>
+#include <unordered_map>
+#include <variant>
+#include <vector>
+
+#include "ir/branch-utils.h"
+#include "ir/child-typer.h"
+#include "ir/glbs.h"
 #include "ir/utils.h"
 #include "pass.h"
 #include "wasm-traversal.h"
 #include "wasm.h"
 
-#ifndef TYPE_GENERALIZING_DEBUG
-#define TYPE_GENERALIZING_DEBUG 0
-#endif
-
-#if TYPE_GENERALIZING_DEBUG
-#define DBG(statement) statement
-#else
-#define DBG(statement)
-#endif
-
-// Generalize the types of program locations as much as possible, both to
-// eliminate unnecessarily refined types from the type section and (TODO) to
-// weaken casts that cast to unnecessarily refined types. If the casts are
-// weakened enough, they will be able to be removed by OptimizeInstructions.
-//
-// Perform a backward analysis tracking requirements on the types of program
-// locations (currently just locals and stack values) to discover how much the
-// type of each location can be generalized without breaking validation or
-// changing program behavior.
-
 namespace wasm {
 
 namespace {
 
-using namespace analysis;
-
-// We will learn stricter and stricter requirements as we perform the analysis,
-// so more specific types need to be higher up the lattice.
-using TypeRequirement = Inverted<ValType>;
-
-// Record a type requirement for each local variable. Shared the requirements
-// across basic blocks.
-using LocalTypeRequirements = SharedPath<Vector<TypeRequirement>>;
-
-// The type requirements for each reference-typed value on the stack at a
-// particular location.
-using ValueStackTypeRequirements = Stack<TypeRequirement>;
-
-// The full lattice used for the analysis.
-using StateLattice =
-  analysis::Tuple<LocalTypeRequirements, ValueStackTypeRequirements>;
-
-// Equip the state lattice with helpful accessors.
-struct State : StateLattice {
-  using Element = StateLattice::Element;
-
-  static constexpr int LocalsIndex = 0;
-  static constexpr int StackIndex = 1;
-
-  State(Function* func)
-    : StateLattice{SharedPath{initLocals(func)}, initStack()} {}
-
-  void push(Element& elem, Type type) const noexcept {
-    stackLattice().push(stack(elem), std::move(type));
-  }
-
-  Type pop(Element& elem) const noexcept {
-    return stackLattice().pop(stack(elem));
-  }
-
-  void clearStack(Element& elem) const noexcept {
-    stack(elem) = stackLattice().getBottom();
+// Find the most general supertype of a signature type that does not change
+// parameter types (which are contravariant and would restrict argument
+// generalization) and whose result type satisfies `resultReq`, if any.
+HeapType generalizeCallRefTarget(HeapType sigType,
+                                 std::optional<Type> resultReq = std::nullopt) {
+  auto sig = sigType.getSignature();
+  auto numParams = sig.params.size();
+  auto targetReq = sigType;
+  while (true) {
+    auto candidateReq = targetReq.getDeclaredSuperType();
+    if (!candidateReq) {
+      break;
+    }
+    auto candidateSig = candidateReq->getSignature();
+    if (resultReq && !Type::isSubType(candidateSig.results, *resultReq)) {
+      break;
+    }
+    for (size_t i = 0; i < numParams; ++i) {
+      if (candidateSig.params[i] != sig.params[i]) {
+        return targetReq;
+      }
+    }
+    targetReq = *candidateReq;
   }
+  return targetReq;
+}
 
-  const std::vector<Type>& getLocals(Element& elem) const noexcept {
-    return *locals(elem);
+// Find the most general supertype of a struct type that still has a field at
+// `index` whose type satisfies `reqFieldType`, if any.
+HeapType generalizeStructType(HeapType type,
+                              Index index,
+                              std::optional<Type> reqFieldType = std::nullopt) {
+  while (true) {
+    auto candidateType = type.getDeclaredSuperType();
+    if (!candidateType) {
+      break;
+    }
+    const auto& candidateFields = candidateType->getStruct().fields;
+    if (candidateFields.size() <= index) {
+      break;
+    }
+    if (reqFieldType) {
+      auto candidateFieldType = candidateFields[index].type;
+      if (!Type::isSubType(candidateFieldType, *reqFieldType)) {
+        break;
+      }
+    }
+    type = *candidateType;
   }
+  return type;
+}
 
-  const std::vector<Type>& getLocals() const noexcept {
-    return *locals(getBottom());
+// Find the most general supertype of an array type whose element type satisfies
+// `reqElemType`, if any.
+HeapType generalizeArrayType(HeapType type,
+                             std::optional<Type> reqElemType = std::nullopt) {
+  while (true) {
+    auto candidateType = type.getDeclaredSuperType();
+    if (!candidateType) {
+      break;
+    }
+    if (reqElemType) {
+      auto candidateElemType = candidateType->getArray().element.type;
+      if (!Type::isSubType(candidateElemType, *reqElemType)) {
+        break;
+      }
+    }
+    type = *candidateType;
   }
+  return type;
+}
 
-  Type getLocal(Element& elem, Index i) const noexcept {
-    return getLocals(elem)[i];
-  }
+// Use ChildTyper to find all subtyping constraints on expressions and locals,
+// and compute the greatest lower bound (GLB) of the required supertypes for
+// each local so that each local is given the least-refined valid type.
+//
+// TODO: handle ref.as_non_null, br_on_null, publish, br_if, etc. better: we do
+//       not need to consider their results fixed.
+struct Generalizer : public ChildTyper<Generalizer> {
 
-  bool updateLocal(Element& elem, Index i, Type type) const noexcept {
-    return localsLattice().join(
-      locals(elem),
-      Vector<TypeRequirement>::SingletonElement(i, std::move(type)));
-  }
+  using Super = ChildTyper<Generalizer>;
 
-private:
-  static LocalTypeRequirements initLocals(Function* func) noexcept {
-    return SharedPath{Vector{Inverted{ValType{}}, func->getNumLocals()}};
-  }
+  // For each expression and local, track the GLB of all types it is required to
+  // be a subtype of.
+  std::unordered_map<Expression*, GLBFinder> exprGLBs;
+  std::vector<GLBFinder> localGLBs;
 
-  static ValueStackTypeRequirements initStack() noexcept {
-    return Stack{Inverted{ValType{}}};
-  }
+  // Map from an expression to the sub-expressions whose types flow out of it
+  // (or depend on its required output type, as in RefAs).
+  std::unordered_map<Expression*, std::vector<Expression*>> exprSubs;
 
-  const LocalTypeRequirements& localsLattice() const noexcept {
-    return std::get<LocalsIndex>(lattices);
-  }
+  // For each local, the values assigned to it via local.set / local.tee.
+  std::vector<std::vector<Expression*>> localSetValues;
 
-  const ValueStackTypeRequirements& stackLattice() const noexcept {
-    return std::get<StackIndex>(lattices);
-  }
+  // We use a worklist of things to process: expressions and local indexes.
+  using WorkItem = std::variant<Expression*, Index>;
+  std::vector<WorkItem> worklist;
 
-  typename LocalTypeRequirements::Element&
-  locals(Element& elem) const noexcept {
-    return std::get<LocalsIndex>(elem);
-  }
+  Expression* currExpr = nullptr;
 
-  const typename LocalTypeRequirements::Element&
-  locals(const Element& elem) const noexcept {
-    return std::get<LocalsIndex>(elem);
-  }
+  // Walker for the code, using ControlFlowWalker for findBreakTarget.
+  struct Walker : ControlFlowWalker<Walker, UnifiedExpressionVisitor<Walker>> {
+    Generalizer& generalizer;
+    Walker(Generalizer& generalizer) : generalizer(generalizer) {}
+    void visitExpression(Expression* curr) {
+      generalizer.currExpr = curr;
+      generalizer.visit(curr);
+    }
+  } walker{*this};
 
-  typename ValueStackTypeRequirements::Element&
-  stack(Element& elem) const noexcept {
-    return std::get<StackIndex>(elem);
-  }
+  Generalizer(Module& wasm, Function* func)
+    : Super(wasm, func), localGLBs(func->getNumLocals()),
+      localSetValues(func->getNumLocals()) {}
 
-  const typename ValueStackTypeRequirements::Element&
-  stack(const Element& elem) const noexcept {
-    return std::get<StackIndex>(elem);
+  void walk() {
+    addConstraint(func->body, func->getResults());
+    walker.walkFunctionInModule(func, &wasm);
   }
-};
 
-struct TransferFn : OverriddenVisitor<TransferFn> {
-  Module& wasm;
-  Function* func;
-  State lattice;
-  typename State::Element* state = nullptr;
-
-  // For each local, the set of blocks we may need to re-analyze when we update
-  // the constraint on the local.
-  std::vector<std::vector<const BasicBlock*>> localDependents;
-
-  // The set of basic blocks that may depend on the result of the current
-  // transfer.
-  std::unordered_set<const BasicBlock*> currDependents;
-
-  TransferFn(Module& wasm, Function* func, CFG& cfg)
-    : wasm(wasm), func(func), lattice(func),
-      localDependents(func->getNumLocals()) {
-    // Initialize `localDependents`. Any block containing a `local.set l` may
-    // need to be re-analyzed whenever the constraint on `l` is updated.
-    auto numLocals = func->getNumLocals();
-    std::vector<std::unordered_set<const BasicBlock*>> dependentSets(numLocals);
-    for (const auto& bb : cfg) {
-      for (const auto* inst : bb) {
-        if (auto set = inst->dynCast<LocalSet>()) {
-          dependentSets[set->index].insert(&bb);
-        }
-      }
-    }
-    for (size_t i = 0, n = dependentSets.size(); i < n; ++i) {
-      localDependents[i] = std::vector<const BasicBlock*>(
-        dependentSets[i].begin(), dependentSets[i].end());
+  void addConstraint(Expression* expr, Type type) {
+    if (!expr->type.isRef() || !type.isRef()) {
+      return;
     }
-  }
-
-  Type pop() noexcept { return lattice.pop(*state); }
-  void push(Type type) noexcept { lattice.push(*state, type); }
-  void clearStack() noexcept { lattice.clearStack(*state); }
-  Type getLocal(Index i) noexcept { return lattice.getLocal(*state, i); }
-  void updateLocal(Index i, Type type) noexcept {
-    if (lattice.updateLocal(*state, i, type)) {
-      currDependents.insert(localDependents[i].begin(),
-                            localDependents[i].end());
+    auto& glb = exprGLBs[expr];
+    auto old = glb.getGLB();
+    glb.note(type);
+    if (glb.getGLB() != old) {
+      worklist.push_back(expr);
     }
   }
 
-  void dumpState() {
-#if TYPE_GENERALIZING_DEBUG
-    std::cerr << "locals: ";
-    for (size_t i = 0, n = lattice.getLocals(*state).size(); i < n; ++i) {
-      if (i != 0) {
-        std::cerr << ", ";
-      }
-      std::cerr << getLocal(i);
+  void addConstraint(Index local, Type type) {
+    if (!func->isVar(local) || !func->getLocalType(local).isRef() ||
+        !type.isRef()) {
+      return;
     }
-    std::cerr << "\nstack: ";
-    auto& stack = std::get<1>(*state);
-    for (size_t i = 0, n = stack.size(); i < n; ++i) {
-      if (i != 0) {
-        std::cerr << ", ";
-      }
-      std::cerr << stack[i];
+    auto& glb = localGLBs[local];
+    auto old = glb.getGLB();
+    glb.note(type);
+    if (glb.getGLB() != old) {
+      worklist.push_back(local);
     }
-    std::cerr << "\n";
-#endif // TYPE_GENERALIZING_DEBUG
   }
 
-  std::unordered_set<const BasicBlock*>
-  transfer(const BasicBlock& bb, typename State::Element& elem) noexcept {
-    DBG(std::cerr << "transferring bb " << bb.getIndex() << "\n");
-    state = &elem;
-
-    // This is a backward analysis: The constraints on a type depend on how it
-    // will be used in the future. Traverse the basic block in reverse and
-    // return the predecessors as the dependent blocks.
-    assert(currDependents.empty());
-    const auto& preds = bb.preds();
-    currDependents.insert(preds.begin(), preds.end());
+  Type getLabelType(Name label) { return walker.findBreakTarget(label)->type; }
 
-    dumpState();
-    if (bb.isExit()) {
-      DBG(std::cerr << "visiting exit\n");
-      visitFunctionExit();
-      dumpState();
+  void noteUnknown() {
+    // When we do not have enough information in the IR, constrain each child to
+    // its current type, which is always safe.
+    for (auto* child : ChildIterator(currExpr)) {
+      addConstraint(child, child->type);
     }
-    for (auto it = bb.rbegin(); it != bb.rend(); ++it) {
-      DBG(std::cerr << "visiting " << ShallowExpression{*it} << "\n");
-      visit(*it);
-      dumpState();
-    }
-    if (bb.isEntry()) {
-      DBG(std::cerr << "visiting entry\n");
-      visitFunctionEntry();
-      dumpState();
-    }
-    DBG(std::cerr << "\n");
-
-    state = nullptr;
-
-    // Return the blocks that may need to be re-analyzed.
-    return std::move(currDependents);
   }
 
-  void visitFunctionExit() {
-    // We cannot change the types of results. Push a requirement that the stack
-    // end up with the correct type.
-    auto result = func->getResults();
-    if (result.isRef()) {
-      push(result);
+  void note(Expression** childp, Constraints constraints) {
+    auto* child = *childp;
+    if (!child->type.isRef()) {
+      return;
     }
-  }
 
-  void visitFunctionEntry() {
-    // We cannot change the types of parameters, so require that they have their
-    // original types.
-    Index i = 0;
-    Index numParams = func->getNumParams();
-    Index numLocals = func->getNumLocals();
-    for (; i < numParams; ++i) {
-      updateLocal(i, func->getLocalType(i));
-    }
-    // We also cannot change the types of any other non-ref locals. For
-    // reference-typed locals, we cannot generalize beyond their top type.
-    for (Index i = numParams; i < numLocals; ++i) {
-      auto type = func->getLocalType(i);
-      // TODO: Support optimizing tuple locals.
-      if (type.isRef()) {
-        updateLocal(i, Type(type.getHeapType().getTop(), Nullable));
+    // Tuples are handled element by element in this pass, so we only receive a
+    // single constraint.
+    assert(constraints.size() == 1);
+    auto& type = constraints[0];
+    if (auto* t = std::get_if<Type>(&type)) {
+      // A constraint to a specific type.
+      addConstraint(child, *t);
+    } else if (auto* ref = std::get_if<VarRef>(&type)) {
+      // If the nullability is variable, set to nullable (as the indexed
+      // variable can appear nowhere else).
+      auto* nullp = std::get_if<Nullability>(&ref->null);
+      auto null = nullp ? *nullp : Nullable;
+
+      if (std::holds_alternative<Index>(ref->ht)) {
+        // The heap type is variable, so use the top.
+        addConstraint(child, Type(child->type.getHeapType().getTop(), null));
+      } else if (auto* abs = std::get_if<VarAbsHeapType>(&ref->ht)) {
+        // The heap type is abstract/basic, possibly with specified
+        // shareability (if not, use the current shareability).
+        auto* sharep = std::get_if<Shareability>(&abs->share);
+        auto share = sharep ? *sharep : child->type.getHeapType().getShared();
+        addConstraint(child, Type(abs->ht.getBasic(share), null));
+      } else if (auto* def = std::get_if<VarDefHeapType>(&ref->ht)) {
+        // The heap type is defined, possibly with specified exactness (if not,
+        // generalize to inexact).
+        auto* exactp = std::get_if<Exactness>(&def->exact);
+        auto exact = exactp ? *exactp : Inexact;
+        addConstraint(child, Type(def->ht, null, exact));
       } else {
-        updateLocal(i, type);
+        // A bottom heap type, but no expression in the IR mandates that.
+        WASM_UNREACHABLE("unexpected bottom heap type");
       }
-    }
-  }
-
-  void visitNop(Nop* curr) {}
-  void visitBlock(Block* curr) {}
-  void visitIf(If* curr) {}
-  void visitLoop(Loop* curr) {}
-
-  void visitBreak(Break* curr) {
-    if (curr->condition) {
-      // `br_if` pops everything but the sent value off the stack if the branch
-      // is taken, but if the branch is not taken, it only pops the condition.
-      // We must therefore propagate all requirements from the fallthrough
-      // successor but only the requirements for the sent value, if any, from
-      // the branch successor. We don't have any way to differentiate between
-      // requirements received from the two successors, however, so we cannot
-      // yet do anything correct here!
-      //
-      // Here is a sample program that would break if we tried to conservatively
-      // preserve the join of the requirements from both successors:
-      //
-      // (module
-      //  (func $func_any (param funcref anyref)
-      //   (unreachable)
-      //  )
-      //
-      //  (func $extern_any-any (param externref anyref) (result anyref)
-      //   (unreachable)
-      //  )
-      //
-      //  (func $br-if-bad
-      //   (local $bang externref)
-      //   (call $func_any ;; 2. Requires [func, any]
-      //    (ref.null nofunc)
-      //    (block $l (result anyref)
-      //     (call $extern_any-any ;; 1. Requires [extern, any]
-      //      (local.get $bang)
-      //      (br_if $l ;; 3. After join, requires [unreachable, any]
-      //       (ref.null none)
-      //       (i32.const 0)
-      //      )
-      //     )
-      //    )
-      //   )
-      //  )
-      // )
-      //
-      // To fix this, we need to insert an extra basic block encompassing the
-      // liminal space between where the br_if determines it should take the
-      // branch and when control arrives at the branch target. This is when the
-      // extra values are popped off the stack.
-      WASM_UNREACHABLE("TODO");
     } else {
-      // `br` pops everything but the sent value off the stack, so do not
-      // require anything of values on the stack except for that sent value, if
-      // it exists.
-      if (curr->value && curr->value->type.isRef()) {
-        auto type = pop();
-        clearStack();
-        push(type);
-      } else {
-        // No sent value. Do not require anything.
-        clearStack();
-      }
+      // Unconstrained type variable (e.g. drop).
+      assert(std::holds_alternative<Index>(type));
     }
   }
 
-  void visitSwitch(Switch* curr) {
-    // Just like `br`, do not require anything of the values on the stack except
-    // for the sent value, if it exists.
-    if (curr->value && curr->value->type.isRef()) {
-      auto type = pop();
-      clearStack();
-      push(type);
-    } else {
-      clearStack();
+  // Control flow handling. TODO: Perhaps find a way to do this in ChildTyper,
+  // or a helper that extends ChildTyper?
+  void visitBlock(Block* curr) {
+    if (curr->type.isConcrete()) {
+      assert(!curr->list.empty());
+      exprSubs[curr].push_back(curr->list.back());
     }
   }
 
-  template<typename T> void handleCall(T* curr, Type params) {
-    if (curr->type.isRef()) {
-      pop();
-    }
-    for (auto param : params) {
-      // Cannot generalize beyond param types without interprocedural analysis.
-      if (param.isRef()) {
-        push(param);
-      }
+  void visitIf(If* curr) {
+    if (curr->type.isConcrete()) {
+      exprSubs[curr].push_back(curr->ifTrue);
+      exprSubs[curr].push_back(curr->ifFalse);
     }
   }
 
-  void visitCall(Call* curr) {
-    handleCall(curr, wasm.getFunction(curr->target)->getParams());
-  }
-
-  void visitCallIndirect(CallIndirect* curr) {
-    handleCall(curr, curr->heapType.getSignature().params);
+  void visitLoop(Loop* curr) {
+    if (curr->type.isConcrete()) {
+      exprSubs[curr].push_back(curr->body);
+    }
   }
 
-  void visitLocalGet(LocalGet* curr) {
-    if (!curr->type.isRef()) {
-      return;
+  void visitBreak(Break* curr) {
+    if (curr->value) {
+      exprSubs[walker.findBreakTarget(curr->name)].push_back(curr->value);
+      if (curr->type.isConcrete()) {
+        exprSubs[curr].push_back(curr->value);
+      }
     }
-    // Propagate the requirement on the local.get output to the local.
-    updateLocal(curr->index, pop());
   }
 
-  void visitLocalSet(LocalSet* curr) {
-    if (!curr->value->type.isRef()) {
-      return;
+  void visitSwitch(Switch* curr) {
+    if (curr->value) {
+      for (auto name : BranchUtils::getUniqueTargets(curr)) {
+        exprSubs[walker.findBreakTarget(name)].push_back(curr->value);
+      }
     }
-    if (curr->isTee()) {
-      // Same as the local.get.
-      updateLocal(curr->index, pop());
-    }
-    // Propagate the requirement on the local to our input value.
-    push(getLocal(curr->index));
-  }
-
-  void visitGlobalGet(GlobalGet* curr) {
-    if (curr->type.isRef()) {
-      // Cannot generalize globals without interprocedural analysis.
-      pop();
-    }
-  }
-
-  void visitGlobalSet(GlobalSet* curr) {
-    auto type = wasm.getGlobal(curr->name)->type;
-    if (type.isRef()) {
-      // Cannot generalize globals without interprocedural analysis.
-      push(type);
-    }
-  }
-
-  void visitLoad(Load* curr) {}
-  void visitStore(Store* curr) {}
-  void visitAtomicRMW(AtomicRMW* curr) {}
-  void visitAtomicCmpxchg(AtomicCmpxchg* curr) {}
-  void visitAtomicWait(AtomicWait* curr) {}
-  void visitAtomicNotify(AtomicNotify* curr) {}
-  void visitAtomicFence(AtomicFence* curr) {}
-  void visitPause(Pause* curr) {}
-  void visitSIMDExtract(SIMDExtract* curr) {}
-  void visitSIMDReplace(SIMDReplace* curr) {}
-  void visitSIMDShuffle(SIMDShuffle* curr) {}
-  void visitSIMDTernary(SIMDTernary* curr) {}
-  void visitSIMDShift(SIMDShift* curr) {}
-  void visitSIMDLoad(SIMDLoad* curr) {}
-  void visitSIMDLoadStoreLane(SIMDLoadStoreLane* curr) {}
-  void visitMemoryInit(MemoryInit* curr) {}
-  void visitDataDrop(DataDrop* curr) {}
-  void visitMemoryCopy(MemoryCopy* curr) {}
-  void visitMemoryFill(MemoryFill* curr) {}
-  void visitConst(Const* curr) {}
-  void visitUnary(Unary* curr) {}
-  void visitBinary(Binary* curr) {}
-  void visitWideIntAddSub(WideIntAddSub* curr) {}
-  void visitWideIntMul(WideIntMul* curr) {}
+  }
 
   void visitSelect(Select* curr) {
-    if (curr->type.isRef()) {
-      // The inputs may be as general as the output.
-      auto type = pop();
-      push(type);
-      push(type);
+    if (curr->type.isConcrete()) {
+      exprSubs[curr].push_back(curr->ifTrue);
+      exprSubs[curr].push_back(curr->ifFalse);
     }
   }
 
-  void visitDrop(Drop* curr) {
-    if (curr->type.isRef()) {
-      pop();
+  void visitTry(Try* curr) {
+    exprSubs[curr].push_back(curr->body);
+    for (auto* body : curr->catchBodies) {
+      exprSubs[curr].push_back(body);
     }
   }
 
-  // This is handled by propagating the stack backward from the exit block.
-  void visitReturn(Return* curr) {}
-
-  void visitMemorySize(MemorySize* curr) {}
-  void visitMemoryGrow(MemoryGrow* curr) {}
-
-  void visitUnreachable(Unreachable* curr) {
-    // Require nothing about values flowing into an unreachable.
-    clearStack();
-  }
-
-  void visitPop(Pop* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitRefNull(RefNull* curr) { pop(); }
-
-  void visitRefIsNull(RefIsNull* curr) {
-    // ref.is_null works on any reference type, so do not impose any
-    // constraints. We still need to push something, so push bottom.
-    push(Type::none);
-  }
-
-  void visitRefFunc(RefFunc* curr) { pop(); }
-
-  void visitRefEq(RefEq* curr) {
-    // Both operands must be eqref.
-    auto eqref = Type(HeapType::eq, Nullable);
-    push(eqref);
-    push(eqref);
-  }
-
-  void visitTableGet(TableGet* curr) {
-    // Cannot generalize table types yet.
-    pop();
-  }
-
-  void visitTableSet(TableSet* curr) {
-    // Cannot generalize table types yet.
-    push(wasm.getTable(curr->table)->type);
-  }
-
-  void visitTableSize(TableSize* curr) {}
-  void visitTableGrow(TableGrow* curr) {}
+  void visitTryTable(TryTable* curr) { exprSubs[curr].push_back(curr->body); }
 
-  void visitTableFill(TableFill* curr) {
-    // Cannot generalize table types yet.
-    push(wasm.getTable(curr->table)->type);
+  void visitLocalSet(LocalSet* curr) {
+    auto localType = func->getLocalType(curr->index);
+    if (func->isParam(curr->index)) {
+      // Parameters have fixed types.
+      addConstraint(curr->value, localType);
+    } else if (localType.isRef()) {
+      localSetValues[curr->index].push_back(curr->value);
+    }
   }
 
-  void visitTableCopy(TableCopy* curr) {
-    // Cannot generalize table types yet.
+  void visitRefAs(RefAs* curr) {
+    // All RefAs ops have output types that depend on their input types, and we
+    // will refinalize them if their input types generalize. Propagate any
+    // requirement on the output back to the input.
+    exprSubs[curr].push_back(curr->value);
   }
 
-  void visitTableInit(TableInit* curr) {}
-
-  void visitElemDrop(ElemDrop* curr) {}
-
-  void visitTry(Try* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitTryTable(TryTable* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitThrow(Throw* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitRethrow(Rethrow* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitThrowRef(ThrowRef* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitTupleMake(TupleMake* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitTupleExtract(TupleExtract* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitRefI31(RefI31* curr) { pop(); }
-  void visitI31Get(I31Get* curr) { push(Type(HeapType::i31, Nullable)); }
-
-  void visitCallRef(CallRef* curr) {
-    auto sigType = curr->target->type.getHeapType();
-    if (sigType.isBottom()) {
-      // This will be emitted as an unreachable, so impose no requirements on
-      // the arguments, but do require that the target continue to have bottom
-      // type.
-      clearStack();
-      push(Type(HeapType::nofunc, Nullable));
+  void visitBrOn(BrOn* curr) {
+    // Note immediate constraints (including descriptor constraints).
+    Super::visitBrOn(curr);
+    if (curr->desc && !curr->desc->type.isStruct()) {
       return;
     }
-
-    auto sig = sigType.getSignature();
-    auto numParams = sig.params.size();
-    std::optional<Type> resultReq;
-    if (sig.results.isRef()) {
-      resultReq = pop();
-    }
-
-    // We have a choice here: We can either try to generalize the type of the
-    // incoming function reference or the type of the incoming function
-    // arguments. Because function parameters are contravariant, generalizing
-    // the function type inhibits generalizing the arguments and vice versa.
-    // Attempt to split the difference by generalizing the function type only as
-    // much as we can without imposing stronger requirements on the arguments.
-    auto targetReq = sigType;
-    while (true) {
-      auto candidateReq = targetReq.getDeclaredSuperType();
-      if (!candidateReq) {
-        // There is no more general type we can require.
+    switch (curr->op) {
+      case BrOnNull:
+        // If we do not branch, we flow out the non-null input.
+        if (curr->type.isRef()) {
+          addConstraint(curr->ref, curr->type.with(Nullable));
+        }
         break;
-      }
-
-      auto candidateSig = candidateReq->getSignature();
-
-      if (resultReq && *resultReq != candidateSig.results &&
-          Type::isSubType(*resultReq, candidateSig.results)) {
-        // Generalizing further would violate the requirement on the result
-        // type.
+      case BrOnNonNull: {
+        // If we branch, we send the non-null input to the target.
+        auto* breakTarget = walker.findBreakTarget(curr->name);
+        if (breakTarget->type.isRef()) {
+          addConstraint(curr->ref, breakTarget->type.with(Nullable));
+        }
         break;
       }
-
-      for (size_t i = 0; i < numParams; ++i) {
-        if (candidateSig.params[i] != sig.params[i]) {
-          // Generalizing further would restrict how much we could generalize
-          // this argument, so we choose not to generalize further.
-          // TODO: Experiment with making the opposite choice.
-          goto done;
+      case BrOnCast:
+      case BrOnCastDescEq:
+        // If we do not branch, we flow out the original input when the cast
+        // fails. If the cast type is nullable then nulls take the branch, so
+        // the fallthrough value is made non-nullable.
+        if (curr->type.isRef()) {
+          auto type = curr->type;
+          if (curr->castType.isNullableRef()) {
+            type = type.with(Nullable);
+          }
+          addConstraint(curr->ref, type);
         }
-      }
-
-      // We can generalize.
-      targetReq = *candidateReq;
-    }
-  done:
-
-    // Push the new requirements for the parameters.
-    auto targetSig = targetReq.getSignature();
-    for (auto param : targetSig.params) {
-      if (param.isRef()) {
-        push(param);
+        break;
+      case BrOnCastFail:
+      case BrOnCastDescEqFail: {
+        // We send the original input along when the cast fails, so the input
+        // must be sendable to the target. If the cast type is nullable then
+        // nulls do not fail the cast, so the sent value is non-nullable.
+        auto* breakTarget = walker.findBreakTarget(curr->name);
+        if (breakTarget->type.isRef()) {
+          auto type = breakTarget->type;
+          if (curr->castType.isNullableRef()) {
+            type = type.with(Nullable);
+          }
+          addConstraint(curr->ref, type);
+        }
+        break;
       }
     }
-    // The new requirement for the call target.
-    push(Type(targetReq, Nullable));
-  }
-
-  void visitRefTest(RefTest* curr) {
-    // Do not require anything of the input.
-    push(Type::none);
   }
 
-  void visitRefCast(RefCast* curr) {
-    // We do not have to require anything of the input, and not doing so might
-    // allow us generalize the output of previous casts enough that they can be
-    // optimized out. On the other hand, allowing the input to this cast to be
-    // generalized might prevent us from optimizing this cast out, so this is
-    // not a clear-cut decision. For now, leave the input unconstrained for
-    // simplicity. TODO: Experiment with requiring the LUB of the output
-    // requirement and the current input instead.
-    pop();
-    push(Type::none);
+  void visitPublish(Publish* curr) {
+    // TODO: Propagate output constraints back to the input, like RefAs.
+    addConstraint(curr->ref, curr->ref->type);
   }
 
-  void visitRefGetDesc(RefGetDesc* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitBrOn(BrOn* curr) {
-    // Like br_if, these instructions do different things to the stack depending
-    // on whether the branch is taken or not. For branches that drop the tested
-    // value, we need to push a requirement for that value, but for branches
-    // that propagate the tested value, we need to propagate the existing
-    // requirement instead. Like br_if, these instructions will require extra
-    // basic blocks on the branches that drop values.
-    WASM_UNREACHABLE("TODO");
-  }
-
-  void visitStructNew(StructNew* curr) {
-    // We cannot yet generalize allocations. Push requirements for the types
-    // needed to initialize the struct.
-    pop();
-    if (!curr->isWithDefault()) {
-      auto type = curr->type.getHeapType();
-      for (const auto& field : type.getStruct().fields) {
-        if (field.type.isRef()) {
-          push(field.type);
-        }
-      }
+  void visitTupleMake(TupleMake* curr) {
+    // TODO: Track constraints on tuple elements.
+    for (auto* op : curr->operands) {
+      addConstraint(op, op->type);
     }
   }
 
-  HeapType
-  generalizeStructType(HeapType type,
-                       Index index,
-                       std::optional<Type> reqFieldType = std::nullopt) {
-    // Find the most general struct type for which this access could be valid,
-    // i.e. the most general supertype that still has a field at the given index
-    // where the field is a subtype of the required type, if any.
-    while (true) {
-      auto candidateType = type.getDeclaredSuperType();
-      if (!candidateType) {
-        // Cannot get any more general.
-        break;
-      }
-      const auto& candidateFields = candidateType->getStruct().fields;
-      if (candidateFields.size() <= index) {
-        // Cannot get any more general and still have a field at the necessary
-        // index.
-        break;
-      }
-      if (reqFieldType) {
-        auto candidateFieldType = candidateFields[index].type;
-        if (candidateFieldType != *reqFieldType &&
-            Type::isSubType(*reqFieldType, candidateFieldType)) {
-          // Cannot generalize without violating the requirements on the field.
-          break;
-        }
-      }
-      type = *candidateType;
+  void visitCallRef(CallRef* curr) {
+    if (!curr->target->type.isSignature()) {
+      Super::visitCallRef(curr);
+      return;
+    }
+    auto sigType = curr->target->type.getHeapType();
+    std::optional<Type> resultReq;
+    if (curr->isReturn) {
+      resultReq = func->getResults();
     }
-    return type;
+    auto generalized = generalizeCallRefTarget(sigType, resultReq);
+    Super::visitCallRef(curr, generalized);
   }
 
   void visitStructGet(StructGet* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
+    if (!curr->ref->type.isStruct()) {
+      Super::visitStructGet(curr);
       return;
     }
-    std::optional<Type> reqFieldType;
-    if (curr->type.isRef()) {
-      reqFieldType = pop();
-    }
-    auto generalized = generalizeStructType(type, curr->index, reqFieldType);
-    push(Type(generalized, Nullable));
+    auto generalized =
+      generalizeStructType(curr->ref->type.getHeapType(), curr->index);
+    Super::visitStructGet(curr, generalized);
   }
 
   void visitStructSet(StructSet* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
-      if (curr->value->type.isRef()) {
-        push(Type::none);
-      }
+    if (!curr->ref->type.isStruct()) {
+      Super::visitStructSet(curr);
       return;
     }
-    auto generalized = generalizeStructType(type, curr->index);
-    push(Type(generalized, Nullable));
-    auto fieldType = generalized.getStruct().fields[curr->index].type;
-    if (fieldType.isRef()) {
-      push(fieldType);
-    }
-  }
-
-  void visitStructRMW(StructRMW* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitStructCmpxchg(StructCmpxchg* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitStructWait(StructWait* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitWaitqueueNew(WaitqueueNew* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitWaitqueueNotify(WaitqueueNotify* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitPublish(Publish* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitArrayNew(ArrayNew* curr) {
-    // We cannot yet generalize allocations. Push a requirement for the
-    // reference type needed to initialize the array, if any.
-    pop();
-    if (!curr->isWithDefault()) {
-      auto type = curr->type.getHeapType();
-      auto fieldType = type.getArray().element.type;
-      if (fieldType.isRef()) {
-        push(fieldType);
-      }
-    }
-  }
-
-  void visitArrayNewData(ArrayNewData* curr) {
-    // We cannot yet generalize allocations.
-    pop();
-  }
-
-  void visitArrayNewElem(ArrayNewElem* curr) {
-    // We cannot yet generalize allocations or tables.
-    pop();
-  }
-
-  void visitArrayNewFixed(ArrayNewFixed* curr) {
-    // We cannot yet generalize allocations. Push a requirements for the
-    // reference type needed to initialize the array, if any.
-    pop();
-    auto type = curr->type.getHeapType();
-    auto fieldType = type.getArray().element.type;
-    if (fieldType.isRef()) {
-      for (size_t i = 0, n = curr->values.size(); i < n; ++i) {
-        push(fieldType);
-      }
-    }
-  }
-
-  void visitArrayRMW(ArrayRMW* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitArrayCmpxchg(ArrayCmpxchg* curr) { WASM_UNREACHABLE("TODO"); }
-
-  HeapType
-  generalizeArrayType(HeapType type,
-                      std::optional<Type> reqFieldType = std::nullopt) {
-    // Find the most general array type for which this access could be valid.
-    while (true) {
-      auto candidateType = type.getDeclaredSuperType();
-      if (!candidateType) {
-        // Cannot get any more general.
-        break;
-      }
-      if (reqFieldType) {
-        auto candidateFieldType = candidateType->getArray().element.type;
-        if (candidateFieldType != *reqFieldType &&
-            Type::isSubType(*reqFieldType, candidateFieldType)) {
-          // Cannot generalize without violating requirements on the field.
-          break;
-        }
-      }
-      type = *candidateType;
-    }
-    return type;
+    auto generalized =
+      generalizeStructType(curr->ref->type.getHeapType(), curr->index);
+    Super::visitStructSet(curr, generalized);
   }
 
   void visitArrayGet(ArrayGet* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
+    if (!curr->ref->type.isArray()) {
+      Super::visitArrayGet(curr);
       return;
     }
-    std::optional<Type> reqFieldType;
-    if (curr->type.isRef()) {
-      reqFieldType = pop();
-    }
-    auto generalized = generalizeArrayType(type, reqFieldType);
-    push(Type(generalized, Nullable));
+    auto generalized = generalizeArrayType(curr->ref->type.getHeapType());
+    Super::visitArrayGet(curr, generalized);
   }
 
   void visitArraySet(ArraySet* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
-      if (curr->value->type.isRef()) {
-        push(Type::none);
-      }
+    if (!curr->ref->type.isArray()) {
+      Super::visitArraySet(curr);
       return;
     }
-    auto generalized = generalizeArrayType(type);
-    push(Type(generalized, Nullable));
-    auto elemType = generalized.getArray().element.type;
-    if (elemType.isRef()) {
-      push(elemType);
-    }
-  }
-
-  void visitArrayLoad(ArrayLoad* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitArrayStore(ArrayStore* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitArrayLen(ArrayLen* curr) {
-    // The input must be an array.
-    push(Type(HeapType::array, Nullable));
+    auto generalized = generalizeArrayType(curr->ref->type.getHeapType());
+    Super::visitArraySet(curr, generalized);
   }
 
   void visitArrayCopy(ArrayCopy* curr) {
-    auto destType = curr->destRef->type.getHeapType();
-    auto srcType = curr->srcRef->type.getHeapType();
-    if (destType.isBottom() || srcType.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the bottom refs remain bottom.
-      clearStack();
-      auto nullref = Type(HeapType::none, Nullable);
-      push(destType.isBottom() ? nullref : Type::none);
-      push(srcType.isBottom() ? nullref : Type::none);
+    if (!curr->destRef->type.isArray() || !curr->srcRef->type.isArray()) {
+      Super::visitArrayCopy(curr);
       return;
     }
-    // Model the copy as a get + set.
-    ArraySet set;
-    set.ref = curr->destRef;
-    set.index = nullptr;
-    set.value = nullptr;
-    visitArraySet(&set);
-    ArrayGet get;
-    get.ref = curr->srcRef;
-    get.index = nullptr;
-    get.type = srcType.getArray().element.type;
-    visitArrayGet(&get);
+    auto destGen = generalizeArrayType(curr->destRef->type.getHeapType());
+    auto elemType = destGen.getArray().element.type;
+    std::optional<Type> reqElemType;
+    if (elemType.isRef()) {
+      reqElemType = elemType;
+    }
+    auto srcGen =
+      generalizeArrayType(curr->srcRef->type.getHeapType(), reqElemType);
+    Super::visitArrayCopy(curr, destGen, srcGen);
   }
 
   void visitArrayFill(ArrayFill* curr) {
-    // Model the fill as a set.
-    ArraySet set;
-    set.ref = curr->ref;
-    set.value = curr->value;
-    visitArraySet(&set);
+    if (!curr->ref->type.isArray()) {
+      Super::visitArrayFill(curr);
+      return;
+    }
+    auto generalized = generalizeArrayType(curr->ref->type.getHeapType());
+    Super::visitArrayFill(curr, generalized);
   }
 
   void visitArrayInitData(ArrayInitData* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
+    if (!curr->ref->type.isArray()) {
+      Super::visitArrayInitData(curr);
       return;
     }
-    auto generalized = generalizeArrayType(type);
-    push(Type(generalized, Nullable));
+    auto generalized = generalizeArrayType(curr->ref->type.getHeapType());
+    Super::visitArrayInitData(curr, generalized);
   }
 
   void visitArrayInitElem(ArrayInitElem* curr) {
-    auto type = curr->ref->type.getHeapType();
-    if (type.isBottom()) {
-      // This will be emitted as unreachable. Do not require anything of the
-      // input, except that the ref remain bottom.
-      clearStack();
-      push(Type(HeapType::none, Nullable));
+    if (!curr->ref->type.isArray()) {
+      Super::visitArrayInitElem(curr);
       return;
     }
-    auto generalized = generalizeArrayType(type);
-    push(Type(generalized, Nullable));
-    // Cannot yet generalize table types.
-  }
-
-  void visitRefAs(RefAs* curr) {
-    auto type = pop();
-    if (type == Type::none) {
-      // No downstream requirement, so no requirement for the input either.
-      push(Type::none);
-      return;
+    auto generalized = generalizeArrayType(curr->ref->type.getHeapType());
+    Super::visitArrayInitElem(curr, generalized);
+  }
+
+  void propagate() {
+    while (!worklist.empty()) {
+      auto item = worklist.back();
+      worklist.pop_back();
+      if (auto* exprPtr = std::get_if<Expression*>(&item)) {
+        auto* expr = *exprPtr;
+        auto type = exprGLBs[expr].getGLB();
+        if (auto* get = expr->dynCast<LocalGet>()) {
+          addConstraint(get->index, type);
+        } else if (auto* set = expr->dynCast<LocalSet>()) {
+          if (set->isTee()) {
+            addConstraint(set->index, type);
+          }
+        } else if (auto* as = expr->dynCast<RefAs>()) {
+          auto share = type.getHeapType().getShared();
+          switch (as->op) {
+            case RefAsNonNull:
+              type = type.with(Nullable);
+              break;
+            case AnyConvertExtern:
+              type =
+                Type(HeapTypes::ext.getBasic(share), type.getNullability());
+              break;
+            case ExternConvertAny:
+              type =
+                Type(HeapTypes::any.getBasic(share), type.getNullability());
+              break;
+          }
+        } else if (auto* get = expr->dynCast<StructGet>()) {
+          if (get->ref->type.isStruct()) {
+            auto generalized = generalizeStructType(
+              get->ref->type.getHeapType(), get->index, type);
+            addConstraint(get->ref, Type(generalized, Nullable));
+          }
+        } else if (auto* get = expr->dynCast<ArrayGet>()) {
+          if (get->ref->type.isArray()) {
+            auto generalized =
+              generalizeArrayType(get->ref->type.getHeapType(), type);
+            addConstraint(get->ref, Type(generalized, Nullable));
+          }
+        } else if (auto* call = expr->dynCast<CallRef>()) {
+          if (call->target->type.isSignature()) {
+            auto generalized =
+              generalizeCallRefTarget(call->target->type.getHeapType(), type);
+            addConstraint(call->target, Type(generalized, Nullable));
+          }
+        }
+        if (auto it = exprSubs.find(expr); it != exprSubs.end()) {
+          for (auto* sub : it->second) {
+            addConstraint(sub, type);
+          }
+        }
+      } else {
+        auto local = std::get<Index>(item);
+        auto type = localGLBs[local].getGLB();
+        for (auto* val : localSetValues[local]) {
+          addConstraint(val, type);
+        }
+      }
     }
-    switch (curr->op) {
-      case RefAsNonNull:
-        push(Type(type.getHeapType(), Nullable));
-        return;
-      case AnyConvertExtern:
-        push(Type(HeapType::ext, type.getNullability()));
-        return;
-      case ExternConvertAny:
-        push(Type(HeapType::any, type.getNullability()));
-        return;
-    }
-    WASM_UNREACHABLE("unexpected op");
-  }
-
-  void visitStringNew(StringNew* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringConst(StringConst* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringMeasure(StringMeasure* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringEncode(StringEncode* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringConcat(StringConcat* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringEq(StringEq* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringTest(StringTest* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringWTF16Get(StringWTF16Get* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStringSliceWTF(StringSliceWTF* curr) { WASM_UNREACHABLE("TODO"); }
-
-  void visitContNew(ContNew* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitContBind(ContBind* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitSuspend(Suspend* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitResume(Resume* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitResumeThrow(ResumeThrow* curr) { WASM_UNREACHABLE("TODO"); }
-  void visitStackSwitch(StackSwitch* curr) { WASM_UNREACHABLE("TODO"); }
+  }
 };
 
 struct TypeGeneralizing : WalkerPass<PostWalker<TypeGeneralizing>> {
@@ -926,23 +541,35 @@ struct TypeGeneralizing : WalkerPass<PostWalker<TypeGeneralizing>> {
 
   void runOnFunction(Module* wasm, Function* func) override {
     // First, remove unreachable code. If we didn't, the unreachable code could
-    // become invalid after this optimization because we do not materialize or
-    // analyze unreachable blocks.
+    // become invalid after this optimization because ChildTyper does not
+    // constrain unreachable expressions in all cases.
     PassRunner runner(getPassRunner());
     runner.add("dce");
     runner.runOnFunction(func);
 
-    auto cfg = CFG::fromFunction(func, wasm);
-    DBG(cfg.print(std::cerr));
-    TransferFn txfn(*wasm, func, cfg);
-    MonotoneCFGAnalyzer analyzer(txfn.lattice, txfn, cfg);
-    analyzer.evaluate();
+    Generalizer generalizer(*wasm, func);
+    generalizer.walk();
+    generalizer.propagate();
 
     // Optimize local types. TODO: Optimize casts as well.
-    localTypes = txfn.lattice.getLocals();
+    auto numLocals = func->getNumLocals();
     auto numParams = func->getNumParams();
-    for (Index i = numParams; i < localTypes.size(); ++i) {
-      func->vars[i - numParams] = localTypes[i];
+    localTypes.resize(numLocals);
+    for (Index i = 0; i < numParams; ++i) {
+      localTypes[i] = func->getLocalType(i);
+    }
+    for (Index i = numParams; i < numLocals; ++i) {
+      auto origType = func->getLocalType(i);
+      if (origType.isRef()) {
+        auto& glb = generalizer.localGLBs[i];
+        auto newType = glb.noted()
+                         ? glb.getGLB()
+                         : Type(origType.getHeapType().getTop(), Nullable);
+        localTypes[i] = newType;
+        func->vars[i - numParams] = newType;
+      } else {
+        localTypes[i] = origType;
+      }
     }
 
     // Update gets and sets accordingly.
diff --git a/test/lit/passes/type-generalizing-strings.wast b/test/lit/passes/type-generalizing-strings.wast
new file mode 100644
index 00000000000..9917645712e
--- /dev/null
+++ b/test/lit/passes/type-generalizing-strings.wast
@@ -0,0 +1,262 @@
+;; NOTE: Assertions have been generated by update_lit_checks.py --all-items and should not be edited.
+
+;; RUN: foreach %s %t wasm-opt --experimental-type-generalizing -all -S -o - | filecheck %s
+
+(module
+ ;; CHECK:      (type $0 (func))
+
+ ;; CHECK:      (type $1 (func (result stringref)))
+
+ ;; CHECK:      (type $i8-array (array (mut i8)))
+ (type $i8-array (array (mut i8)))
+ ;; CHECK:      (type $i16-array (array (mut i16)))
+ (type $i16-array (array (mut i16)))
+
+ ;; CHECK:      (type $4 (func (result externref)))
+
+ ;; CHECK:      (type $5 (func (result i32)))
+
+ ;; CHECK:      (func $string-new-utf8 (type $1) (result stringref)
+ ;; CHECK-NEXT:  (local $arr (ref null $i8-array))
+ ;; CHECK-NEXT:  (string.new_lossy_utf8_array
+ ;; CHECK-NEXT:   (local.get $arr)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-new-utf8 (result stringref)
+  (local $arr nullref)
+  ;; Require typeof($arr) <: (ref null $i8-array).
+  (string.new_lossy_utf8_array
+   (local.get $arr)
+   (i32.const 0)
+   (i32.const 0)
+  )
+ )
+
+ ;; CHECK:      (func $string-new-wtf16 (type $1) (result stringref)
+ ;; CHECK-NEXT:  (local $arr (ref null $i16-array))
+ ;; CHECK-NEXT:  (string.new_wtf16_array
+ ;; CHECK-NEXT:   (local.get $arr)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-new-wtf16 (result stringref)
+  (local $arr nullref)
+  ;; Require typeof($arr) <: (ref null $i16-array).
+  (string.new_wtf16_array
+   (local.get $arr)
+   (i32.const 0)
+   (i32.const 0)
+  )
+ )
+
+ ;; CHECK:      (func $string-from-code-point-and-const (type $0)
+ ;; CHECK-NEXT:  (local $s1 externref)
+ ;; CHECK-NEXT:  (local $s2 externref)
+ ;; CHECK-NEXT:  (local.set $s1
+ ;; CHECK-NEXT:   (string.from_code_point
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (local.set $s2
+ ;; CHECK-NEXT:   (string.const "hello")
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-from-code-point-and-const
+  (local $s1 stringref)
+  (local $s2 stringref)
+  ;; No constraints on $s1 or $s2, so they generalize to externref.
+  (local.set $s1
+   (string.from_code_point
+    (i32.const 0)
+   )
+  )
+  (local.set $s2
+   (string.const "hello")
+  )
+ )
+
+ ;; CHECK:      (func $string-measure (type $0)
+ ;; CHECK-NEXT:  (local $s1 stringref)
+ ;; CHECK-NEXT:  (local $s2 stringref)
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.measure_utf8
+ ;; CHECK-NEXT:    (local.get $s1)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.measure_wtf16
+ ;; CHECK-NEXT:    (local.get $s2)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-measure
+  (local $s1 nullexternref)
+  (local $s2 nullexternref)
+  ;; Require typeof($s1) <: stringref and typeof($s2) <: stringref.
+  (drop
+   (string.measure_utf8
+    (local.get $s1)
+   )
+  )
+  (drop
+   (string.measure_wtf16
+    (local.get $s2)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $string-encode-utf8 (type $0)
+ ;; CHECK-NEXT:  (local $s stringref)
+ ;; CHECK-NEXT:  (local $arr (ref null $i8-array))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.encode_lossy_utf8_array
+ ;; CHECK-NEXT:    (local.get $s)
+ ;; CHECK-NEXT:    (local.get $arr)
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-encode-utf8
+  (local $s nullexternref)
+  (local $arr nullref)
+  ;; Require typeof($s) <: stringref and typeof($arr) <: (ref null $i8-array).
+  (drop
+   (string.encode_lossy_utf8_array
+    (local.get $s)
+    (local.get $arr)
+    (i32.const 0)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $string-encode-wtf16 (type $0)
+ ;; CHECK-NEXT:  (local $s stringref)
+ ;; CHECK-NEXT:  (local $arr (ref null $i16-array))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.encode_wtf16_array
+ ;; CHECK-NEXT:    (local.get $s)
+ ;; CHECK-NEXT:    (local.get $arr)
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-encode-wtf16
+  (local $s nullexternref)
+  (local $arr nullref)
+  ;; Require typeof($s) <: stringref and typeof($arr) <: (ref null $i16-array).
+  (drop
+   (string.encode_wtf16_array
+    (local.get $s)
+    (local.get $arr)
+    (i32.const 0)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $string-concat (type $4) (result externref)
+ ;; CHECK-NEXT:  (local $s1 stringref)
+ ;; CHECK-NEXT:  (local $s2 stringref)
+ ;; CHECK-NEXT:  (string.concat
+ ;; CHECK-NEXT:   (local.get $s1)
+ ;; CHECK-NEXT:   (local.get $s2)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-concat (result externref)
+  (local $s1 nullexternref)
+  (local $s2 nullexternref)
+  ;; Require typeof($s1) <: stringref and typeof($s2) <: stringref.
+  (string.concat
+   (local.get $s1)
+   (local.get $s2)
+  )
+ )
+
+ ;; CHECK:      (func $string-eq (type $0)
+ ;; CHECK-NEXT:  (local $s1 stringref)
+ ;; CHECK-NEXT:  (local $s2 stringref)
+ ;; CHECK-NEXT:  (local $s3 stringref)
+ ;; CHECK-NEXT:  (local $s4 stringref)
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.eq
+ ;; CHECK-NEXT:    (local.get $s1)
+ ;; CHECK-NEXT:    (local.get $s2)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (string.compare
+ ;; CHECK-NEXT:    (local.get $s3)
+ ;; CHECK-NEXT:    (local.get $s4)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-eq
+  (local $s1 nullexternref)
+  (local $s2 nullexternref)
+  (local $s3 nullexternref)
+  (local $s4 nullexternref)
+  ;; Require all operands <: stringref.
+  (drop
+   (string.eq
+    (local.get $s1)
+    (local.get $s2)
+   )
+  )
+  (drop
+   (string.compare
+    (local.get $s3)
+    (local.get $s4)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $string-test (type $5) (result i32)
+ ;; CHECK-NEXT:  (local $s externref)
+ ;; CHECK-NEXT:  (string.test
+ ;; CHECK-NEXT:   (local.get $s)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-test (result i32)
+  (local $s stringref)
+  ;; Require typeof($s) <: externref.
+  (string.test
+   (local.get $s)
+  )
+ )
+
+ ;; CHECK:      (func $string-wtf16-get (type $5) (result i32)
+ ;; CHECK-NEXT:  (local $s stringref)
+ ;; CHECK-NEXT:  (stringview_wtf16.get_codeunit
+ ;; CHECK-NEXT:   (local.get $s)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-wtf16-get (result i32)
+  (local $s nullexternref)
+  ;; Require typeof($s) <: stringref.
+  (stringview_wtf16.get_codeunit
+   (local.get $s)
+   (i32.const 0)
+  )
+ )
+
+ ;; CHECK:      (func $string-slice-wtf (type $4) (result externref)
+ ;; CHECK-NEXT:  (local $s stringref)
+ ;; CHECK-NEXT:  (stringview_wtf16.slice
+ ;; CHECK-NEXT:   (local.get $s)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $string-slice-wtf (result externref)
+  (local $s nullexternref)
+  ;; Require typeof($s) <: stringref.
+  (stringview_wtf16.slice
+   (local.get $s)
+   (i32.const 0)
+   (i32.const 0)
+  )
+ )
+)
diff --git a/test/lit/passes/type-generalizing.wast b/test/lit/passes/type-generalizing.wast
index c9a1c2f9326..948117c3cc0 100644
--- a/test/lit/passes/type-generalizing.wast
+++ b/test/lit/passes/type-generalizing.wast
@@ -913,7 +913,7 @@
 
  ;; CHECK:      (func $call-ref-impossible (type $0) (result eqref)
  ;; CHECK-NEXT:  (local $f nullfuncref)
- ;; CHECK-NEXT:  (local $arg anyref)
+ ;; CHECK-NEXT:  (local $arg i31ref)
  ;; CHECK-NEXT:  (block ;; (replaces unreachable CallRef we can't emit)
  ;; CHECK-NEXT:   (drop
  ;; CHECK-NEXT:    (local.get $arg)
@@ -929,6 +929,8 @@
   (local $arg i31ref)
   ;; Require that typeof($f) <: nullref, but do not constrain $arg because the
   ;; call_ref will not be reached.
+  ;; TODO: for now this keeps the $arg unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (call_ref $bot
    (local.get $arg)
    (local.get $f)
@@ -1099,7 +1101,7 @@
 
  ;; CHECK:      (func $struct-set-impossible (type $3)
  ;; CHECK-NEXT:  (local $ref nullref)
- ;; CHECK-NEXT:  (local $val anyref)
+ ;; CHECK-NEXT:  (local $val nullref)
  ;; CHECK-NEXT:  (block ;; (replaces unreachable StructSet we can't emit)
  ;; CHECK-NEXT:   (drop
  ;; CHECK-NEXT:    (local.get $ref)
@@ -1114,6 +1116,8 @@
   (local $ref nullref)
   (local $val nullref)
   ;; Require that typeof($ref) <: nullref, but do not constrain $val.
+  ;; TODO: for now this keeps the type unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (struct.set $bot 0
    (local.get $ref)
    (local.get $val)
@@ -1138,6 +1142,7 @@
  (type $sub (sub $super (array (field i31ref))))
 
  (type $super-mut (sub (array (field (mut eqref)))))
+ ;; CHECK:      (type $sub-mut (sub $super-mut (array (mut eqref))))
  (type $sub-mut (sub $super-mut (array (field (mut eqref)))))
 
  (type $bytes (sub (array i8)))
@@ -1287,7 +1292,7 @@
 
  ;; CHECK:      (func $array-set-impossible (type $0)
  ;; CHECK-NEXT:  (local $ref nullref)
- ;; CHECK-NEXT:  (local $val anyref)
+ ;; CHECK-NEXT:  (local $val i31ref)
  ;; CHECK-NEXT:  (block ;; (replaces unreachable ArraySet we can't emit)
  ;; CHECK-NEXT:   (drop
  ;; CHECK-NEXT:    (local.get $ref)
@@ -1305,6 +1310,8 @@
   (local $ref nullref)
   (local $val i31ref)
   ;; Require that typeof($ref) <: nullref and do not constrain $ref.
+  ;; TODO: for now this keeps the type unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (array.set $sub-mut
    (local.get $ref)
    (i32.const 0)
@@ -1381,7 +1388,7 @@
 
  ;; CHECK:      (func $array-copy-impossible-dest (type $0)
  ;; CHECK-NEXT:  (local $dest nullref)
- ;; CHECK-NEXT:  (local $src anyref)
+ ;; CHECK-NEXT:  (local $src (ref null $sub))
  ;; CHECK-NEXT:  (block ;; (replaces unreachable ArrayCopy we can't emit)
  ;; CHECK-NEXT:   (drop
  ;; CHECK-NEXT:    (local.get $dest)
@@ -1406,6 +1413,8 @@
   (local $dest nullref)
   (local $src (ref null $sub))
   ;; Require that typeof($dest) <: nullref but do not constrain $src.
+  ;; TODO: for now this keeps $src's type unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (array.copy $sub-mut $sub
    (local.get $dest)
    (i32.const 0)
@@ -1416,7 +1425,7 @@
  )
 
  ;; CHECK:      (func $array-copy-impossible-src (type $0)
- ;; CHECK-NEXT:  (local $dest anyref)
+ ;; CHECK-NEXT:  (local $dest (ref null $sub-mut))
  ;; CHECK-NEXT:  (local $src nullref)
  ;; CHECK-NEXT:  (block ;; (replaces unreachable ArrayCopy we can't emit)
  ;; CHECK-NEXT:   (drop
@@ -1442,6 +1451,8 @@
   (local $dest (ref null $sub-mut))
   (local $src nullref)
   ;; Require that typeof($src) <: nullref but do not constrain $dest.
+  ;; TODO: for now this keeps the type unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (array.copy $sub-mut $sub
    (local.get $dest)
    (i32.const 0)
@@ -1512,7 +1523,7 @@
 
  ;; CHECK:      (func $array-fill-impossible (type $0)
  ;; CHECK-NEXT:  (local $ref nullref)
- ;; CHECK-NEXT:  (local $val anyref)
+ ;; CHECK-NEXT:  (local $val i31ref)
  ;; CHECK-NEXT:  (block ;; (replaces unreachable ArrayFill we can't emit)
  ;; CHECK-NEXT:   (drop
  ;; CHECK-NEXT:    (local.get $ref)
@@ -1533,6 +1544,8 @@
   (local $ref nullref)
   (local $val i31ref)
   ;; Require that typeof($ref) <: nullref, but do not constrain $val.
+  ;; TODO: for now this keeps the type unchanged (and is likely not worth
+  ;;       optimizing, as this is dead code)
   (array.fill $sub-mut
    (local.get $ref)
    (i32.const 0)
@@ -1639,3 +1652,993 @@
   )
  )
 )
+
+(module
+ ;; CHECK:      (type $outer-super (sub (struct)))
+ (type $outer-super (sub (struct)))
+ ;; CHECK:      (type $outer-sub (sub $outer-super (struct (field i32))))
+ (type $outer-sub (sub $outer-super (struct (field i32))))
+ ;; CHECK:      (type $inner-super (sub (struct (field (ref $outer-super)))))
+ (type $inner-super (sub (struct (field (ref $outer-super)))))
+ ;; CHECK:      (type $inner-sub (sub $inner-super (struct (field (ref $outer-sub)))))
+ (type $inner-sub (sub $inner-super (struct (field (ref $outer-sub)))))
+
+ ;; CHECK:      (type $4 (func (result i32)))
+
+ ;; CHECK:      (func $struct-get-non-null-field (type $4) (result i32)
+ ;; CHECK-NEXT:  (local $var (ref null $inner-sub))
+ ;; CHECK-NEXT:  (struct.get $outer-sub 0
+ ;; CHECK-NEXT:   (struct.get $inner-sub 0
+ ;; CHECK-NEXT:    (local.get $var)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $struct-get-non-null-field (result i32)
+  (local $var (ref null $inner-sub))
+  ;; The outer struct.get must return an i32, so it cannot be generalized from
+  ;; $outer-sub to $outer-super. That means we cannot generalize the inner
+  ;; struct.get from $inner-sub to $inner-super (which would emit $outer-super).
+  (struct.get $outer-sub 0
+   (struct.get $inner-sub 0
+    (local.get $var)
+   )
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $0 (func (result eqref)))
+
+ ;; CHECK:      (type $1 (func (param eqref anyref)))
+
+ ;; CHECK:      (type $2 (func))
+
+ ;; CHECK:      (type $3 (func (param (ref (shared noextern))) (result (ref null (shared any)))))
+
+ ;; CHECK:      (type $4 (func (param (ref (shared noextern))) (result (ref (shared any)))))
+
+ ;; CHECK:      (type $5 (func (result (ref null (shared extern)))))
+
+ ;; CHECK:      (type $6 (func (result (ref (shared extern)))))
+
+ ;; CHECK:      (table $eq-table 0 0 eqref)
+ (table $eq-table 0 0 eqref)
+
+ ;; CHECK:      (func $br_if (type $1) (param $eq eqref) (param $any anyref)
+ ;; CHECK-NEXT:  (local $var1 eqref)
+ ;; CHECK-NEXT:  (local $var2 eqref)
+ ;; CHECK-NEXT:  (local.set $eq
+ ;; CHECK-NEXT:   (block $l1 (result eqref)
+ ;; CHECK-NEXT:    (local.set $any
+ ;; CHECK-NEXT:     (br_if $l1
+ ;; CHECK-NEXT:      (local.get $var1)
+ ;; CHECK-NEXT:      (i32.const 0)
+ ;; CHECK-NEXT:     )
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:    (unreachable)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (local.set $any
+ ;; CHECK-NEXT:   (block $l2 (result eqref)
+ ;; CHECK-NEXT:    (local.set $eq
+ ;; CHECK-NEXT:     (br_if $l2
+ ;; CHECK-NEXT:      (local.get $var2)
+ ;; CHECK-NEXT:      (i32.const 0)
+ ;; CHECK-NEXT:     )
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:    (unreachable)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $br_if (param $eq eqref) (param $any anyref)
+  (local $var1 i31ref)
+  (local $var2 i31ref)
+  ;; Require typeof($var1) <: eqref from the branch target.
+  (local.set $eq
+   (block $l1 (result i31ref)
+    (local.set $any
+     (br_if $l1
+      (local.get $var1)
+      (i32.const 0)
+     )
+    )
+    (unreachable)
+   )
+  )
+  ;; Require typeof($var2) <: eqref from the value flowing through the br_if.
+  (local.set $any
+   (block $l2 (result i31ref)
+    (local.set $eq
+     (br_if $l2
+      (local.get $var2)
+      (i32.const 0)
+     )
+    )
+    (unreachable)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $return (type $0) (result eqref)
+ ;; CHECK-NEXT:  (local $var eqref)
+ ;; CHECK-NEXT:  (return
+ ;; CHECK-NEXT:   (local.get $var)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $return (result eqref)
+  (local $var i31ref)
+  ;; Require typeof($var) <: eqref.
+  (return
+   (local.get $var)
+  )
+ )
+
+ ;; CHECK:      (func $table-grow (type $2)
+ ;; CHECK-NEXT:  (local $var eqref)
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (table.grow $eq-table
+ ;; CHECK-NEXT:    (local.get $var)
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $table-grow
+  (local $var i31ref)
+  ;; Require typeof($var) <: eqref.
+  (drop
+   (table.grow $eq-table
+    (local.get $var)
+    (i32.const 0)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $any-convert-extern-shared-nullable (type $3) (param $x (ref (shared noextern))) (result (ref null (shared any)))
+ ;; CHECK-NEXT:  (local $var (ref null (shared extern)))
+ ;; CHECK-NEXT:  (local.set $var
+ ;; CHECK-NEXT:   (local.get $x)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (any.convert_extern
+ ;; CHECK-NEXT:   (local.get $var)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $any-convert-extern-shared-nullable (param $x (ref (shared noextern))) (result (ref null (shared any)))
+  (local $var (ref (shared noextern)))
+  (local.set $var
+   (local.get $x)
+  )
+  ;; Require that typeof($var) <: (ref null (shared extern)).
+  (any.convert_extern
+   (local.get $var)
+  )
+ )
+
+ ;; CHECK:      (func $any-convert-extern-shared-non-nullable (type $4) (param $x (ref (shared noextern))) (result (ref (shared any)))
+ ;; CHECK-NEXT:  (local $var (ref (shared extern)))
+ ;; CHECK-NEXT:  (local.set $var
+ ;; CHECK-NEXT:   (local.get $x)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (any.convert_extern
+ ;; CHECK-NEXT:   (local.get $var)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $any-convert-extern-shared-non-nullable (param $x (ref (shared noextern))) (result (ref (shared any)))
+  (local $var (ref (shared noextern)))
+  (local.set $var
+   (local.get $x)
+  )
+  ;; Require that typeof($var) <: (ref (shared extern)).
+  (any.convert_extern
+   (local.get $var)
+  )
+ )
+
+ ;; CHECK:      (func $extern-convert-any-shared-nullable (type $5) (result (ref null (shared extern)))
+ ;; CHECK-NEXT:  (local $var (ref null (shared any)))
+ ;; CHECK-NEXT:  (local.set $var
+ ;; CHECK-NEXT:   (ref.i31_shared
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (extern.convert_any
+ ;; CHECK-NEXT:   (local.get $var)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $extern-convert-any-shared-nullable (result (ref null (shared extern)))
+  (local $var (ref (shared i31)))
+  (local.set $var
+   (ref.i31_shared
+    (i32.const 0)
+   )
+  )
+  ;; Require that typeof($var) <: (ref null (shared any)).
+  (extern.convert_any
+   (local.get $var)
+  )
+ )
+
+ ;; CHECK:      (func $extern-convert-any-shared-non-nullable (type $6) (result (ref (shared extern)))
+ ;; CHECK-NEXT:  (local $var (ref (shared any)))
+ ;; CHECK-NEXT:  (local.set $var
+ ;; CHECK-NEXT:   (ref.i31_shared
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (extern.convert_any
+ ;; CHECK-NEXT:   (local.get $var)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $extern-convert-any-shared-non-nullable (result (ref (shared extern)))
+  (local $var (ref (shared i31)))
+  (local.set $var
+   (ref.i31_shared
+    (i32.const 0)
+   )
+  )
+  ;; Require that typeof($var) <: (ref (shared any)).
+  (extern.convert_any
+   (local.get $var)
+  )
+ )
+
+ ;; CHECK:      (func $publish (type $0) (result eqref)
+ ;; CHECK-NEXT:  (local $var1 i31ref)
+ ;; CHECK-NEXT:  (local $var2 i31ref)
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (publish
+ ;; CHECK-NEXT:    (local.get $var1)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (publish
+ ;; CHECK-NEXT:   (local.get $var2)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $publish (result eqref)
+  (local $var1 i31ref)
+  (local $var2 i31ref)
+  ;; No constraint on $var1 because the publish is dropped.
+  ;; TODO
+  (drop
+   (publish
+    (local.get $var1)
+   )
+  )
+  ;; Require that typeof($var2) <: eqref through the publish.
+  ;; TODO
+  (publish
+   (local.get $var2)
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $top (sub (func (param i31ref) (result anyref))))
+ (type $top (sub (func (param i31ref) (result anyref))))
+ ;; CHECK:      (type $mid (sub $top (func (param eqref) (result anyref))))
+ (type $mid (sub $top (func (param eqref) (result anyref))))
+ ;; CHECK:      (type $bot (sub $mid (func (param eqref) (result eqref))))
+ (type $bot (sub $mid (func (param eqref) (result eqref))))
+
+ ;; CHECK:      (type $3 (func (result anyref)))
+
+ ;; CHECK:      (type $4 (func (result eqref)))
+
+ ;; CHECK:      (func $return-call-ref-params-limited (type $3) (result anyref)
+ ;; CHECK-NEXT:  (local $f (ref null $mid))
+ ;; CHECK-NEXT:  (local $arg eqref)
+ ;; CHECK-NEXT:  (return_call_ref $mid
+ ;; CHECK-NEXT:   (local.get $arg)
+ ;; CHECK-NEXT:   (local.get $f)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $return-call-ref-params-limited (result anyref)
+  (local $f (ref null $bot))
+  (local $arg i31ref)
+  ;; Same as $call-ref-params-limited, but with return_call_ref.
+  (return_call_ref $bot
+   (local.get $arg)
+   (local.get $f)
+  )
+ )
+
+ ;; CHECK:      (func $return-call-ref-results-limited (type $4) (result eqref)
+ ;; CHECK-NEXT:  (local $f (ref null $bot))
+ ;; CHECK-NEXT:  (local $arg eqref)
+ ;; CHECK-NEXT:  (return_call_ref $bot
+ ;; CHECK-NEXT:   (local.get $arg)
+ ;; CHECK-NEXT:   (local.get $f)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $return-call-ref-results-limited (result eqref)
+  (local $f (ref null $bot))
+  (local $arg i31ref)
+  ;; Same as $call-ref-results-limited, but with return_call_ref, testing that
+  ;; the function's return type constrains the target signature.
+  (return_call_ref $bot
+   (local.get $arg)
+   (local.get $f)
+  )
+ )
+)
+
+(module
+ (rec
+  ;; CHECK:      (rec
+  ;; CHECK-NEXT:  (type $described (descriptor $desc) (struct (field eqref) (field anyref)))
+  (type $described (descriptor $desc) (struct (field eqref) (field anyref)))
+  ;; CHECK:       (type $desc (describes $described) (struct))
+  (type $desc (describes $described) (struct))
+ )
+
+ ;; CHECK:      (type $2 (func (result anyref)))
+
+ ;; CHECK:      (func $struct-new-desc (type $2) (result anyref)
+ ;; CHECK-NEXT:  (local $var1 eqref)
+ ;; CHECK-NEXT:  (local $var2 anyref)
+ ;; CHECK-NEXT:  (local $desc (ref null (exact $desc)))
+ ;; CHECK-NEXT:  (struct.new_desc $described
+ ;; CHECK-NEXT:   (local.get $var1)
+ ;; CHECK-NEXT:   (local.get $var2)
+ ;; CHECK-NEXT:   (local.get $desc)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $struct-new-desc (result anyref)
+  (local $var1 i31ref)
+  (local $var2 i31ref)
+  (local $desc nullref)
+  ;; Require that typeof($var1) <: eqref, typeof($var2) <: anyref, and
+  ;; typeof($desc) <: (ref null (exact $desc)).
+  (struct.new_desc $described
+   (local.get $var1)
+   (local.get $var2)
+   (local.get $desc)
+  )
+ )
+
+ ;; CHECK:      (func $struct-new-default-desc (type $2) (result anyref)
+ ;; CHECK-NEXT:  (local $desc (ref null (exact $desc)))
+ ;; CHECK-NEXT:  (struct.new_default_desc $described
+ ;; CHECK-NEXT:   (local.get $desc)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $struct-new-default-desc (result anyref)
+  (local $desc nullref)
+  ;; Require that typeof($desc) <: (ref null (exact $desc)).
+  (struct.new_default_desc $described
+   (local.get $desc)
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $0 (func))
+
+ ;; CHECK:      (type $mut-i31 (sub (array (mut i31ref))))
+
+ ;; CHECK:      (type $super (sub (array eqref)))
+ (type $super (sub (array (field eqref))))
+ ;; CHECK:      (type $sub (sub $super (array i31ref)))
+ (type $sub (sub $super (array (field i31ref))))
+ (type $mut-i31 (sub (array (field (mut i31ref)))))
+ (type $shared-array (shared (array i8)))
+
+ ;; CHECK:      (type $4 (func (result i31ref)))
+
+ ;; CHECK:      (func $array-get-type (type $4) (result i31ref)
+ ;; CHECK-NEXT:  (local $val (ref null $sub))
+ ;; CHECK-NEXT:  (array.get $sub
+ ;; CHECK-NEXT:   (local.get $val)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $array-get-type (result i31ref)
+  (local $val (ref null $sub))
+  ;; Require that typeof($val) <: (ref null $sub) because further supertypes do
+  ;; not satisfy the requirement on the element type.
+  (array.get $sub
+   (local.get $val)
+   (i32.const 0)
+  )
+ )
+
+ ;; CHECK:      (func $array-len-shared (type $0)
+ ;; CHECK-NEXT:  (local $ref (ref null (shared array)))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (array.len
+ ;; CHECK-NEXT:    (local.get $ref)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $array-len-shared
+  (local $ref (ref null $shared-array))
+  (drop
+   ;; Require that typeof($ref) <: (ref null (shared array)).
+   (array.len
+    (local.get $ref)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $i31-get-shared (type $0)
+ ;; CHECK-NEXT:  (local $null (ref null (shared i31)))
+ ;; CHECK-NEXT:  (local $nonnullable (ref null (shared i31)))
+ ;; CHECK-NEXT:  (local.set $nonnullable
+ ;; CHECK-NEXT:   (ref.i31_shared
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (i31.get_s
+ ;; CHECK-NEXT:    (local.get $null)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (i31.get_u
+ ;; CHECK-NEXT:    (local.get $nonnullable)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $i31-get-shared
+  (local $null (ref null (shared none)))
+  (local $nonnullable (ref (shared i31)))
+  (local.set $nonnullable
+   (ref.i31_shared
+    (i32.const 0)
+   )
+  )
+  (drop
+   ;; Require that typeof($null) <: (ref null (shared i31)).
+   (i31.get_s
+    (local.get $null)
+   )
+  )
+  (drop
+   ;; Require that typeof($nonnullable) <: (ref null (shared i31)).
+   (i31.get_u
+    (local.get $nonnullable)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $array-copy-ref-limited (type $0)
+ ;; CHECK-NEXT:  (local $dest (ref null $mut-i31))
+ ;; CHECK-NEXT:  (local $src (ref null $sub))
+ ;; CHECK-NEXT:  (array.copy $mut-i31 $sub
+ ;; CHECK-NEXT:   (local.get $dest)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (local.get $src)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $array-copy-ref-limited
+  (local $dest (ref null $mut-i31))
+  (local $src (ref null $sub))
+  ;; Require that typeof($dest) <: $mut-i31 and that typeof($src) <: $sub
+  ;; because $super's element type (eqref) is not a subtype of $mut-i31's
+  ;; element type (i31ref).
+  (array.copy $mut-i31 $sub
+   (local.get $dest)
+   (i32.const 0)
+   (local.get $src)
+   (i32.const 0)
+   (i32.const 0)
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $outer-super (sub (struct)))
+ (type $outer-super (sub (struct)))
+ ;; CHECK:      (type $outer-sub (sub $outer-super (struct (field i32))))
+ (type $outer-sub (sub $outer-super (struct (field i32))))
+ ;; CHECK:      (type $2 (func (result i32)))
+
+ ;; CHECK:      (type $array-super (sub (array (ref $outer-super))))
+ (type $array-super (sub (array (ref $outer-super))))
+ ;; CHECK:      (type $array-sub (sub $array-super (array (ref $outer-sub))))
+ (type $array-sub (sub $array-super (array (ref $outer-sub))))
+ ;; CHECK:      (type $func-super (sub (func (result (ref $outer-super)))))
+ (type $func-super (sub (func (result (ref $outer-super)))))
+ ;; CHECK:      (type $func-sub (sub $func-super (func (result (ref $outer-sub)))))
+ (type $func-sub (sub $func-super (func (result (ref $outer-sub)))))
+
+ ;; CHECK:      (func $array-get-non-null-elem (type $2) (result i32)
+ ;; CHECK-NEXT:  (local $var (ref null $array-sub))
+ ;; CHECK-NEXT:  (struct.get $outer-sub 0
+ ;; CHECK-NEXT:   (array.get $array-sub
+ ;; CHECK-NEXT:    (local.get $var)
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $array-get-non-null-elem (result i32)
+  (local $var (ref null $array-sub))
+  ;; Same as $struct-get-non-null-field, but with an inner array.get.
+  (struct.get $outer-sub 0
+   (array.get $array-sub
+    (local.get $var)
+    (i32.const 0)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $call-ref-non-null-result (type $2) (result i32)
+ ;; CHECK-NEXT:  (local $var (ref null $func-sub))
+ ;; CHECK-NEXT:  (struct.get $outer-sub 0
+ ;; CHECK-NEXT:   (call_ref $func-sub
+ ;; CHECK-NEXT:    (local.get $var)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $call-ref-non-null-result (result i32)
+  (local $var (ref null $func-sub))
+  ;; Same as $struct-get-non-null-field, but with an inner call_ref.
+  (struct.get $outer-sub 0
+   (call_ref $func-sub
+    (local.get $var)
+   )
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $func-void (func))
+
+ ;; CHECK:      (type $cont-void (cont $func-void))
+
+ ;; CHECK:      (type $super-func (sub (func (param eqref) (result eqref))))
+ (type $super-func (sub (func (param eqref) (result eqref))))
+ (type $sub-func (sub $super-func (func (param anyref) (result i31ref))))
+ ;; CHECK:      (type $3 (func (param (ref null $cont-void))))
+
+ ;; CHECK:      (type $4 (func (param eqref)))
+
+ ;; CHECK:      (type $cont-super (cont $super-func))
+ (type $cont-super (cont $super-func))
+ (type $func-void (func))
+ (type $cont-void (cont $func-void))
+
+ ;; CHECK:      (tag $tag-eq (type $4) (param eqref))
+ (tag $tag-eq (param eqref))
+
+ ;; CHECK:      (func $throw (type $func-void)
+ ;; CHECK-NEXT:  (local $val eqref)
+ ;; CHECK-NEXT:  (throw $tag-eq
+ ;; CHECK-NEXT:   (local.get $val)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $throw
+  (local $val i31ref)
+  ;; Require typeof($val) <: eqref.
+  (throw $tag-eq
+   (local.get $val)
+  )
+ )
+
+ ;; CHECK:      (func $throw-ref (type $func-void)
+ ;; CHECK-NEXT:  (local $exn exnref)
+ ;; CHECK-NEXT:  (throw_ref
+ ;; CHECK-NEXT:   (local.get $exn)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $throw-ref
+  (local $exn nullexnref)
+  ;; Require typeof($exn) <: exnref.
+  (throw_ref
+   (local.get $exn)
+  )
+ )
+
+ ;; CHECK:      (func $cont-new (type $func-void)
+ ;; CHECK-NEXT:  (local $f (ref null $super-func))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (cont.new $cont-super
+ ;; CHECK-NEXT:    (local.get $f)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $cont-new
+  (local $f (ref null $sub-func))
+  ;; Require typeof($f) <: (ref null $super-func).
+  (drop
+   (cont.new $cont-super
+    (local.get $f)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $resume-throw (type $3) (param $c (ref null $cont-void))
+ ;; CHECK-NEXT:  (local $val eqref)
+ ;; CHECK-NEXT:  (resume_throw $cont-void $tag-eq
+ ;; CHECK-NEXT:   (local.get $val)
+ ;; CHECK-NEXT:   (local.get $c)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $resume-throw (param $c (ref null $cont-void))
+  (local $val i31ref)
+  ;; Require typeof($val) <: eqref.
+  (resume_throw $cont-void $tag-eq
+   (local.get $val)
+   (local.get $c)
+  )
+ )
+
+ ;; CHECK:      (func $resume-throw-ref (type $3) (param $c (ref null $cont-void))
+ ;; CHECK-NEXT:  (local $exn exnref)
+ ;; CHECK-NEXT:  (resume_throw_ref $cont-void
+ ;; CHECK-NEXT:   (local.get $exn)
+ ;; CHECK-NEXT:   (local.get $c)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $resume-throw-ref (param $c (ref null $cont-void))
+  (local $exn nullexnref)
+  ;; Require typeof($exn) <: exnref.
+  (resume_throw_ref $cont-void
+   (local.get $exn)
+   (local.get $c)
+  )
+ )
+)
+
+(module
+ (rec
+  ;; CHECK:      (rec
+  ;; CHECK-NEXT:  (type $A (descriptor $A.desc) (struct))
+  (type $A (descriptor $A.desc) (struct))
+  ;; CHECK:       (type $A.desc (describes $A) (struct))
+  (type $A.desc (describes $A) (struct))
+ )
+
+ ;; CHECK:      (type $2 (func))
+
+ ;; CHECK:      (type $3 (func (param anyref)))
+
+ ;; CHECK:      (type $4 (func (result (ref $A.desc))))
+
+ ;; CHECK:      (func $ref.cast_desc_eq (type $2)
+ ;; CHECK-NEXT:  (local $x (ref null $A.desc))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (ref.cast_desc_eq (ref $A)
+ ;; CHECK-NEXT:    (ref.null none)
+ ;; CHECK-NEXT:    (local.get $x)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $ref.cast_desc_eq
+  (local $x (ref null $A.desc))
+  ;; We cannot generalize x to anyref: it is used as descriptor, and must
+  ;; remain a valid descriptor type.
+  (drop
+   (ref.cast_desc_eq (ref $A)
+    (ref.null eq)
+    (local.get $x)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $br-on-cast-desc-eq (type $3) (param $any anyref)
+ ;; CHECK-NEXT:  (local $x (ref null $A.desc))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (block $l (result (ref null $A))
+ ;; CHECK-NEXT:    (drop
+ ;; CHECK-NEXT:     (br_on_cast_desc_eq $l anyref (ref null $A)
+ ;; CHECK-NEXT:      (local.get $any)
+ ;; CHECK-NEXT:      (local.get $x)
+ ;; CHECK-NEXT:     )
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:    (unreachable)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $br-on-cast-desc-eq (param $any anyref)
+  (local $x (ref null $A.desc))
+  ;; As above, with br_on.
+  (drop
+   (block $l (result (ref null $A))
+    (br_on_cast_desc_eq $l anyref (ref null $A)
+     (local.get $any)
+     (local.get $x)
+    )
+    (unreachable)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $ref.get_desc (type $4) (result (ref $A.desc))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (ref.get_desc $A
+ ;; CHECK-NEXT:   (local.get $x)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $ref.get_desc (result (ref $A.desc))
+  ;; We cannot generalize x to anyref: it must have a descriptor.
+  (local $x (ref null $A))
+  (ref.get_desc $A
+   (local.get $x)
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $A (sub (struct)))
+ (type $A (sub (struct)))
+
+ ;; CHECK:      (type $1 (func (result (ref $A))))
+
+ ;; CHECK:      (func $br_on_non_null (type $1) (result (ref $A))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (block $block (result (ref $A))
+ ;; CHECK-NEXT:   (br_on_non_null $block
+ ;; CHECK-NEXT:    (local.get $x)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:   (unreachable)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $br_on_non_null (result (ref $A))
+  (local $x (ref null $A))
+  ;; We cannot refine the local to anyref, as the result is (ref $A).
+  (block $block (result (ref $A))
+   (br_on_non_null $block
+    (local.get $x)
+   )
+   (unreachable)
+  )
+ )
+
+ ;; CHECK:      (func $br_on_cast_fail (type $1) (result (ref $A))
+ ;; CHECK-NEXT:  (local $A (ref $A))
+ ;; CHECK-NEXT:  (block $block (result (ref $A))
+ ;; CHECK-NEXT:   (drop
+ ;; CHECK-NEXT:    (br_on_cast_fail $block (ref $A) (ref $A)
+ ;; CHECK-NEXT:     (local.tee $A
+ ;; CHECK-NEXT:      (struct.new_default $A)
+ ;; CHECK-NEXT:     )
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:   (unreachable)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $br_on_cast_fail (result (ref $A))
+  (local $A (ref $A))
+  ;; The block must return $A, so the cast_fail must send it, and the local
+  ;; cannot be refined to anyref.
+  (block $block (result (ref $A))
+   (drop
+    (br_on_cast_fail $block (ref $A) (ref $A)
+     (local.tee $A
+      (struct.new $A)
+     )
+    )
+   )
+   (unreachable)
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $A (struct (field (mut i32))))
+ (type $A (struct (field (mut i32))))
+
+ ;; CHECK:      (type $1 (func (result i32)))
+
+ ;; CHECK:      (type $2 (func (result i32 (ref null $A))))
+
+ ;; CHECK:      (func $struct.atomic (type $1) (result i32)
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (struct.atomic.rmw.cmpxchg $A 0
+ ;; CHECK-NEXT:   (local.tee $x
+ ;; CHECK-NEXT:    (ref.null none)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:   (i32.const 0)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $struct.atomic (result i32)
+  ;; TODO: Optimize struct/array atomics. For now, just do not error by
+  ;;       generalizing too much so validation breaks.
+  (local $x (ref null $A))
+  (struct.atomic.rmw.cmpxchg $A 0
+   (local.tee $x
+    (ref.null none)
+   )
+   (i32.const 0)
+   (i32.const 0)
+  )
+ )
+
+ ;; CHECK:      (func $tuple.make (type $2) (result i32 (ref null $A))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (local $tuple (tuple i32 (ref null $A)))
+ ;; CHECK-NEXT:  (local.tee $tuple
+ ;; CHECK-NEXT:   (tuple.make 2
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:    (local.get $x)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $tuple.make (result i32 (ref null $A))
+  ;; TODO: Optimize tuples. For now, just do not error by generalizing operands
+  ;;       of tuple.make too much so validation breaks.
+  (local $x (ref null $A))
+  (local $tuple (tuple i32 (ref null $A)))
+  (local.tee $tuple
+   (tuple.make 2
+    (i32.const 0)
+    (local.get $x)
+   )
+  )
+ )
+)
+
+(module
+ ;; CHECK:      (type $A (sub (struct)))
+ (type $A (sub (struct)))
+ ;; CHECK:      (type $1 (func (result (ref $A))))
+
+ ;; CHECK:      (type $B (sub $A (struct)))
+ (type $B (sub $A (struct)))
+
+ ;; CHECK:      (func $br_on_cast_fail_nullable (type $1) (result (ref $A))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (block $block (result (ref $A))
+ ;; CHECK-NEXT:   (drop
+ ;; CHECK-NEXT:    (br_on_cast_fail $block (ref null $A) (ref null $B)
+ ;; CHECK-NEXT:     (local.get $x)
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:   (unreachable)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $br_on_cast_fail_nullable (result (ref $A))
+  (local $x (ref null $B))
+  ;; The cast type is nullable, so nulls succeed the cast and do not branch.
+  ;; The sent value is therefore non-nullable, allowing $x to generalize to
+  ;; nullable (ref null $A) even though $block expects non-nullable (ref $A).
+  (block $block (result (ref $A))
+   (drop
+    (br_on_cast_fail $block (ref null $B) (ref null $B)
+     (local.get $x)
+    )
+   )
+   (unreachable)
+  )
+ )
+
+ ;; CHECK:      (func $br_on_null (type $1) (result (ref $A))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (block $block
+ ;; CHECK-NEXT:   (return
+ ;; CHECK-NEXT:    (br_on_null $block
+ ;; CHECK-NEXT:     (local.get $x)
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (unreachable)
+ ;; CHECK-NEXT: )
+ (func $br_on_null (result (ref $A))
+  (local $x (ref null $A))
+  ;; The fallthrough value is returned as (ref $A), so $x cannot generalize to
+  ;; anyref, though it remains nullable.
+  (block $block
+   (return
+    (br_on_null $block
+     (local.get $x)
+    )
+   )
+  )
+  (unreachable)
+ )
+
+ ;; CHECK:      (func $br_on_cast_fallthrough (type $1) (result (ref $A))
+ ;; CHECK-NEXT:  (local $x (ref null $A))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (block $block (result (ref null $A))
+ ;; CHECK-NEXT:    (return
+ ;; CHECK-NEXT:     (br_on_cast $block (ref null $A) (ref null $A)
+ ;; CHECK-NEXT:      (local.get $x)
+ ;; CHECK-NEXT:     )
+ ;; CHECK-NEXT:    )
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT:  (unreachable)
+ ;; CHECK-NEXT: )
+ (func $br_on_cast_fallthrough (result (ref $A))
+  (local $x (ref null $A))
+  ;; The fallthrough value is returned as (ref $A), so $x cannot generalize to
+  ;; anyref, though it remains nullable because nulls take the branch.
+  (drop
+   (block $block (result (ref null $A))
+    (return
+     (br_on_cast $block (ref null $A) (ref null $A)
+      (local.get $x)
+     )
+    )
+   )
+  )
+  (unreachable)
+ )
+)
+
+(module
+ ;; CHECK:      (type $void (func))
+
+ ;; CHECK:      (type $val (sub (struct)))
+ (type $val (sub (struct)))
+ (type $subval (sub $val (struct)))
+ ;; CHECK:      (type $cont (cont $void))
+
+ ;; CHECK:      (type $struct (struct (field (mut (ref null $val)))))
+ (type $struct (struct (field (mut (ref null $val)))))
+ ;; CHECK:      (type $arr (array (mut (ref null $val))))
+ (type $arr (array (mut (ref null $val))))
+ (type $void (func))
+ (type $cont (cont $void))
+
+ ;; CHECK:      (func $struct.atomic.xchg (type $void)
+ ;; CHECK-NEXT:  (local $s (ref null $struct))
+ ;; CHECK-NEXT:  (local $v (ref null $val))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (struct.atomic.rmw.xchg $struct 0
+ ;; CHECK-NEXT:    (local.get $s)
+ ;; CHECK-NEXT:    (local.get $v)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $struct.atomic.xchg
+  (local $s (ref null $struct))
+  (local $v (ref null $subval))
+  ;; $s must remain (ref null $struct), while $v can generalize to (ref null $val)
+  ;; (the field type), not anyref.
+  (drop
+   (struct.atomic.rmw.xchg $struct 0
+    (local.get $s)
+    (local.get $v)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $array.atomic.cmpxchg (type $void)
+ ;; CHECK-NEXT:  (local $a (ref null $arr))
+ ;; CHECK-NEXT:  (local $exp eqref)
+ ;; CHECK-NEXT:  (local $rep (ref null $val))
+ ;; CHECK-NEXT:  (drop
+ ;; CHECK-NEXT:   (array.atomic.rmw.cmpxchg $arr
+ ;; CHECK-NEXT:    (local.get $a)
+ ;; CHECK-NEXT:    (i32.const 0)
+ ;; CHECK-NEXT:    (local.get $exp)
+ ;; CHECK-NEXT:    (local.get $rep)
+ ;; CHECK-NEXT:   )
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $array.atomic.cmpxchg
+  (local $a (ref null $arr))
+  (local $exp (ref null $subval))
+  (local $rep (ref null $subval))
+  ;; $a must remain (ref null $arr), $exp can generalize to eqref, and $rep can
+  ;; generalize to (ref null $val).
+  (drop
+   (array.atomic.rmw.cmpxchg $arr
+    (local.get $a)
+    (i32.const 0)
+    (local.get $exp)
+    (local.get $rep)
+   )
+  )
+ )
+
+ ;; CHECK:      (func $resume.local (type $void)
+ ;; CHECK-NEXT:  (local $c (ref null $cont))
+ ;; CHECK-NEXT:  (resume $cont
+ ;; CHECK-NEXT:   (local.get $c)
+ ;; CHECK-NEXT:  )
+ ;; CHECK-NEXT: )
+ (func $resume.local
+  (local $c (ref null $cont))
+  ;; $c must remain (ref null $cont), not generalize to contref.
+  (resume $cont
+   (local.get $c)
+  )
+ )
+)
+