Add gradual-typing elaboration to Laurel resolution

[julesmt]

Adds an optional GradualConfig so resolution keeps native operators on native operands and routes Any operands through prelude operators, inserting box/unbox/toBool casts. Inert without a config; strict typing unchanged. Foundation for the stacked native typed-Python PR.

---

Continuation of #1422. That PR was auto-closed by GitHub when its head branch was renamed to julesmt/feature/native-types/laurel (GitHub closes any open PR whose head branch is renamed). Same commits, same base.

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

Review (COMMENTED):

Great PR ! This goes really helps moving forward to lower Dyn type into Laurel
I wrote a few design considerations that we can discuss and asked for some modifications

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

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

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

sure, like a canonical HighType.Dyn constructor in LaurelAST.lean?

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

maybe another PR no ?

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

is there a benefit to having two fields as opposed to destructing gradual to Some _ | None ?
In other words, do we gain anything from not defining gradualActive = gradual.isSome() ?

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

I don't think so, at least without some refactoring.
So gradual tells us if gradual typing enabled globally and gradualActive tells us if the current procedure be elaborated. The latter is gradual.isSome && shouldElaborate(currentProc), so they are not equivalent. However, I agree it's not super elegant, let me see if we have something neeter.

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

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 ?

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

good catch

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

can you expand this docstring (eg providing an example) or provide an example in response to this thread ?

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

sure

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

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

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

I'll ask kiro to check if you have something similar to extract a helper !

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

at least I didn't find anything close, nor did Kiro, could you look ?

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

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

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

true

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

see comment https://github.com/strata-org/Strata/pull/1422/changes#r3483561857

[julesmt]

↪ Imported from #1422 — originally by @leo-leesco on 2026-06-26 (original)

maybe we can discuss the location of this ? If it makes sense to move it, that's perfectly okay

[julesmt]

↪ Imported from #1422 — originally by @julesmt on 2026-06-26 (original)

yeah let's discuss it monday

[keyboardDrummer]

I had a different design in mind to support performant Python that I would hoping would be more powerful, and so would enable supporting different use-cases as well, related to nullable reference types and exceptions.

The design I had in mind for performant Python is:

• Do not insert any Any types in PythonToLaurel, except for possibly as type annotations in library functions. Leave local variables without a type annotation.
• Configure Laurel with a set of implicit value conversions from specific types to the Any type.

Input Laurel from Python:

procedure foo(b) {
  var x := 3;
  var y := x + x;
  var z := if b then y else "hello";
  var a := z + z
};

After Laurel type inference:

procedure foo(b: bool) {
  var x: int := 3;
  var y: int := x +int x;
  var z: Any := Any..int(y) if b else Any..string("hello");
  var a := z +Any z;
};

The + operator in Laurel would be overloaded, meaning there are several definitions with different signatures, and type inference would decide which one to pick.

In the first implementation I would say that the implicit conversions related to Any would be one directional, only going from specific types to Any but not the other way around: once you're in Any land you're not getting out. We could enable going both ways but this would change the verification output and we should be careful to keep the verification and runtime behavior in sync, especially if we view not verifying everything as Any as purely a verification performance optimization.

@leo-leesco @ssomayyajula does that match with your thoughts?

What I like about the above system is that I think it would also resolve issues other than Python's dynamic value. For example, Java has nullable reference variables, and they need to be wrapped in an Option in Laurel.

Input Laurel from Java:

procedure foo() {
  var o := new Object();
  var p := o;
  p := null;
  p.toString();
}

After Laurel type inference:

procedure foo() {
  var o: Object := new Object();
  var p: Object := Some(o); 
  o := None();
  Option..fromSome(p).toString(); // precondition adds an implicit assertion
}

Java programs would have the option to use annotations to specify that a particular dereference can throw, which would not generate an assertion but will possibly throw a NullPointerException, which will then propagate up the call-chain until caught.

Java program:

void foo() {
  var p: Object := null;
  JVerify.allowNullPointerException();
  p.toString();
}

Before type inference:

void foo() {
  var p: Object := null;
  dereferenceOrThrow(p).toString();
}

procedure derefenceOrThrow<T>(nullable: Option<T>): T throws NullPointerException
  .. ensures clauses..

After type inference:

void foo() throws NullPointerException // throws has been added, ie: procedure type has been lifted
{
  var p: Option<Object> := null; // local variable type has been lifted!
  dereferenceOrThrow(p).toString();
}

[keyboardDrummer]

Can we try a GradualConfig that is just coercions: List Coercion with

structure Coercion where
   from : HighType
   to : HighType
   cast: StmtExprMd -> StmtExprMd 

and then fill this with coercions from all the constructors of PythonAny to PythonAny?

We might need to remove some (or all?) of the PythonAny boxing that is happening in PythonToLaurel, so Resolution can ensure to only insert it where necessary.