From 540ad3a08f269a133f4383c1aa273dec97e80b83 Mon Sep 17 00:00:00 2001
From: Kevin Gibbons <bakkot@gmail.com>
Date: Tue, 17 Sep 2024 19:17:48 -0700
Subject: [PATCH] Refactor typechecker (#612)

---
 src/Spec.ts        |   5 +-
 src/type-logic.ts  | 576 +++++++++++++++++++++++++++++
 src/typechecker.ts | 900 ++++++++++-----------------------------------
 test/typecheck.js  |   6 +-
 4 files changed, 773 insertions(+), 714 deletions(-)
 create mode 100644 src/type-logic.ts

diff --git a/src/Spec.ts b/src/Spec.ts
index ea865a67..1183114c 100644
--- a/src/Spec.ts
+++ b/src/Spec.ts
@@ -526,12 +526,13 @@ export default class Spec {
 
     this.setReplacementAlgorithmOffsets();
 
-    this.autolink();
-
     if (this.opts.lintSpec) {
       this.log('Checking types...');
       typecheck(this);
     }
+
+    this.autolink();
+
     this.log('Propagating effect annotations...');
     this.propagateEffects();
     this.log('Annotating external links...');
diff --git a/src/type-logic.ts b/src/type-logic.ts
new file mode 100644
index 00000000..15f1fecd
--- /dev/null
+++ b/src/type-logic.ts
@@ -0,0 +1,576 @@
+import type Biblio from './Biblio';
+import type { Type as BiblioType } from './Biblio';
+import type { Expr, NonSeq } from './expr-parser';
+
+type Type =
+  | { kind: 'unknown' } // top
+  | { kind: 'never' } // bottom
+  | { kind: 'union'; of: NonUnion[] } // constraint: nothing in the union dominates anything else in the union
+  | { kind: 'list'; of: Type }
+  | { kind: 'record' } // TODO more precision
+  | { kind: 'normal completion'; of: Type }
+  | { kind: 'abrupt completion' }
+  | { kind: 'real' }
+  | { kind: 'integer' }
+  | { kind: 'non-negative integer' }
+  | { kind: 'negative integer' }
+  | { kind: 'positive integer' }
+  | { kind: 'concrete real'; value: string }
+  | { kind: 'ES value' }
+  | { kind: 'string' }
+  | { kind: 'number' }
+  | { kind: 'integral number' }
+  | { kind: 'bigint' }
+  | { kind: 'boolean' }
+  | { kind: 'null' }
+  | { kind: 'undefined' }
+  | { kind: 'concrete string'; value: string }
+  | { kind: 'concrete number'; value: number }
+  | { kind: 'concrete bigint'; value: bigint }
+  | { kind: 'concrete boolean'; value: boolean }
+  | { kind: 'enum value'; value: string };
+type NonUnion = Exclude<Type, { kind: 'union' }>;
+const simpleKinds = new Set<Type['kind']>([
+  'unknown',
+  'never',
+  'record',
+  'abrupt completion',
+  'real',
+  'integer',
+  'non-negative integer',
+  'negative integer',
+  'positive integer',
+  'ES value',
+  'string',
+  'number',
+  'integral number',
+  'bigint',
+  'boolean',
+  'null',
+  'undefined',
+]);
+const dominateGraph: Partial<Record<Type['kind'], Type['kind'][]>> = {
+  // @ts-expect-error TS does not know about __proto__
+  __proto__: null,
+  record: ['normal completion', 'abrupt completion'],
+  real: [
+    'integer',
+    'non-negative integer',
+    'negative integer',
+    'positive integer',
+    'concrete real',
+  ],
+  integer: ['non-negative integer', 'negative integer', 'positive integer'],
+  'non-negative integer': ['positive integer'],
+  'ES value': [
+    'string',
+    'number',
+    'integral number',
+    'bigint',
+    'boolean',
+    'null',
+    'undefined',
+    'concrete string',
+    'concrete number',
+    'concrete bigint',
+    'concrete boolean',
+  ],
+  string: ['concrete string'],
+  number: ['integral number', 'concrete number'],
+  bigint: ['concrete bigint'],
+  boolean: ['concrete boolean'],
+};
+/*
+The type lattice used here is very simple (aside from explicit unions).
+As such we mostly only need to define the `dominates` relationship and apply trivial rules:
+if `x` dominates `y`, then `join(x,y) = x` and `meet(x,y) = y`; if neither dominates the other than the join is top and the meet is bottom.
+Unions/lists/completions take a little more work.
+*/
+export function dominates(a: Type, b: Type): boolean {
+  if (a.kind === 'unknown' || b.kind === 'never') {
+    return true;
+  }
+  if (b.kind === 'union') {
+    return b.of.every(t => dominates(a, t));
+  }
+  if (a.kind === 'union') {
+    // not necessarily true for arbitrary lattices, but true for ours
+    return a.of.some(t => dominates(t, b));
+  }
+  if (
+    (a.kind === 'list' && b.kind === 'list') ||
+    (a.kind === 'normal completion' && b.kind === 'normal completion')
+  ) {
+    return dominates(a.of, b.of);
+  }
+  if (simpleKinds.has(a.kind) && simpleKinds.has(b.kind) && a.kind === b.kind) {
+    return true;
+  }
+  if (dominateGraph[a.kind]?.includes(b.kind) ?? false) {
+    return true;
+  }
+  if (a.kind === 'integer' && b.kind === 'concrete real') {
+    return !b.value.includes('.');
+  }
+  if (a.kind === 'integral number' && b.kind === 'concrete number') {
+    return Number.isFinite(b.value) && b.value === Math.round(b.value);
+  }
+  if (a.kind === 'non-negative integer' && b.kind === 'concrete real') {
+    return !b.value.includes('.') && b.value[0] !== '-';
+  }
+  if (a.kind === 'negative integer' && b.kind === 'concrete real') {
+    return !b.value.includes('.') && b.value[0] === '-';
+  }
+  if (a.kind === 'positive integer' && b.kind === 'concrete real') {
+    return !b.value.includes('.') && b.value[0] !== '-' && b.value !== '0';
+  }
+  if (
+    a.kind === b.kind &&
+    [
+      'concrete string',
+      'concrete number',
+      'concrete real',
+      'concrete bigint',
+      'concrete boolean',
+      'enum value',
+    ].includes(a.kind)
+  ) {
+    // @ts-expect-error TS is not quite smart enough for this
+    return Object.is(a.value, b.value);
+  }
+  return false;
+}
+function addToUnion(types: NonUnion[], type: NonUnion): Type {
+  if (type.kind === 'normal completion') {
+    const existingNormalCompletionIndex = types.findIndex(t => t.kind === 'normal completion');
+    if (existingNormalCompletionIndex !== -1) {
+      // prettier-ignore
+      const joined = join(types[existingNormalCompletionIndex], type) as Type & { kind: 'normal completion' };
+      if (types.length === 1) {
+        return joined;
+      }
+      const typesCopy = [...types];
+      typesCopy.splice(existingNormalCompletionIndex, 1, joined);
+      return { kind: 'union', of: typesCopy };
+    }
+  }
+
+  if (types.some(t => dominates(t, type))) {
+    return { kind: 'union', of: types };
+  }
+  const live = types.filter(t => !dominates(type, t));
+  if (live.length === 0) {
+    return type;
+  }
+  return { kind: 'union', of: [...live, type] };
+}
+
+export function join(a: Type, b: Type): Type {
+  if (dominates(a, b)) {
+    return a;
+  }
+  if (dominates(b, a)) {
+    return b;
+  }
+  if (b.kind === 'union') {
+    [a, b] = [b, a];
+  }
+  if (a.kind === 'union') {
+    if (b.kind === 'union') {
+      return b.of.reduce(
+        (acc: Type, t) => (acc.kind === 'union' ? addToUnion(acc.of, t) : join(acc, t)),
+        a,
+      );
+    }
+    return addToUnion(a.of, b);
+  }
+  if (
+    (a.kind === 'list' && b.kind === 'list') ||
+    (a.kind === 'normal completion' && b.kind === 'normal completion')
+  ) {
+    return { kind: a.kind, of: join(a.of, b.of) };
+  }
+  return { kind: 'union', of: [a, b as NonUnion] };
+}
+
+export function meet(a: Type, b: Type): Type {
+  if (dominates(a, b)) {
+    return b;
+  }
+  if (dominates(b, a)) {
+    return a;
+  }
+  if (a.kind !== 'union' && b.kind === 'union') {
+    [a, b] = [b, a];
+  }
+  if (a.kind === 'union') {
+    // union is join. meet distributes over join.
+    return a.of.map(t => meet(t, b)).reduce(join);
+  }
+  if (
+    (a.kind === 'list' && b.kind === 'list') ||
+    (a.kind === 'normal completion' && b.kind === 'normal completion')
+  ) {
+    return { kind: a.kind, of: meet(a.of, b.of) };
+  }
+  return { kind: 'never' };
+}
+
+export function serialize(type: Type): string {
+  switch (type.kind) {
+    case 'unknown': {
+      return 'unknown';
+    }
+    case 'never': {
+      return 'never';
+    }
+    case 'union': {
+      const parts = type.of.map(serialize);
+      if (parts.length > 2) {
+        return parts.slice(0, -1).join(', ') + ', or ' + parts[parts.length - 1];
+      }
+      return parts[0] + ' or ' + parts[1];
+    }
+    case 'list': {
+      if (type.of.kind === 'never') {
+        return 'empty List';
+      }
+      return 'List of ' + serialize(type.of);
+    }
+    case 'record': {
+      return 'Record';
+    }
+    case 'normal completion': {
+      if (type.of.kind === 'never') {
+        return 'never';
+      } else if (type.of.kind === 'unknown') {
+        return 'a normal completion';
+      }
+      return 'a normal completion containing ' + serialize(type.of);
+    }
+    case 'abrupt completion': {
+      return 'an abrupt completion';
+    }
+    case 'real': {
+      return 'mathematical value';
+    }
+    case 'integer':
+    case 'non-negative integer':
+    case 'negative integer':
+    case 'positive integer':
+    case 'null':
+    case 'undefined': {
+      return type.kind;
+    }
+    case 'concrete string': {
+      return `"${type.value}"`;
+    }
+    case 'concrete real': {
+      return type.value;
+    }
+    case 'concrete boolean': {
+      return `${type.value}`;
+    }
+    case 'enum value': {
+      return `~${type.value}~`;
+    }
+    case 'concrete number': {
+      if (Object.is(type.value, 0 / 0)) {
+        return '*NaN*';
+      }
+      let repr;
+      if (Object.is(type.value, -0)) {
+        repr = '-0';
+      } else if (type.value === 0) {
+        repr = '+0';
+      } else if (type.value === 2e308) {
+        repr = '+&infin;';
+      } else if (type.value === -2e308) {
+        repr = '-&infin;';
+      } else if (type.value > 4503599627370495.5) {
+        repr = String(BigInt(type.value));
+      } else {
+        repr = String(type.value);
+      }
+      return `*${repr}*<sub>𝔽</sub>`;
+    }
+    case 'concrete bigint': {
+      return `*${type.value}*<sub>ℤ</sub>`;
+    }
+    case 'ES value': {
+      return 'ECMAScript language value';
+    }
+    case 'boolean': {
+      return 'Boolean';
+    }
+    case 'string': {
+      return 'String';
+    }
+    case 'number': {
+      return 'Number';
+    }
+    case 'integral number': {
+      return 'integral Number';
+    }
+    case 'bigint': {
+      return 'BigInt';
+    }
+  }
+}
+
+export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
+  seq: if (expr.name === 'seq') {
+    const items = stripWhitespace(expr.items);
+    if (items.length === 1) {
+      expr = items[0];
+      break seq;
+    }
+
+    if (
+      items.length === 2 &&
+      items[0].name === 'star' &&
+      items[0].contents[0].name === 'text' &&
+      items[1].name === 'text'
+    ) {
+      switch (items[1].contents) {
+        case '𝔽': {
+          const text = items[0].contents[0].contents;
+          let value;
+          if (text === '-0') {
+            value = -0;
+          } else if (text === '+&infin;') {
+            value = 2e308;
+          } else if (text === '-&infin;') {
+            value = -2e308;
+          } else {
+            value = parseFloat(text);
+          }
+          return { kind: 'concrete number', value };
+        }
+        case 'ℤ': {
+          return { kind: 'concrete bigint', value: BigInt(items[0].contents[0].contents) };
+        }
+      }
+    }
+
+    if (items[0]?.name === 'text' && ['!', '?'].includes(items[0].contents.trim())) {
+      const remaining = stripWhitespace(items.slice(1));
+      if (remaining.length === 1 && ['call', 'sdo-call'].includes(remaining[0].name)) {
+        const callType = typeFromExpr(remaining[0], biblio);
+        if (isCompletion(callType)) {
+          const normal: Type =
+            callType.kind === 'normal completion'
+              ? callType.of
+              : callType.kind === 'abrupt completion'
+                ? // the expression `? _abrupt_` strictly speaking has type `never`
+                  // however we mostly use `never` to mean user error, so use unknown instead
+                  // this should only ever happen after `Return`
+                  { kind: 'unknown' }
+                : callType.of.find(k => k.kind === 'normal completion')?.of ?? { kind: 'unknown' };
+          return normal;
+        }
+      }
+    }
+  }
+
+  switch (expr.name) {
+    case 'text': {
+      const text = expr.contents.trim();
+      if (/^-?[0-9]+(\.[0-9]+)?$/.test(text)) {
+        return { kind: 'concrete real', value: text };
+      }
+      break;
+    }
+    case 'list': {
+      return {
+        kind: 'list',
+        of: expr.elements.map(t => typeFromExpr(t, biblio)).reduce(join, { kind: 'never' }),
+      };
+    }
+    case 'record': {
+      return { kind: 'record' };
+    }
+    case 'call':
+    case 'sdo-call': {
+      const { callee } = expr;
+      if (!(callee.length === 1 && callee[0].name === 'text')) {
+        break;
+      }
+      const calleeName = callee[0].contents;
+
+      const biblioEntry = biblio.byAoid(calleeName);
+      if (biblioEntry?.signature?.return == null) {
+        break;
+      }
+      return typeFromExprType(biblioEntry.signature.return);
+    }
+    case 'tilde': {
+      if (expr.contents.length === 1 && expr.contents[0].name === 'text') {
+        return { kind: 'enum value', value: expr.contents[0].contents };
+      }
+      break;
+    }
+    case 'star': {
+      if (expr.contents.length === 1 && expr.contents[0].name === 'text') {
+        const text = expr.contents[0].contents;
+        if (text === 'null') {
+          return { kind: 'null' };
+        } else if (text === 'undefined') {
+          return { kind: 'undefined' };
+        } else if (text === 'NaN') {
+          return { kind: 'concrete number', value: 0 / 0 };
+        } else if (text === 'true') {
+          return { kind: 'concrete boolean', value: true };
+        } else if (text === 'false') {
+          return { kind: 'concrete boolean', value: false };
+        } else if (text.startsWith('"') && text.endsWith('"')) {
+          return { kind: 'concrete string', value: text.slice(1, -1) };
+        }
+      }
+
+      break;
+    }
+  }
+  return { kind: 'unknown' };
+}
+export function typeFromExprType(type: BiblioType): Type {
+  switch (type.kind) {
+    case 'union': {
+      return type.types.map(typeFromExprType).reduce(join);
+    }
+    case 'list': {
+      return {
+        kind: 'list',
+        of: type.elements == null ? { kind: 'unknown' } : typeFromExprType(type.elements),
+      };
+    }
+    case 'completion': {
+      if (type.completionType === 'abrupt') {
+        return { kind: 'abrupt completion' };
+      } else {
+        const normalType: Type =
+          type.typeOfValueIfNormal == null
+            ? { kind: 'unknown' }
+            : typeFromExprType(type.typeOfValueIfNormal);
+        if (type.completionType === 'normal') {
+          return { kind: 'normal completion', of: normalType };
+        } else if (type.completionType === 'mixed') {
+          return {
+            kind: 'union',
+            of: [{ kind: 'normal completion', of: normalType }, { kind: 'abrupt completion' }],
+          };
+        } else {
+          throw new Error('unreachable: completion kind ' + type.completionType);
+        }
+      }
+    }
+    case 'opaque': {
+      const text = type.type;
+      if (text.startsWith('"') && text.endsWith('"')) {
+        return { kind: 'concrete string', value: text.slice(1, -1) };
+      }
+      if (text.startsWith('~') && text.endsWith('~')) {
+        return { kind: 'enum value', value: text.slice(1, -1) };
+      }
+      if (/^-?[0-9]+(\.[0-9]+)?$/.test(text)) {
+        return { kind: 'concrete real', value: text };
+      }
+      if (text.startsWith('*') && text.endsWith('*<sub>𝔽</sub>')) {
+        const innerText = text.slice(1, -14);
+        let value;
+        if (innerText === '-0') {
+          value = -0;
+        } else if (innerText === '+&infin;') {
+          value = 2e308;
+        } else if (innerText === '-&infin;') {
+          value = -2e308;
+        } else {
+          value = parseFloat(innerText);
+        }
+        return { kind: 'concrete number', value };
+      }
+      if (text === '*NaN*') {
+        return { kind: 'concrete number', value: 0 / 0 };
+      }
+      if (text.startsWith('*') && text.endsWith('*<sub>ℤ</sub>')) {
+        return { kind: 'concrete bigint', value: BigInt(text.slice(1, -14)) };
+      }
+      if (text === 'an ECMAScript language value' || text === 'ECMAScript language values') {
+        return { kind: 'ES value' };
+      }
+      if (text === 'a String' || text === 'Strings') {
+        return { kind: 'string' };
+      }
+      if (text === 'a Number' || text === 'Numbers') {
+        return { kind: 'number' };
+      }
+      if (text === 'a Boolean' || text === 'Booleans') {
+        return { kind: 'boolean' };
+      }
+      if (text === 'a BigInt' || text === 'BigInts') {
+        return { kind: 'bigint' };
+      }
+      if (text === 'an integral Number' || text === 'integral Numbers') {
+        return { kind: 'integral number' };
+      }
+      if (text === 'a mathematical value' || text === 'mathematical values') {
+        return { kind: 'real' };
+      }
+      if (text === 'an integer' || text === 'integers') {
+        return { kind: 'integer' };
+      }
+      if (text === 'a non-negative integer' || text === 'non-negative integers') {
+        return { kind: 'non-negative integer' };
+      }
+      if (text === 'a negative integer' || text === 'negative integers') {
+        return { kind: 'negative integer' };
+      }
+      if (text === 'a positive integer' || text === 'positive integers') {
+        return { kind: 'positive integer' };
+      }
+      if (text === 'a time value' || text === 'time values') {
+        return {
+          kind: 'union',
+          of: [{ kind: 'integral number' }, { kind: 'concrete number', value: 0 / 0 }],
+        };
+      }
+      if (text === '*null*') {
+        return { kind: 'null' };
+      }
+      if (text === '*undefined*') {
+        return { kind: 'undefined' };
+      }
+      break;
+    }
+    case 'unused': {
+      // this is really only a return type, but might as well handle it
+      return { kind: 'enum value', value: '~unused~' };
+    }
+  }
+  return { kind: 'unknown' };
+}
+
+export function isCompletion(
+  type: Type,
+): type is Type & { kind: 'normal completion' | 'abrupt completion' | 'union' } {
+  return (
+    type.kind === 'normal completion' ||
+    type.kind === 'abrupt completion' ||
+    (type.kind === 'union' && type.of.some(isCompletion))
+  );
+}
+
+export function stripWhitespace(items: NonSeq[]) {
+  items = [...items];
+  while (items[0]?.name === 'text' && /^\s+$/.test(items[0].contents)) {
+    items.shift();
+  }
+  while (
+    items[items.length - 1]?.name === 'text' &&
+    // @ts-expect-error
+    /^\s+$/.test(items[items.length - 1].contents)
+  ) {
+    items.pop();
+  }
+  return items;
+}
diff --git a/src/typechecker.ts b/src/typechecker.ts
index b1237145..c6b4ddb0 100644
--- a/src/typechecker.ts
+++ b/src/typechecker.ts
@@ -2,10 +2,182 @@ import type { OrderedListNode } from 'ecmarkdown';
 import type { AlgorithmElementWithTree } from './Algorithm';
 import type { AlgorithmBiblioEntry, Type as BiblioType } from './Biblio';
 import type Spec from './Spec';
-import type { Expr, NonSeq, PathItem, Seq } from './expr-parser';
+import type { Expr, PathItem, Seq } from './expr-parser';
 import { walk as walkExpr, parse as parseExpr, isProsePart } from './expr-parser';
 import { offsetToLineAndColumn, zip } from './utils';
-import type Biblio from './Biblio';
+import {
+  typeFromExpr,
+  typeFromExprType,
+  meet,
+  serialize,
+  dominates,
+  stripWhitespace,
+} from './type-logic';
+
+type OnlyPerformedMap = Map<string, null | 'only performed' | 'top'>;
+type AlwaysAssertedToBeNormalMap = Map<string, null | 'always asserted normal' | 'top'>;
+
+const getExpressionVisitor =
+  (
+    spec: Spec,
+    warn: (offset: number, message: string) => void,
+    onlyPerformed: OnlyPerformedMap,
+    alwaysAssertedToBeNormal: AlwaysAssertedToBeNormalMap,
+  ) =>
+  (expr: Expr, path: PathItem[]) => {
+    if (expr.name !== 'call' && expr.name !== 'sdo-call') {
+      return;
+    }
+
+    const { callee, arguments: args } = expr;
+    if (!(callee.length === 1 && callee[0].name === 'text')) {
+      return;
+    }
+    const calleeName = callee[0].contents;
+
+    const biblioEntry = spec.biblio.byAoid(calleeName);
+    if (biblioEntry == null) {
+      if (!['toUppercase', 'toLowercase'].includes(calleeName)) {
+        // TODO make the spec not do this
+        warn(callee[0].location.start.offset, `could not find definition for ${calleeName}`);
+      }
+      return;
+    }
+
+    if (biblioEntry.kind === 'syntax-directed operation' && expr.name === 'call') {
+      warn(
+        callee[0].location.start.offset,
+        `${calleeName} is a syntax-directed operation and should not be invoked like a regular call`,
+      );
+    } else if (
+      biblioEntry.kind != null &&
+      biblioEntry.kind !== 'syntax-directed operation' &&
+      expr.name === 'sdo-call'
+    ) {
+      warn(
+        callee[0].location.start.offset,
+        `${calleeName} is not a syntax-directed operation but here is being invoked as one`,
+      );
+    }
+
+    if (biblioEntry.signature == null) {
+      return;
+    }
+    const { signature } = biblioEntry;
+    const min = signature.parameters.length;
+    const max = min + signature.optionalParameters.length;
+    if (args.length < min || args.length > max) {
+      const count = `${min}${min === max ? '' : `-${max}`}`;
+      const message = `${calleeName} takes ${count} argument${count === '1' ? '' : 's'}, but this invocation passes ${args.length}`;
+      warn(callee[0].location.start.offset, message);
+    } else {
+      const params = signature.parameters.concat(signature.optionalParameters);
+      for (const [arg, param] of zip(args, params, true)) {
+        if (param.type == null) continue;
+        const argType = typeFromExpr(arg, spec.biblio);
+        const paramType = typeFromExprType(param.type);
+
+        // often we can't infer the argument precisely, so we check only that the intersection is nonempty rather than that the argument type is a subtype of the parameter type
+        const intersection = meet(argType, paramType);
+
+        if (
+          intersection.kind === 'never' ||
+          (intersection.kind === 'list' &&
+            intersection.of.kind === 'never' &&
+            // if the meet is list<never>, and we're passing a concrete list, it had better be empty
+            argType.kind === 'list' &&
+            argType.of.kind !== 'never')
+        ) {
+          const argDescriptor =
+            argType.kind.startsWith('concrete') ||
+            argType.kind === 'enum value' ||
+            argType.kind === 'null' ||
+            argType.kind === 'undefined'
+              ? `(${serialize(argType)})`
+              : `type (${serialize(argType)})`;
+
+          let hint = '';
+          if (argType.kind === 'concrete number' && dominates({ kind: 'real' }, paramType)) {
+            hint =
+              '\nhint: you passed an ES language Number, but this position takes a mathematical value';
+          } else if (argType.kind === 'concrete real' && dominates({ kind: 'number' }, paramType)) {
+            hint =
+              '\nhint: you passed a mathematical value, but this position takes an ES language Number';
+          } else if (argType.kind === 'concrete real' && dominates({ kind: 'bigint' }, paramType)) {
+            hint =
+              '\nhint: you passed a mathematical value, but this position takes an ES language BigInt';
+          }
+
+          const items = stripWhitespace(arg.items);
+          warn(
+            items[0].location.start.offset,
+            `argument ${argDescriptor} does not look plausibly assignable to parameter type (${serialize(paramType)})${hint}`,
+          );
+        }
+      }
+    }
+
+    const { return: returnType } = signature;
+    if (returnType == null) {
+      return;
+    }
+
+    const consumedAsCompletion = isConsumedAsCompletion(expr, path);
+
+    // checks elsewhere ensure that well-formed documents never have a union of completion and non-completion, so checking the first child suffices
+    // TODO: this is for 'a break completion or a throw completion', which is kind of a silly union; maybe address that in some other way?
+    const isCompletion =
+      returnType.kind === 'completion' ||
+      (returnType.kind === 'union' && returnType.types[0].kind === 'completion');
+    if (
+      ['Completion', 'ThrowCompletion', 'NormalCompletion', 'ReturnCompletion'].includes(calleeName)
+    ) {
+      if (consumedAsCompletion) {
+        warn(
+          callee[0].location.start.offset,
+          `${calleeName} clearly creates a Completion Record; it does not need to be marked as such, and it would not be useful to immediately unwrap its result`,
+        );
+      }
+    } else if (isCompletion && !consumedAsCompletion) {
+      warn(
+        callee[0].location.start.offset,
+        `${calleeName} returns a Completion Record, but is not consumed as if it does`,
+      );
+    } else if (!isCompletion && consumedAsCompletion) {
+      warn(
+        callee[0].location.start.offset,
+        `${calleeName} does not return a Completion Record, but is consumed as if it does`,
+      );
+    }
+    if (returnType.kind === 'unused' && !isCalledAsPerform(expr, path, false)) {
+      warn(
+        callee[0].location.start.offset,
+        `${calleeName} does not return a meaningful value and should only be invoked as \`Perform ${calleeName}(...).\``,
+      );
+    }
+
+    if (onlyPerformed.has(calleeName) && onlyPerformed.get(calleeName) !== 'top') {
+      const old = onlyPerformed.get(calleeName);
+      const performed = isCalledAsPerform(expr, path, true);
+      if (!performed) {
+        onlyPerformed.set(calleeName, 'top');
+      } else if (old === null) {
+        onlyPerformed.set(calleeName, 'only performed');
+      }
+    }
+    if (
+      alwaysAssertedToBeNormal.has(calleeName) &&
+      alwaysAssertedToBeNormal.get(calleeName) !== 'top'
+    ) {
+      const old = alwaysAssertedToBeNormal.get(calleeName);
+      const asserted = isAssertedToBeNormal(expr, path);
+      if (!asserted) {
+        alwaysAssertedToBeNormal.set(calleeName, 'top');
+      } else if (old === null) {
+        alwaysAssertedToBeNormal.set(calleeName, 'always asserted normal');
+      }
+    }
+  };
 
 export function typecheck(spec: Spec) {
   const isUnused = (t: BiblioType) =>
@@ -15,10 +187,10 @@ export function typecheck(spec: Spec) {
   const AOs = spec.biblio
     .localEntries()
     .filter(e => e.type === 'op' && e.signature?.return != null) as AlgorithmBiblioEntry[];
-  const onlyPerformed: Map<string, null | 'only performed' | 'top'> = new Map(
+  const onlyPerformed: OnlyPerformedMap = new Map(
     AOs.filter(e => !isUnused(e.signature!.return!)).map(a => [a.aoid, null]),
   );
-  const alwaysAssertedToBeNormal: Map<string, null | 'always asserted normal' | 'top'> = new Map(
+  const alwaysAssertedToBeNormal: AlwaysAssertedToBeNormalMap = new Map(
     // prettier-ignore
     AOs
       .filter(e => e.signature!.return!.kind === 'completion' && !e.skipGlobalChecks)
@@ -38,179 +210,23 @@ export function typecheck(spec: Spec) {
       continue;
     }
     const originalHtml = (node as AlgorithmElementWithTree).originalHtml;
-
-    const expressionVisitor = (expr: Expr, path: PathItem[]) => {
-      if (expr.name !== 'call' && expr.name !== 'sdo-call') {
-        return;
-      }
-
-      const { callee, arguments: args } = expr;
-      if (!(callee.length === 1 && callee[0].name === 'text')) {
-        return;
-      }
-      const calleeName = callee[0].contents;
-
-      const warn = (message: string) => {
-        const { line, column } = offsetToLineAndColumn(
-          originalHtml,
-          callee[0].location.start.offset,
-        );
-        spec.warn({
-          type: 'contents',
-          ruleId: 'typecheck',
-          message,
-          node,
-          nodeRelativeLine: line,
-          nodeRelativeColumn: column,
-        });
-      };
-
-      const biblioEntry = spec.biblio.byAoid(calleeName);
-      if (biblioEntry == null) {
-        if (!['toUppercase', 'toLowercase'].includes(calleeName)) {
-          // TODO make the spec not do this
-          warn(`could not find definition for ${calleeName}`);
-        }
-        return;
-      }
-
-      if (biblioEntry.kind === 'syntax-directed operation' && expr.name === 'call') {
-        warn(
-          `${calleeName} is a syntax-directed operation and should not be invoked like a regular call`,
-        );
-      } else if (
-        biblioEntry.kind != null &&
-        biblioEntry.kind !== 'syntax-directed operation' &&
-        expr.name === 'sdo-call'
-      ) {
-        warn(`${calleeName} is not a syntax-directed operation but here is being invoked as one`);
-      }
-
-      if (biblioEntry.signature == null) {
-        return;
-      }
-      const { signature } = biblioEntry;
-      const min = signature.parameters.length;
-      const max = min + signature.optionalParameters.length;
-      if (args.length < min || args.length > max) {
-        const count = `${min}${min === max ? '' : `-${max}`}`;
-        const message = `${calleeName} takes ${count} argument${count === '1' ? '' : 's'}, but this invocation passes ${args.length}`;
-        warn(message);
-      } else {
-        const params = signature.parameters.concat(signature.optionalParameters);
-        for (const [arg, param] of zip(args, params, true)) {
-          if (param.type == null) continue;
-          const argType = typeFromExpr(arg, spec.biblio);
-          const paramType = typeFromExprType(param.type);
-
-          // often we can't infer the argument precisely, so we check only that the intersection is nonempty rather than that the argument type is a subtype of the parameter type
-          const intersection = meet(argType, paramType);
-
-          if (
-            intersection.kind === 'never' ||
-            (intersection.kind === 'list' &&
-              intersection.of.kind === 'never' &&
-              // if the meet is list<never>, and we're passing a concrete list, it had better be empty
-              argType.kind === 'list' &&
-              argType.of.kind !== 'never')
-          ) {
-            const items = stripWhitespace(arg.items);
-            const { line, column } = offsetToLineAndColumn(
-              originalHtml,
-              items[0].location.start.offset,
-            );
-            const argDescriptor =
-              argType.kind.startsWith('concrete') ||
-              argType.kind === 'enum value' ||
-              argType.kind === 'null' ||
-              argType.kind === 'undefined'
-                ? `(${serialize(argType)})`
-                : `type (${serialize(argType)})`;
-
-            let hint = '';
-            if (argType.kind === 'concrete number' && dominates({ kind: 'real' }, paramType)) {
-              hint =
-                '\nhint: you passed an ES language Number, but this position takes a mathematical value';
-            } else if (
-              argType.kind === 'concrete real' &&
-              dominates({ kind: 'number' }, paramType)
-            ) {
-              hint =
-                '\nhint: you passed a mathematical value, but this position takes an ES language Number';
-            } else if (
-              argType.kind === 'concrete real' &&
-              dominates({ kind: 'bigint' }, paramType)
-            ) {
-              hint =
-                '\nhint: you passed a mathematical value, but this position takes an ES language BigInt';
-            }
-
-            spec.warn({
-              type: 'contents',
-              ruleId: 'typecheck',
-              message: `argument ${argDescriptor} does not look plausibly assignable to parameter type (${serialize(paramType)})${hint}`,
-              node,
-              nodeRelativeLine: line,
-              nodeRelativeColumn: column,
-            });
-          }
-        }
-      }
-
-      const { return: returnType } = signature;
-      if (returnType == null) {
-        return;
-      }
-
-      const consumedAsCompletion = isConsumedAsCompletion(expr, path);
-
-      // checks elsewhere ensure that well-formed documents never have a union of completion and non-completion, so checking the first child suffices
-      // TODO: this is for 'a break completion or a throw completion', which is kind of a silly union; maybe address that in some other way?
-      const isCompletion =
-        returnType.kind === 'completion' ||
-        (returnType.kind === 'union' && returnType.types[0].kind === 'completion');
-      // prettier-ignore
-      if (['Completion', 'ThrowCompletion', 'NormalCompletion', 'ReturnCompletion'].includes(calleeName)) {
-        if (consumedAsCompletion) {
-          warn(
-            `${calleeName} clearly creates a Completion Record; it does not need to be marked as such, and it would not be useful to immediately unwrap its result`,
-          );
-        }
-      } else if (isCompletion && !consumedAsCompletion) {
-        warn(`${calleeName} returns a Completion Record, but is not consumed as if it does`);
-      } else if (!isCompletion && consumedAsCompletion) {
-        warn(`${calleeName} does not return a Completion Record, but is consumed as if it does`);
-      }
-      if (returnType.kind === 'unused' && !isCalledAsPerform(expr, path, false)) {
-        warn(
-          `${calleeName} does not return a meaningful value and should only be invoked as \`Perform ${calleeName}(...).\``,
-        );
-      }
-
-      if (onlyPerformed.has(calleeName) && onlyPerformed.get(calleeName) !== 'top') {
-        const old = onlyPerformed.get(calleeName);
-        const performed = isCalledAsPerform(expr, path, true);
-        if (!performed) {
-          onlyPerformed.set(calleeName, 'top');
-        } else if (old === null) {
-          onlyPerformed.set(calleeName, 'only performed');
-        }
-      }
-      if (
-        alwaysAssertedToBeNormal.has(calleeName) &&
-        alwaysAssertedToBeNormal.get(calleeName) !== 'top'
-      ) {
-        const old = alwaysAssertedToBeNormal.get(calleeName);
-        const asserted = isAssertedToBeNormal(expr, path);
-        if (!asserted) {
-          alwaysAssertedToBeNormal.set(calleeName, 'top');
-        } else if (old === null) {
-          alwaysAssertedToBeNormal.set(calleeName, 'always asserted normal');
-        }
-      }
+    const warn = (offset: number, message: string) => {
+      const { line, column } = offsetToLineAndColumn(originalHtml, offset);
+      spec.warn({
+        type: 'contents',
+        ruleId: 'typecheck',
+        message,
+        node,
+        nodeRelativeLine: line,
+        nodeRelativeColumn: column,
+      });
     };
+
     const walkLines = (list: OrderedListNode) => {
       for (const line of list.contents) {
+        // we already parsed in collect-algorithm-diagnostics, but that was before generating the biblio
+        // the biblio affects the parse of calls, so we need to re-do it
+        // TODO do collect-algorithm-diagnostics after generating the biblio, somehow?
         const item = parseExpr(line.contents, opNames);
         if (item.name === 'failure') {
           const { line, column } = offsetToLineAndColumn(originalHtml, item.offset);
@@ -223,7 +239,7 @@ export function typecheck(spec: Spec) {
             nodeRelativeColumn: column,
           });
         } else {
-          walkExpr(expressionVisitor, item);
+          walkExpr(getExpressionVisitor(spec, warn, onlyPerformed, alwaysAssertedToBeNormal), item);
         }
         if (line.sublist?.name === 'ol') {
           walkLines(line.sublist);
@@ -361,537 +377,3 @@ function textFromPreviousPart(seq: Seq, index: number): string | null {
   }
   return text;
 }
-
-function stripWhitespace(items: NonSeq[]) {
-  items = [...items];
-  while (items[0]?.name === 'text' && /^\s+$/.test(items[0].contents)) {
-    items.shift();
-  }
-  while (
-    items[items.length - 1]?.name === 'text' &&
-    // @ts-expect-error
-    /^\s+$/.test(items[items.length - 1].contents)
-  ) {
-    items.pop();
-  }
-  return items;
-}
-
-type Type =
-  | { kind: 'unknown' } // top
-  | { kind: 'never' } // bottom
-  | { kind: 'union'; of: NonUnion[] } // constraint: nothing in the union dominates anything else in the union
-  | { kind: 'list'; of: Type }
-  | { kind: 'record' } // TODO more precision
-  | { kind: 'completion'; of: Type }
-  | { kind: 'real' }
-  | { kind: 'integer' }
-  | { kind: 'non-negative integer' }
-  | { kind: 'negative integer' }
-  | { kind: 'positive integer' }
-  | { kind: 'concrete real'; value: string }
-  | { kind: 'ES value' }
-  | { kind: 'string' }
-  | { kind: 'number' }
-  | { kind: 'integral number' }
-  | { kind: 'bigint' }
-  | { kind: 'boolean' }
-  | { kind: 'null' }
-  | { kind: 'undefined' }
-  | { kind: 'concrete string'; value: string }
-  | { kind: 'concrete number'; value: number }
-  | { kind: 'concrete bigint'; value: bigint }
-  | { kind: 'concrete boolean'; value: boolean }
-  | { kind: 'enum value'; value: string };
-
-type NonUnion = Exclude<Type, { kind: 'union' }>;
-
-const simpleKinds = new Set<Type['kind']>([
-  'unknown',
-  'never',
-  'record',
-  'real',
-  'integer',
-  'non-negative integer',
-  'negative integer',
-  'positive integer',
-  'ES value',
-  'string',
-  'number',
-  'integral number',
-  'bigint',
-  'boolean',
-  'null',
-  'undefined',
-]);
-
-const dominateGraph: Partial<Record<Type['kind'], Type['kind'][]>> = {
-  // @ts-expect-error TS does not know about __proto__
-  __proto__: null,
-  record: ['completion'],
-  real: [
-    'integer',
-    'non-negative integer',
-    'negative integer',
-    'positive integer',
-    'concrete real',
-  ],
-  integer: ['non-negative integer', 'negative integer', 'positive integer'],
-  'non-negative integer': ['positive integer'],
-  'ES value': [
-    'string',
-    'number',
-    'integral number',
-    'bigint',
-    'boolean',
-    'null',
-    'undefined',
-    'concrete string',
-    'concrete number',
-    'concrete bigint',
-    'concrete boolean',
-  ],
-  string: ['concrete string'],
-  number: ['integral number', 'concrete number'],
-  bigint: ['concrete bigint'],
-  boolean: ['concrete boolean'],
-};
-
-/*
-The type lattice used here is very simple (aside from explicit unions).
-As such we mostly only need to define the `dominates` relationship and apply trivial rules:
-if `x` dominates `y`, then `join(x,y) = x` and `meet(x,y) = y`; if neither dominates the other than the join is top and the meet is bottom.
-Unions/lists/completions take a little more work.
-*/
-
-function dominates(a: Type, b: Type): boolean {
-  if (a.kind === 'unknown' || b.kind === 'never') {
-    return true;
-  }
-  if (b.kind === 'union') {
-    return b.of.every(t => dominates(a, t));
-  }
-  if (a.kind === 'union') {
-    // not necessarily true for arbitrary lattices, but true for ours
-    return a.of.some(t => dominates(t, b));
-  }
-  if (
-    (a.kind === 'list' && b.kind === 'list') ||
-    (a.kind === 'completion' && b.kind === 'completion')
-  ) {
-    return dominates(a.of, b.of);
-  }
-  if (simpleKinds.has(a.kind) && simpleKinds.has(b.kind) && a.kind === b.kind) {
-    return true;
-  }
-  if (dominateGraph[a.kind]?.includes(b.kind) ?? false) {
-    return true;
-  }
-  if (a.kind === 'integer' && b.kind === 'concrete real') {
-    return !b.value.includes('.');
-  }
-  if (a.kind === 'integral number' && b.kind === 'concrete number') {
-    return Number.isFinite(b.value) && b.value === Math.round(b.value);
-  }
-  if (a.kind === 'non-negative integer' && b.kind === 'concrete real') {
-    return !b.value.includes('.') && b.value[0] !== '-';
-  }
-  if (a.kind === 'negative integer' && b.kind === 'concrete real') {
-    return !b.value.includes('.') && b.value[0] === '-';
-  }
-  if (a.kind === 'positive integer' && b.kind === 'concrete real') {
-    return !b.value.includes('.') && b.value[0] !== '-' && b.value !== '0';
-  }
-  if (
-    a.kind === b.kind &&
-    [
-      'concrete string',
-      'concrete number',
-      'concrete real',
-      'concrete bigint',
-      'concrete boolean',
-      'enum value',
-    ].includes(a.kind)
-  ) {
-    // @ts-expect-error TS is not quite smart enough for this
-    return Object.is(a.value, b.value);
-  }
-  return false;
-}
-
-function addToUnion(types: NonUnion[], type: NonUnion): Type {
-  if (types.some(t => dominates(t, type))) {
-    return { kind: 'union', of: types };
-  }
-  const live = types.filter(t => !dominates(type, t));
-  if (live.length === 0) {
-    return type;
-  }
-  return { kind: 'union', of: [...live, type] };
-}
-
-export function join(a: Type, b: Type): Type {
-  if (dominates(a, b)) {
-    return a;
-  }
-  if (dominates(b, a)) {
-    return b;
-  }
-  if (b.kind === 'union') {
-    [a, b] = [b, a];
-  }
-  if (a.kind === 'union') {
-    if (b.kind === 'union') {
-      return b.of.reduce(
-        (acc: Type, t) => (acc.kind === 'union' ? addToUnion(acc.of, t) : join(acc, t)),
-        a,
-      );
-    }
-    return addToUnion(a.of, b);
-  }
-  if (
-    (a.kind === 'list' && b.kind === 'list') ||
-    (a.kind === 'completion' && b.kind === 'completion')
-  ) {
-    return { kind: a.kind, of: join(a.of, b.of) };
-  }
-  return { kind: 'union', of: [a, b as NonUnion] };
-}
-
-export function meet(a: Type, b: Type): Type {
-  if (dominates(a, b)) {
-    return b;
-  }
-  if (dominates(b, a)) {
-    return a;
-  }
-  if (a.kind !== 'union' && b.kind === 'union') {
-    [a, b] = [b, a];
-  }
-  if (a.kind === 'union') {
-    // union is join. meet distributes over join.
-    return a.of.map(t => meet(t, b)).reduce(join);
-  }
-  if (
-    (a.kind === 'list' && b.kind === 'list') ||
-    (a.kind === 'completion' && b.kind === 'completion')
-  ) {
-    return { kind: a.kind, of: meet(a.of, b.of) };
-  }
-  return { kind: 'never' };
-}
-
-function serialize(type: Type): string {
-  switch (type.kind) {
-    case 'unknown': {
-      return 'unknown';
-    }
-    case 'never': {
-      return 'never';
-    }
-    case 'union': {
-      const parts = type.of.map(serialize);
-      if (parts.length > 2) {
-        return parts.slice(0, -1).join(', ') + ', or ' + parts[parts.length - 1];
-      }
-      return parts[0] + ' or ' + parts[1];
-    }
-    case 'list': {
-      if (type.of.kind === 'never') {
-        return 'empty List';
-      }
-      return 'List of ' + serialize(type.of);
-    }
-    case 'record': {
-      return 'Record';
-    }
-    case 'completion': {
-      if (type.of.kind === 'never') {
-        return 'an abrupt Completion Record';
-      } else if (type.of.kind === 'unknown') {
-        return 'a Completion Record';
-      }
-      return 'a Completion Record normally holding ' + serialize(type.of);
-    }
-    case 'real': {
-      return 'mathematical value';
-    }
-    case 'integer':
-    case 'non-negative integer':
-    case 'negative integer':
-    case 'positive integer':
-    case 'null':
-    case 'undefined': {
-      return type.kind;
-    }
-    case 'concrete string': {
-      return `"${type.value}"`;
-    }
-    case 'concrete real': {
-      return type.value;
-    }
-    case 'concrete boolean': {
-      return `${type.value}`;
-    }
-    case 'enum value': {
-      return `~${type.value}~`;
-    }
-    case 'concrete number': {
-      if (Object.is(type.value, 0 / 0)) {
-        return '*NaN*';
-      }
-      let repr;
-      if (Object.is(type.value, -0)) {
-        repr = '-0';
-      } else if (type.value === 0) {
-        repr = '+0';
-      } else if (type.value === 2e308) {
-        repr = '+&infin;';
-      } else if (type.value === -2e308) {
-        repr = '-&infin;';
-      } else if (type.value > 4503599627370495.5) {
-        repr = String(BigInt(type.value));
-      } else {
-        repr = String(type.value);
-      }
-      return `*${repr}*<sub>𝔽</sub>`;
-    }
-    case 'concrete bigint': {
-      return `*${type.value}*<sub>ℤ</sub>`;
-    }
-    case 'ES value': {
-      return 'ECMAScript language value';
-    }
-    case 'boolean': {
-      return 'Boolean';
-    }
-    case 'string': {
-      return 'String';
-    }
-    case 'number': {
-      return 'Number';
-    }
-    case 'integral number': {
-      return 'integral Number';
-    }
-    case 'bigint': {
-      return 'BigInt';
-    }
-  }
-}
-
-export function typeFromExpr(expr: Expr, biblio: Biblio): Type {
-  seq: if (expr.name === 'seq') {
-    const items = stripWhitespace(expr.items);
-    if (items.length === 1) {
-      expr = items[0];
-      break seq;
-    }
-
-    if (
-      items.length === 2 &&
-      items[0].name === 'star' &&
-      items[0].contents[0].name === 'text' &&
-      items[1].name === 'text'
-    ) {
-      switch (items[1].contents) {
-        case '𝔽': {
-          const text = items[0].contents[0].contents;
-          let value;
-          if (text === '-0') {
-            value = -0;
-          } else if (text === '+&infin;') {
-            value = 2e308;
-          } else if (text === '-&infin;') {
-            value = -2e308;
-          } else {
-            value = parseFloat(text);
-          }
-          return { kind: 'concrete number', value };
-        }
-        case 'ℤ': {
-          return { kind: 'concrete bigint', value: BigInt(items[0].contents[0].contents) };
-        }
-      }
-    }
-
-    if (items[0]?.name === 'text' && ['!', '?'].includes(items[0].contents.trim())) {
-      const remaining = stripWhitespace(items.slice(1));
-      if (remaining.length === 1 && ['call', 'sdo-call'].includes(remaining[0].name)) {
-        const callType = typeFromExpr(remaining[0], biblio);
-        if (callType.kind === 'completion') {
-          return callType.of;
-        }
-      }
-    }
-  }
-
-  switch (expr.name) {
-    case 'text': {
-      const text = expr.contents.trim();
-      if (/^-?[0-9]+(\.[0-9]+)?$/.test(text)) {
-        return { kind: 'concrete real', value: text };
-      }
-      break;
-    }
-    case 'list': {
-      return {
-        kind: 'list',
-        of: expr.elements.map(t => typeFromExpr(t, biblio)).reduce(join, { kind: 'never' }),
-      };
-    }
-    case 'record': {
-      return { kind: 'record' };
-    }
-    case 'call':
-    case 'sdo-call': {
-      const { callee } = expr;
-      if (!(callee.length === 1 && callee[0].name === 'text')) {
-        break;
-      }
-      const calleeName = callee[0].contents;
-
-      const biblioEntry = biblio.byAoid(calleeName);
-      if (biblioEntry?.signature?.return == null) {
-        break;
-      }
-      return typeFromExprType(biblioEntry.signature.return);
-    }
-    case 'tilde': {
-      if (expr.contents.length === 1 && expr.contents[0].name === 'text') {
-        return { kind: 'enum value', value: expr.contents[0].contents };
-      }
-      break;
-    }
-    case 'star': {
-      if (expr.contents.length === 1 && expr.contents[0].name === 'text') {
-        const text = expr.contents[0].contents;
-        if (text === 'null') {
-          return { kind: 'null' };
-        } else if (text === 'undefined') {
-          return { kind: 'undefined' };
-        } else if (text === 'NaN') {
-          return { kind: 'concrete number', value: 0 / 0 };
-        } else if (text === 'true') {
-          return { kind: 'concrete boolean', value: true };
-        } else if (text === 'false') {
-          return { kind: 'concrete boolean', value: false };
-        } else if (text.startsWith('"') && text.endsWith('"')) {
-          return { kind: 'concrete string', value: text.slice(1, -1) };
-        }
-      }
-
-      break;
-    }
-  }
-  return { kind: 'unknown' };
-}
-
-function typeFromExprType(type: BiblioType): Type {
-  switch (type.kind) {
-    case 'union': {
-      return type.types.map(typeFromExprType).reduce(join);
-    }
-    case 'list': {
-      return {
-        kind: 'list',
-        of: type.elements == null ? { kind: 'unknown' } : typeFromExprType(type.elements),
-      };
-    }
-    case 'completion': {
-      if (type.completionType === 'abrupt') {
-        return { kind: 'completion', of: { kind: 'never' } };
-      }
-      return {
-        kind: 'completion',
-        of:
-          type.typeOfValueIfNormal == null
-            ? { kind: 'unknown' }
-            : typeFromExprType(type.typeOfValueIfNormal),
-      };
-    }
-    case 'opaque': {
-      const text = type.type;
-      if (text.startsWith('"') && text.endsWith('"')) {
-        return { kind: 'concrete string', value: text.slice(1, -1) };
-      }
-      if (text.startsWith('~') && text.endsWith('~')) {
-        return { kind: 'enum value', value: text.slice(1, -1) };
-      }
-      if (/^-?[0-9]+(\.[0-9]+)?$/.test(text)) {
-        return { kind: 'concrete real', value: text };
-      }
-      if (text.startsWith('*') && text.endsWith('*<sub>𝔽</sub>')) {
-        const innerText = text.slice(1, -14);
-        let value;
-        if (innerText === '-0') {
-          value = -0;
-        } else if (innerText === '+&infin;') {
-          value = 2e308;
-        } else if (innerText === '-&infin;') {
-          value = -2e308;
-        } else {
-          value = parseFloat(innerText);
-        }
-        return { kind: 'concrete number', value };
-      }
-      if (text === '*NaN*') {
-        return { kind: 'concrete number', value: 0 / 0 };
-      }
-      if (text.startsWith('*') && text.endsWith('*<sub>ℤ</sub>')) {
-        return { kind: 'concrete bigint', value: BigInt(text.slice(1, -14)) };
-      }
-      if (text === 'an ECMAScript language value' || text === 'ECMAScript language values') {
-        return { kind: 'ES value' };
-      }
-      if (text === 'a String' || text === 'Strings') {
-        return { kind: 'string' };
-      }
-      if (text === 'a Number' || text === 'Numbers') {
-        return { kind: 'number' };
-      }
-      if (text === 'a Boolean' || text === 'Booleans') {
-        return { kind: 'boolean' };
-      }
-      if (text === 'a BigInt' || text === 'BigInts') {
-        return { kind: 'bigint' };
-      }
-      if (text === 'an integral Number' || text === 'integral Numbers') {
-        return { kind: 'integral number' };
-      }
-      if (text === 'a mathematical value' || text === 'mathematical values') {
-        return { kind: 'real' };
-      }
-      if (text === 'an integer' || text === 'integers') {
-        return { kind: 'integer' };
-      }
-      if (text === 'a non-negative integer' || text === 'non-negative integers') {
-        return { kind: 'non-negative integer' };
-      }
-      if (text === 'a negative integer' || text === 'negative integers') {
-        return { kind: 'negative integer' };
-      }
-      if (text === 'a positive integer' || text === 'positive integers') {
-        return { kind: 'positive integer' };
-      }
-      if (text === 'a time value' || text === 'time values') {
-        return {
-          kind: 'union',
-          of: [{ kind: 'integral number' }, { kind: 'concrete number', value: 0 / 0 }],
-        };
-      }
-      if (text === '*null*') {
-        return { kind: 'null' };
-      }
-      if (text === '*undefined*') {
-        return { kind: 'undefined' };
-      }
-      break;
-    }
-    case 'unused': {
-      // this is really only a return type, but might as well handle it
-      return { kind: 'enum value', value: '~unused~' };
-    }
-  }
-  return { kind: 'unknown' };
-}
diff --git a/test/typecheck.js b/test/typecheck.js
index 90d33cec..a1be0d57 100644
--- a/test/typecheck.js
+++ b/test/typecheck.js
@@ -1511,7 +1511,7 @@ describe('type system', () => {
     await assertTypeError(
       'an ECMAScript language value',
       'NormalCompletion(42)',
-      'argument type (a Completion Record) does not look plausibly assignable to parameter type (ECMAScript language value)',
+      'argument type (a normal completion) does not look plausibly assignable to parameter type (ECMAScript language value)',
       [completionBiblio],
     );
 
@@ -1528,14 +1528,14 @@ describe('type system', () => {
     await assertTypeError(
       'either a normal completion containing a Boolean or an abrupt completion',
       '*false*',
-      'argument (false) does not look plausibly assignable to parameter type (a Completion Record normally holding Boolean)',
+      'argument (false) does not look plausibly assignable to parameter type (a normal completion containing Boolean or an abrupt completion)',
       [completionBiblio],
     );
 
     await assertTypeError(
       'a Boolean',
       'NormalCompletion(*false*)',
-      'argument type (a Completion Record) does not look plausibly assignable to parameter type (Boolean)',
+      'argument type (a normal completion) does not look plausibly assignable to parameter type (Boolean)',
       [completionBiblio],
     );