check: a `where` clause with a concrete subject, and `into()` under an `Into` bound #748

New issue

Open

opened 2026-11-13 12:39:37 +00:00 by orion · 0 comments

orion commented

2026-11-13 12:39:37 +00:00

Collaborator

Context

docs/TYPECHECKER.md section 9 ends one gap with "two neighbouring holes stay open", and no issue tracks them:

path.into() under a bound <Source: Into<Path>> type checks and reaches neither back end.
A where clause whose subject is a concrete type is not honoured: fn open<Source>(path: Source): Path where Path: From<Source> { Path.from path } answers "Path has no member from".

Both are the generic form of the conversion pair the standard library uses everywhere (From, Into), so a library author meets them early.

Source

Cleanup audit 2026-11 (#742), finding F7; the report is docs/project/2026-11-cleanup-audit.md.
docs/TYPECHECKER.md section 9, the gap that names the two holes.

Goal

Both programs type check and run on tier A and tier B, or the checker refuses each with a message that names the rule. A program that type checks and cannot be built is not an outcome.

Design record point

docs/TYPECHECKER.md section 9 (the gap and its neighbours); CONCEPT, the sections on where clauses and on From and Into.

Acceptance criteria

Hole 1: a conformance program calls into() under an Into bound and runs on both tiers, or a checker test pins the refusal
Hole 2: a where clause with a concrete subject brings the members of the bound into scope for that type, pinned by a checker test and a conformance program, or is refused where it is written
The spec gap is updated: the sentence "two neighbouring holes stay open" goes, each hole has its _Decision: line
The four gates and the fixpoint are green

Dependencies

None. The two holes may be two PRs.

Seed

None.

Size

One or two PRs, one commit each.

## Context `docs/TYPECHECKER.md` section 9 ends one gap with "two neighbouring holes stay open", and no issue tracks them: 1. `path.into()` under a bound `<Source: Into<Path>>` type checks and reaches neither back end. 2. A `where` clause whose subject is a concrete type is not honoured: `fn open<Source>(path: Source): Path where Path: From<Source> { Path.from path }` answers "`Path` has no member `from`". Both are the generic form of the conversion pair the standard library uses everywhere (`From`, `Into`), so a library author meets them early. ## Source - Cleanup audit 2026-11 (#742), finding F7; the report is `docs/project/2026-11-cleanup-audit.md`. - `docs/TYPECHECKER.md` section 9, the gap that names the two holes. ## Goal Both programs type check and run on tier A and tier B, or the checker refuses each with a message that names the rule. A program that type checks and cannot be built is not an outcome. ## Design record point `docs/TYPECHECKER.md` section 9 (the gap and its neighbours); CONCEPT, the sections on `where` clauses and on `From` and `Into`. ## Acceptance criteria - [ ] Hole 1: a conformance program calls `into()` under an `Into` bound and runs on both tiers, or a checker test pins the refusal - [ ] Hole 2: a `where` clause with a concrete subject brings the members of the bound into scope for that type, pinned by a checker test and a conformance program, or is refused where it is written - [ ] The spec gap is updated: the sentence "two neighbouring holes stay open" goes, each hole has its `_Decision:` line - [ ] The four gates and the fixpoint are green ## Dependencies None. The two holes may be two PRs. ## Seed None. ## Size One or two PRs, one commit each.

orion added the

loop

label

2026-11-13 12:39:37 +00:00

orion referenced this issue

2026-11-13 12:41:38 +00:00

cleanup: 2026-11 audit plan (epic) #742