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. -/
  

[tautschnig]

Unconditional change. This new .tvar arm runs regardless of the typecheck flag — it's a general relaxation of applyNArgs, not part of the opt-in path. A typecheck = true program that previously errored with .error (args, .tvar _ _) will now succeed with placeholder arguments.

Is that deliberate? If the intent is to preserve existing behaviour for typecheck-on programs and only relax for typecheck-off:

Suggested change

	| .tvar ann _ =>
	let placeholder := .placeholder ann
	let tvars := Array.replicate (n - args.size) placeholder
	.ok (⟨args ++ tvars, by simp [tvars]; omega⟩, placeholder)
	| .tvar ann _ =>
	-- Producing placeholder arguments for tvars is required by the
	-- `typecheck off` path (so that arity-dependent slots can be filled
	-- without unification); it is also a relaxation for typecheck-on
	-- programs where `applyNArgs` previously errored. If this broader
	-- semantics is undesired outside the typecheck-off path, gate here.
	let placeholder := .placeholder ann
	let tvars := Array.replicate (n - args.size) placeholder
	.ok (⟨args ++ tvars, by simp [tvars]; omega⟩, placeholder)

Either way, a comment explaining the scope of the change would help — I reached for the PR description to discover that this was general.

A small proof to lock the contract of this branch (see the main review body):

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
  …

[tautschnig]

Two small improvements to make this scale as more options land:

1. Dispatch via a data-driven table. The nested match on ("typecheck", "on"/"off") is already two levels deep; a third option adds a third. Extract a DialectOption sum with fromKeyValue:

inductive DialectOption where
  | typecheck (value : Bool)

def DialectOption.fromKeyValue (key : String) (val : String)
    : Except String DialectOption :=
  match key, val with
  | "typecheck", "on" => .ok (.typecheck true)
  | "typecheck", "off" => .ok (.typecheck false)
  | "typecheck", v => .error s!"Expected 'on' or 'off' for option 'typecheck', got '{v}'."
  | key, _ => .error s!"Unknown option '{key}'."

def DialectOption.apply : DialectOption → Dialect → Dialect
  | .typecheck b, d => { d with typecheck := b }

Then elabSetOptionCommand is just a parse-then-apply pipeline and error messages live in one place.

2. Include the bad value in the error — currently the error "Expected 'on' or 'off' for option 'typecheck'." doesn't echo back what the user typed, which is less helpful than e.g. "Expected 'on' or 'off' for option 'typecheck', got 'maybe'.".

Also: add a #guard_msgs fixture to lock these error messages so a future rewrite doesn't silently change them — the tests in TypecheckSkip.lean only cover the successful off case.

[tautschnig]

The doc says what typecheck off does. It doesn't warn about what it doesn't do. Worth one paragraph covering the failure modes that are moved downstream:

Suggested change

	## Dialect Options
	Dialect options configure elaboration behavior for programs using the dialect.
	:::paragraph
	`dialect_option` _name_ _value_`;`
	Sets the dialect option _name_ to _value_.
	:::
	The following options are supported:
	- `typecheck` (`on` | `off`, default `on`): When set to `off`, the elaborator
	skips type inference and unification for expression arguments. Implicit type
	parameter slots are filled with anonymous type placeholders. Variable name
	resolution and global context population still operate normally.
	## Dialect Options
	Dialect options configure elaboration behavior for programs using the dialect.
	:::paragraph
	`dialect_option` _name_ _value_`;`
	Sets the dialect option _name_ to _value_.
	:::
	The following options are supported:
	- `typecheck` (`on` | `off`, default `on`): When set to `off`, the elaborator
	skips type inference and unification for expression arguments. Implicit type
	parameter slots are filled with anonymous type placeholders. Variable name
	resolution and global context population still operate normally.
	This is intended as a workaround for cases where the type checker cannot
	infer implicit type arguments — notably when template-generated accessors
	with unresolved tvar return types are composed with polymorphic functions
	(see issue #650).
	⚠️ With `typecheck off`, type errors in a program are not detected at
	elaboration. They will surface at later pipeline stages (VC generation,
	symbolic evaluation, SMT encoding) with less-helpful diagnostics, or — in
	the worst case — will silently produce ill-typed intermediate terms. Only
	use this flag when the elaboration error is known to be a type-checker
	limitation rather than a real type mismatch.

Without this paragraph, a user who turns the flag on because they saw it in an example is likely to discover the downside the hard way when their downstream pipeline fails opaquely.

[tautschnig]

The file covers the positive case (typecheck-off succeeds on the motivating shape). A few additional fixtures would pin the feature's contract:

1. Typecheck-off still catches unresolved identifiers — pin the "only type inference is bypassed" promise from the PR description:

   /-- Even with typecheck off, an undefined identifier must be rejected. -/
   /--
   error: Unknown identifier 'undefined_name'  -- or whatever the actual message is
   -/
   #guard_msgs in
   def typecheckOffStillCatchesUndefined :=
   #strata
   program TestTCOff;
   procedure Test () returns () {
     assert [t]: undefined_name == 0;
   };
   #end

2. Invalid option values produce clean errors:

   /-- `dialect_option typecheck maybe` should fail with the expected message. -/
   /-- error: Expected 'on' or 'off' for option 'typecheck'. -/
   #guard_msgs in
   #dialect
   dialect BadOption;
   dialect_option typecheck maybe;
   #end
   
   /-- `dialect_option nonsense on` should fail with the expected message. -/
   /-- error: Unknown option 'nonsense'. -/
   #guard_msgs in
   #dialect
   dialect BadOption2;
   dialect_option nonsense on;
   #end

3. Primary-dialect semantics across import boundary — what happens when TestTCOn (typecheck on) imports TestTCOff, or vice versa? elabProgramRest uses only the primary dialect's flag. Worth a fixture plus a one-line docstring where the flag is read.

4. Ion round-trip — if a dialect-with-typecheck-off is serialized to Ion and re-read, does the flag survive? I didn't see serialization support for Dialect.typecheck in the Ion changes. If it doesn't persist, that's a correctness gap for workflows that round-trip through Ion.

[tautschnig]

Update the docstring to reflect that placeholder is used in two places, not one:

Suggested change

	def placeholder {α} (loc : α) : TypeExprF α := .tvar loc ""
	/-- An anonymous type placeholder (`.tvar loc ""`) used when a concrete type
	cannot be inferred. Currently produced by:
	- `runSyntaxElaborator` post-pass when `typecheck off` leaves type slots unfilled,
	- `applyNArgs` when the type of the applied expression is itself a tvar
	(the latter runs regardless of the `typecheck` flag; see Elab/Core.lean:114).
	Represented as an unnamed tvar — compatible with `TypingContext.hnf`
	and `unifyTypes`, which treat empty-name tvars as fresh / matching-any. -/
	def placeholder {α} (loc : α) : TypeExprF α := .tvar loc ""

Also worth a trivial @[simp] definitional theorem so downstream proofs don't need to unfold:

@[simp] theorem placeholder_def {α} (loc : α) :
    placeholder loc = TypeExprF.tvar loc "" := rfl

[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.