Add dialect_option typecheck off to bypass DDM type checker

[joehendrix]

Summary

The DDM type checker uses unification to infer implicit type arguments, but this fails in some cases — notably when template-generated accessors with unresolved tvar return types are composed with polymorphic functions. This PR adds a per-dialect option to bypass type checking entirely, filling implicit type parameter slots with anonymous type placeholders instead.

How to use

In a dialect definition, add dialect_option typecheck off; to disable type checking for all programs using that dialect:

#dialect
dialect MyDialect;
dialect_option typecheck off;

type Foo;
fn bar (A : Type, x : A) : A => x;
...
#end

Programs using the dialect will skip inferType and unifyTypes for expression arguments. Variable name resolution and global context population still work normally — only type inference is bypassed.

Test changes

StrataTest/DDM/TypecheckSkip.lean defines an inline dialect with parameterized types, polymorphic functions, and perField accessor templates. It demonstrates that the accessor-into-polymorphic-fn pattern (from issue #650 / PR #734) produces type errors with typecheck on, and elaborates successfully with typecheck off.

Details

• AST.lean: Add TypeExprF.skip (anonymous type placeholder .tvar loc ""), Dialect.typecheck : Bool := true, refactor Program.globalContext into explicit computeGlobalContext function
• Elab/Core.lean: Add ElabContext.typecheck, skip inferType/unifyTypes in elabSyntaxArg, fill unfilled type param slots in runSyntaxElaborator post-pass, skip pre-registration in elabOperation, fix applyNArgs to handle tvar types
• Elab/DeclM.lean: Add DeclContext.typecheck
• Elab/DialectM.lean: Add elabSetOptionCommand handler dispatching on "typecheck" option
• BuiltinDialects/StrataDDL.lean: Add setOptionCommand with syntax dialect_option <name> <value> ;
• Elab.lean: Thread Dialect.typecheck into DeclContext in elabProgramRest
• Ion.lean, Python/Specs/DDM.lean: Update Program construction for globalContext refactor

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[tautschnig]

I'm concerned about the shape of the feature (not any specific details of the implementation). dialect_option typecheck off; is an escape hatch around a type-checker bug we don't yet understand. Merging this is fine and pragmatic, but I'd push for the following so the escape hatch doesn't silently become permanent technical debt:

1. File a tracking issue for the underlying type-checker bug. The PR description mentions "accessor-into-polymorphic-fn" as the specific failure mode from #650/#734, but there's no issue with "remove typecheck off once the root cause is fixed". Without that, any future user who hits a type error is going to reach for typecheck off as a Band-Aid, and we won't have a way to tell whether the root cause has been addressed.

2. Document which categories of program are expected to need this. The test file (TypecheckSkip.lean) names exactly one shape (accessor → polymorphic fn). If that's the only expected use, say so in the DDM manual. If there are others, enumerate them.

3. Warn about typecheck off's blast radius in the docs. docs/verso/DDMDoc.lean says only what the option does, not what it doesn't do. With typecheck off, a program with a genuine type error (e.g., passing a Lst Inte where Inte is expected) will elaborate silently. Downstream consumers — the VC generator, the symbolic evaluator, the SMT encoder — will then encounter the type error and produce confusing diagnostics ("Expression has type X when Y expected" at an IR level the user hasn't seen) or, worse, will silently proceed with ill-typed terms. A paragraph in the doc saying "turning this off means type errors surface at later pipeline stages with less-helpful messages" is fair warning.

4. Audit applyNArgs's new .tvar case — it's a general change, not gated on typecheck. At Elab/Core.lean:114-117, the new branch

   | .tvar ann _ =>
     let placeholder := .placeholder ann
     let tvars := Array.replicate (n - args.size) placeholder
     .ok (⟨args ++ tvars, by simp [tvars]; omega⟩, placeholder)

   runs regardless of the typecheck flag. Previously the function errored on tvar; now it produces placeholder arguments. This means programs elaborated with typecheck = true (the default) can now succeed where they previously errored — the broadening is not confined to the opt-in path. Is that intended? If so, worth a comment; if not, gate on (← read).typecheck.

5. Program.globalContext refactor is a cleanly-scoped improvement — removing the panic-in-default and exposing computeGlobalContext + Program.create is strictly better. I verified no other callers in-tree reach into Program.mk directly after this change. Good.

Test coverage:

The one test file covers the positive case (typecheck-off succeeds where typecheck-on fails). Missing cases that would pin the feature's behaviour:

• Negative test: typecheck off still catches unresolved identifiers. The PR description promises "Variable name resolution and global context population still work normally — only type inference is bypassed". A test that demonstrates an undefined identifier (e.g., assert [t]: undefined_name == 0;) still fails under typecheck off would pin this contract.
• Test: typecheck off across a dialect import boundary. What happens when a typecheck = true dialect imports a typecheck = false dialect? elabProgramRest threads d.typecheck into DeclContext — where d is the primary dialect. So the imported dialect's flag is ignored. Worth a test (and a docstring note) to pin this semantics.
• Test: invalid dialect_option values fail cleanly. dialect_option typecheck maybe; or dialect_option nonsense on; should produce the explicit "expected 'on' or 'off'" / "Unknown option" errors — worth a #guard_msgs fixture to lock those error messages.
• Test: option flag survives Ion round-trip. A DDM program with typecheck off serialized to Ion and re-read should preserve the flag. If it doesn't, the typecheck field may need serialization support.

Proof-coverage suggestions:

Three small theorems pinning the load-bearing invariants:

/-- `placeholder` is definitionally a `tvar` with empty name. -/
@[simp] theorem TypeExprF.placeholder_def {α} (loc : α) :
    TypeExprF.placeholder loc = TypeExprF.tvar loc "" := rfl

/-- `applyNArgs` on any tvar produces exactly `n` placeholder-typed
    arguments — contract for the new `.tvar` branch. -/
theorem applyNArgs_tvar_placeholder
    (tctx : TypingContext) (ann : _) (name : String) (n : Nat) :
    applyNArgs tctx (.tvar ann name) n =
    .ok (Vector.replicate n (.placeholder ann), .placeholder ann) := by
  cases n <;> simp [applyNArgs, applyNArgs.aux, …]

/-- Elaboration with `typecheck = false` still rejects unresolved
    identifier references (only type unification is bypassed). -/
theorem elabProgram_typecheck_off_preserves_resolution
    (d : Dialect) (h : d.typecheck = false) (cmds : Array Operation) :
    elabProgram d cmds = .ok p →
    ∀ op ∈ p.commands, ∀ id ∈ op.idents, identResolves p.globalContext id

The first is trivial; the second locks the new branch; the third is the user-visible contract ("name resolution still works") the PR description promises. Even as sorry-terminated stubs these would make the contract explicit.

Refactor / style:

• elabSyntaxArg has three copies of if !typecheck then return trees.set argIdx (some tree) at :1174, :1195 (and conceptually a third for the unnamed preType arm). A tiny helper

  private def bypassIfTypecheckOff (tree : Tree) (trees : …) : ElabM _ := do
    if !(← read).typecheck then return trees.set argIdx (some tree) else …

  would collapse the duplication and make future maintenance of the skip condition land in one place.
• elabSetOptionCommand uses a nested match on string pairs ("typecheck" × "on"/"off"). If more options are added, this will balloon. A DialectOption sum type with fromKeyValue : String → String → Except String DialectOption would centralize the parsing.
• dialect_option is a nice name, but the current implementation only recognizes one option (typecheck). If this is the only expected option long-term, consider a narrower syntax like @[typecheck off] dialect …. If more are coming, say so in a comment.
• Minor: TypeInfo construction at Elab/Core.lean:1266-1273 uses inputCtx := tctx0 (the initial context) rather than t.resultContext. That's intentional (the placeholder doesn't depend on earlier args) but worth a one-line comment — a reader stepping through the generic flow will expect the per-arg context.
• The renamed TypeExprF.skip → TypeExprF.placeholder (commit 9449f1c) is an improvement. The docstring now says "An anonymous type placeholder used when type checking is skipped." — but applyNArgs now uses placeholder regardless of the typecheck flag. Update the docstring:

  /-- An anonymous type placeholder (`.tvar loc ""`) used when a concrete type
      cannot be inferred — either because type checking is skipped at the
      dialect level, or because `applyNArgs` encountered a tvar where an
      arrow type was expected. -/
  

[joehendrix]

I'll take a look at more detail. But I'm going to react to this:

I'm concerned about the shape of the feature (not any specific details of the implementation). dialect_option typecheck off; is an escape hatch around a type-checker bug we don't yet understand.

In fact, I have a pretty good understanding of the issue #734 is a fix. However, there is a desire from the Strata Core folks to have this feature rather than expanding higher order type checking.

I'll look into the more detailed review soon, and I appreciate it, but I'm kind of stuck here. We have three options from my perspective:

1. Fix the bug (e.g., Resolve tvars in inferType's fvar case to fix panic on polymorphic accessor chains #734 or a better PR).
2. Leave as is and just panic (basically won't fix).
3. Provide an escape hatch (this PR).

At this point, I am just ashamed how much work is going into not fixing an issue. I'll review the PR comments, but if it's too much work, then I'm going to move to option 2.

[joscoh]

I disagree that this PR is problematic. I am fine mentioning this in the docs, but this option/escape hatch should be used when there is a separate typechecker that will be run on the resulting programs (as is the case for Core and Boole). It does not introduce any soundness/mistranslation issues, but rather reduces typechecking to a single function that can be reasoned about, avoiding some duplication.

[atomb]

I disagree that this PR is problematic. I am fine mentioning this in the docs, but this option/escape hatch should be used when there is a separate typechecker that will be run on the resulting programs (as is the case for Core and Boole). It does not introduce any soundness/mistranslation issues, but rather reduces typechecking to a single function that can be reasoned about, avoiding some duplication.

I second this.

[joehendrix]

Responding to the top-level review:

This isn't an escape hatch around a type-checker bug — it's a deliberate design choice. The Strata Core team implemented their own type checker downstream and doesn't want/need the DDM elaborator's type inference. They haven't ported everything away from Type/Expr at the DDM layer, and typecheck off enables that without issues. The DDM type system was always limited (tvars were already placeholders for "we don't know the type"), and this makes that explicit.

Re: the specific suggestions:

• Tracking issue — I don't think one is needed. This isn't a bug to fix; it's a deliberate opt-in for dialects that manage their own type checking downstream.
• Revert path — the feature is additive and backward-compatible (typecheck defaults to on), so reverting is straightforward if ever needed, but I don't expect it to be.
• Broader testing — covered by the fixtures added (see inline comment response on TypecheckSkip.lean).

[MikaelMayer]

🤖🔍 Overall this is a well-structured feature addition. The threading of the typecheck flag through the elaboration pipeline is clean, the Ion round-trip is handled correctly, and the test coverage demonstrates the core use case. A few items below.

Positives:

• The computeGlobalContext extraction is a good refactor — it makes Program.create the single place where the panic lives, and globalContext is now an explicit field rather than a computed default.
• The SymbolTable privacy hardening and the SystemSymbolIds.lean extraction are clean improvements.
• Test file is well-commented and covers the key scenarios (typecheck-on fails, typecheck-off succeeds, name resolution still works, invalid options error).

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

• Ion error messages now properly distinguish unknown options from invalid values (commit 994676a) ✅
• Pre-registration skip has an explanatory comment (commit 994676a) ✅
• Visibility changes and PySpecPipeline nit were informational only, no action needed ✅