Type narrowing for imperative early-return patterns
Expression mode narrows optional types through if-else branches:
# Expression mode: t narrowed to non-optional in else branch
treeSize(t) = if(t==none) 0 else 1 + treeSize(t?.left) + treeSize(t?.right)
Lang mode blocks don't apply narrowing after early returns:
# Lang mode: t stays optional after the if-block
fun treeSize(t):
if t == none: return 0
return 1 + treeSize(t?.left) + treeSize(t?.right) # t still optional here
Impact
- Named type recursive tree functions fail at runtime (FunnyNone → FunnyStruct cast)
- Type inference is less precise (types stay wider than necessary)
t.field after if t == none: return should work without ?.
Proposed fix
In Visit(BlockSyntaxNode), analyze statements: when a statement is an if-block with early return and the condition is x == none, narrow x to non-optional for subsequent statements.
Pattern: if x == none: return/break/continue → x is non-optional after this point.
This is equivalent to expression-mode VisitIfThenElseWithNarrowing but for sequential block statements.
Algebraic justification
if t == none: return 0; expr ≡ if(t==none, return 0, expr). The second form applies narrowing in expression mode. The first should apply identical narrowing.
Type narrowing for imperative early-return patterns
Expression mode narrows optional types through if-else branches:
Lang mode blocks don't apply narrowing after early returns:
Impact
t.fieldafterif t == none: returnshould work without?.Proposed fix
In
Visit(BlockSyntaxNode), analyze statements: when a statement is an if-block with early return and the condition isx == none, narrowxto non-optional for subsequent statements.Pattern:
if x == none: return/break/continue→ x is non-optional after this point.This is equivalent to expression-mode
VisitIfThenElseWithNarrowingbut for sequential block statements.Algebraic justification
if t == none: return 0; expr≡if(t==none, return 0, expr). The second form applies narrowing in expression mode. The first should apply identical narrowing.