Rewrite of Python FE to separate out Python-specific resolution, threading of effects, and coercion insertion with Laurel resolver#1415

Draft

ssomayyajula wants to merge 10 commits into

strata-org:reviewed-kbd-will-merge-to-mainfrom

ssomayyajula:ssomayyajula/incremental-hybrid-experiment-v4

Commits on Jun 25, 2026

[checkpoint] v4 port green baseline: 159 success / 4 fail / 43 inconclusive / 14 internal
ssomayyajula
committed
[coercion a] Proof-relevant generic subtyping: coerce returns abstract Coercion verdict
ssomayyajula
committed
[coercion b+c] Resolver is sole coercer: realize witnesses, elaborator effects-only
ssomayyajula
committed
[coercion] Container coercion (Any<->ListAny/DictStrAny) + float->TReal; remove toBool hack
ssomayyajula
committed
[coercion] Truthiness as a coerce verdict (.truthify), folding out the toBool side-hook
ssomayyajula
committed
[coercion] Remove dead toBool plumbing (folded into .truthify verdict)
ssomayyajula
committed
[fix] Assignment-form type aliases (MyInt = int)
ssomayyajula
committed
[fix] Declare unmodeled builtins (type/abs/chr/ord/getattr/setattr) as prelude stubs
ssomayyajula
committed
[doc] PR explanation: v2 Python->Core pipeline + proof-relevant coercion
ssomayyajula
committed

Commits on Jun 26, 2026

[fix] Keep generic Laurel resolver identical to baseline; coercion is Python-only
ssomayyajula
committed