diff --git a/src/type-logic.ts b/src/type-logic.ts index 7314e5f2..5034ff44 100644 --- a/src/type-logic.ts +++ b/src/type-logic.ts @@ -4,6 +4,7 @@ import type { Expr, NonSeq } from './expr-parser'; export type Type = | { kind: 'unknown' } // top + | { kind: 'unknown-non-enum' } // anything except an enum value | { kind: 'never' } // bottom | { kind: 'union'; of: NonUnion[] } // constraint: nothing in the union dominates anything else in the union | { kind: 'list'; of: Type } @@ -34,6 +35,7 @@ export type Type = type NonUnion = Exclude; const simpleKinds = new Set([ 'unknown', + 'unknown-non-enum', 'never', 'record', 'abrupt completion', @@ -97,13 +99,19 @@ export function dominates(a: Type, b: Type): boolean { if (a.kind === 'unknown' || b.kind === 'never') { return true; } + if (b.kind === 'unknown') { + return false; + } 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 + // not necessarily true for arbitrary lattices, but true for ours: our non-union types are join-prime, i.e., a union dominates such a type only if one of the members of the union dominates it return a.of.some(t => dominates(t, b)); } + if (a.kind === 'unknown-non-enum') { + return b.kind !== 'enum value'; + } if ( (a.kind === 'list' && b.kind === 'list') || (a.kind === 'normal completion' && b.kind === 'normal completion') @@ -233,6 +241,9 @@ export function serialize(type: Type): string { case 'unknown': { return 'unknown'; } + case 'unknown-non-enum': { + return 'unknown-non-enum'; + } case 'never': { return 'never'; } @@ -614,7 +625,7 @@ export function typeFromExprType(type: BiblioType): Type { return { kind: 'enum value', value: 'unused' }; } } - return { kind: 'unknown' }; + return { kind: 'unknown-non-enum' }; } export function isCompletion( diff --git a/test/type-logic.ts b/test/type-logic.ts new file mode 100644 index 00000000..ca38d1f8 --- /dev/null +++ b/test/type-logic.ts @@ -0,0 +1,19 @@ +import assert from 'node:assert'; +import { describe, it } from 'node:test'; +import { dominates, join } from '../lib/type-logic.js'; + +describe('type lattice', () => { + it('unknown-non-enum remains distinct from enums and genuine unknown', () => { + const unknown = { kind: 'unknown' } as const; + const unknownNonEnum = { kind: 'unknown-non-enum' } as const; + const empty = { kind: 'enum value', value: 'empty' } as const; + const unused = { kind: 'enum value', value: 'unused' } as const; + const unknownNonEnumOrEmpty = join(unknownNonEnum, empty); + + assert(dominates(unknown, unknownNonEnumOrEmpty)); + assert(!dominates(unknownNonEnumOrEmpty, unknown)); + assert(dominates(unknownNonEnumOrEmpty, unknownNonEnum)); + assert(dominates(unknownNonEnumOrEmpty, empty)); + assert(!dominates(unknownNonEnumOrEmpty, unused)); + }); +}); diff --git a/test/typecheck.ts b/test/typecheck.ts index f035668b..25b26bae 100644 --- a/test/typecheck.ts +++ b/test/typecheck.ts @@ -1751,8 +1751,16 @@ describe('type system', () => { "returned value (~iterate-strings~) does not look plausibly assignable to algorithm's return type (~sync~ or ~async~)", ); + await assertTypeError( + 'either a PrivateElement or ~empty~', + '~unused~', + 'argument (~unused~) does not look plausibly assignable to parameter type (unknown-non-enum or ~empty~)', + "returned value (~unused~) does not look plausibly assignable to algorithm's return type (unknown-non-enum or ~empty~)", + ); + await assertNoTypeError('~sync~ or ~async~', '~sync~'); await assertNoTypeError('~sync~ or ~async~', '~async~'); + await assertNoTypeError('either a PrivateElement or ~empty~', '~empty~'); }); it('boolean', async () => {