Add gradual-typing elaboration to Laurel resolution#1422
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.
| /-- 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 |
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
There was a problem hiding this comment.
sure, like a canonical HighType.Dyn constructor in LaurelAST.lean?
| /-- 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 }) |
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 ?
| /-- 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 |
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
There was a problem hiding this comment.
I'll ask kiro to check if you have something similar to extract a helper !
| -- 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 |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
yeah let's discuss it monday
| /-- Substring containment. -/ | ||
| private def containsSubstr (haystack needle : String) : Bool := | ||
| (haystack.splitOn needle).length > 1 |
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 ?
2 participants
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.