Add gradual-typing elaboration to Laurel resolution#1422
Closed
julesmt wants to merge 8 commits into
Closed
Conversation
Synth.primitiveOp inlined two match arms -- one for the arithmetic operators, one for the boolean / comparison / equality / concatenation families. Extract them into standalone nativeArith and nativeOther helpers (with an isArithmeticOp predicate and a joinAll LUB fold), and have Synth.primitiveOp resolve its operands once and dispatch to them. Pure refactor, no behavior change. Gives the native typing rules a single home so a later commit can reuse them as the fallback for gradual elaboration.
For datatype constructors, getCallInfo returned an empty parameter-type list, so constructor arguments were never checked against their declared types. Return ctor.args.map (.type) so a constructor call is type-checked like any other call. No behavior change for existing programs (their arguments already matched); this lets a later commit coerce constructor arguments under gradual typing.
Add an optional GradualConfig (a frontend's dynamic type, its boxing constructors, checked downcast accessors, per-operator prelude functions, and which procedures to elaborate). A gradualActive flag, set only inside a frontend's own procedures, gates a single dispatch in Synth.primitiveOp: when active, route operands through synthArith / synthOther, which keep a native operator when the operands are native and switch to the Any-prelude operator (inserting box / unbox / Any_to_bool coercions at boundaries), falling back to the native nativeArith / nativeOther rules; when inactive the native rules apply unchanged. Inert until a frontend supplies a config.
Add gradualConfig to LaurelTranslateOptions and pass it from LaurelCompilationPipeline into resolve by named argument. Defaults to none, so pipelines that supply no config are unaffected.
filterPrelude runs before elaboration, so the prelude calls it may insert are not yet referenced by the user program. Add extraSeeds (retained unconditionally) and a generic opSeed (Operation -> Option String) so an operator's prelude function is retained only when that operator appears. Inert without seeds.
leo-leesco
reviewed
Jun 26, 2026
Comment on lines
+144
to
+147
| /-- The dynamic type whose values are boxed (`TCore "Any"` for Python). -/ | ||
| dynamic : HighType | ||
| /-- Whether a type is the dynamic type (may have several spellings). -/ | ||
| isDynamic : HighType → Bool |
Contributor
There was a problem hiding this comment.
Design consideration : instead of threading this Dyn type in the resolution, can we imagine referencing it throughout the program?
In other words, do we expect Dyn to be source-language dependent ? This looks like a dependency inversion to me, if we were to add a new type to express the Dyn type, we could probably defer translating the source-language Dyn to Laurel's Dyn to the corresponding frontend
Member
Author
There was a problem hiding this comment.
sure, like a canonical HighType.Dyn constructor in LaurelAST.lean?
Comment on lines
+758
to
+763
| /-- LUB of the operand types, or `none` if inconsistent. -/ | ||
| private def joinAll (ctx : TypeLattice) (argTypes : List HighTypeMd) | ||
| (source : Option FileRange) : Option HighTypeMd := | ||
| argTypes.foldl | ||
| (fun acc t => match acc with | some l => join ctx l t | none => none) | ||
| (some { val := .Unknown, source := source }) |
Contributor
There was a problem hiding this comment.
just a warning : this is not yet an actual LUB (please update doc) as it does not walk any inheritance tree
join simply erases any Unknown if tried to merge with another static type. Can you look at join and see if it needs updating using your GradualConfig ?
Comment on lines
+780
to
+792
| /-- A `MultiValuedExpr` operand (a multi-output call used in value position) is | ||
| an internal pseudo-type with no Core lowering, so it must never reach an | ||
| operator slot — letting it through crashes a later pass as a `StrataBug`. | ||
| Emit the position-oriented diagnostic and return `true` so the caller | ||
| short-circuits to the operator's result type, suppressing cascades. -/ | ||
| private def reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Bool := do | ||
| match aTy.val with | ||
| | .MultiValuedExpr _ => | ||
| let diag := diagnosticFromSource a.source | ||
| "multi-output call cannot be used as a value here; it returns multiple values. Unpack it into separate variables first" | ||
| modify fun s => { s with errors := s.errors.push diag } | ||
| pure true | ||
| | _ => pure false |
Contributor
There was a problem hiding this comment.
I might be wrong, but I seem to remember the typechecker was already making the same kind of check ; if not we should move this helper function with the rest of the typechecker
Member
Author
There was a problem hiding this comment.
I'll ask kiro to check if you have something similar to extract a helper !
Member
Author
There was a problem hiding this comment.
at least I didn't find anything close, nor did Kiro, could you look ?
Contributor
There was a problem hiding this comment.
Looks like this is the same function : #1422 (comment)
| -- and return `true` so the caller short-circuits to the operator's natural | ||
| -- result type, suppressing the per-family check (and its cascading error) | ||
| -- on that operand. | ||
| let reportMultiValued (a : StmtExprMd) (aTy : HighTypeMd) : ResolveM Bool := do |
Contributor
There was a problem hiding this comment.
Contributor
There was a problem hiding this comment.
maybe we can discuss the location of this ? If it makes sense to move it, that's perfectly okay
Member
Author
There was a problem hiding this comment.
yeah let's discuss it monday
Comment on lines
+27
to
+29
| /-- Substring containment. -/ | ||
| private def containsSubstr (haystack needle : String) : Bool := | ||
| (haystack.splitOn needle).length > 1 |
Contributor
There was a problem hiding this comment.
[out of scope of this PR] : considering we have a similar helper function used to match annotations in tests, maybe we could factor both of them out ?
Addresses PR #1422 review (comment on gradualActive vs gradual.isSome). The reviewer's instinct was right that storing a derived boolean is a smell, but gradualActive cannot simply be gradual.isSome: it must also account for GradualConfig.shouldElaborate, which keeps elaboration out of hand-written prelude bodies and out of top-level (non-procedure) contexts. Replace the manually save/restored gradualActive : Bool with a meaningful currentProc : Option String (none = not inside a procedure body, mirroring answerType/instanceTypeName), and derive activeGradual as gradual.filter (currentProc.elim false shouldElaborate). Centralize the per-procedure save/restore in a withProc combinator, used by resolveProcedure and resolveInstanceProcedure. Behavior is unchanged.
Addresses PR #1422 review (join, line ~763). - Doc: join/joinAll are consistency merges, not a least upper bound (they do not walk the inheritance tree), so a none result means "cannot merge structurally", not "inconsistent". - Fix: join only erased .Unknown, but the dynamic type is .TCore (e.g. Any), which isConsistent treats as top while join did not. At the if-branch merge this made the inferred type order-dependent: 'if c then (e:Any) else (e:int)' inferred Any, but the swapped branches inferred int. Add .TCore absorbing arms so join agrees with isConsistent (dynamic wins), plus a symmetric-branch regression test. The operator path is unaffected (elaborateDynamicOp intercepts dynamic operands before join; nativeArith gates on isNumeric).
Addresses PR #1422 review (comment on the OpAlt docstring). Explain that an OpAlt is one candidate in the priority list firstElab walks (none = try next, some = commit), and add a concrete a + b walkthrough under synthArith: Any + Int commits via elaborateDynamicOp, String + String falls to strConcatAlt, and Int + Int falls through to the native Add. Doc-only.
Member
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds an optional
GradualConfigso resolution keeps native operators on native operands and routesAnyoperands through prelude operators, inserting box/unbox/toBoolcasts. Inert without a config; strict typingunchanged. Foundation for the stacked native typed-Python PR.