@@ -283,6 +283,11 @@ func (c *checker) walkStatement(s ast.Statement) {
283283 c .env .pop ()
284284 case * ast.ExpressionStatement :
285285 c .walkExpressionDiscard (n .Expression )
286+ // `assert(cond)` only returns when cond held, so its positive
287+ // narrowing applies to the rest of the block.
288+ if cond , ok := assertCondition (n .Expression ); ok {
289+ c .applyRefinement (c .refine (cond , true ))
290+ }
286291 case * ast.DeferStatement :
287292 // The deferred call is checked like any other call statement; it
288293 // produces no value the surrounding scope can observe.
@@ -378,7 +383,9 @@ func (c *checker) walkAssignStatement(s *ast.AssignStatement) {
378383 for i , t := range s .Targets {
379384 switch tgt := t .(type ) {
380385 case * ast.Identifier :
381- declared , ok := c .env .lookup (tgt .Name )
386+ // Check against the declared type, not any narrowing shadow —
387+ // `s = nil` inside `if s ~= nil then` is legal for a `string?`.
388+ declared , ok := c .env .lookupDeclared (tgt .Name )
382389 if ! ok {
383390 // First-time global write: bind to the RHS type so later
384391 // reads see it. Matches Lua's "globals materialize on
@@ -389,6 +396,9 @@ func (c *checker) walkAssignStatement(s *ast.AssignStatement) {
389396 if ! assignable (rhs [i ], declared ) {
390397 c .errAssign (s .Line (), rhs [i ], declared )
391398 }
399+ // The value changed; any active narrowing must absorb the new
400+ // type or it would keep vouching for the old one.
401+ c .env .widenRefined (tgt .Name , rhs [i ])
392402 case * ast.IndexExpression :
393403 // Field assignment to a table. We currently don't enforce
394404 // shape conformance on writes (most Lua tables are open),
@@ -408,7 +418,14 @@ func (c *checker) walkIfStatement(s *ast.IfStatement) {
408418 // earlier condition was false — exactly Lua's evaluation order. The
409419 // then-branch of each clause gets its own child frame on top.
410420 c .env .push ()
411- defer c .env .pop ()
421+
422+ // Early-exit narrowing: when a leading prefix of clauses always
423+ // terminates (`if s == nil then return end`), falling past the whole
424+ // statement proves each of those conditions was false, so their
425+ // negations outlive the `end`. Only a prefix qualifies — once a clause
426+ // can fall through, later conditions may never have been evaluated.
427+ var persist []refinement
428+ prefixTerminates := true
412429
413430 for _ , cl := range s .Clauses {
414431 // Walk the condition once (in the already-narrowed scope) for error
@@ -423,14 +440,28 @@ func (c *checker) walkIfStatement(s *ast.IfStatement) {
423440
424441 // Fold this clause's "condition is false" narrowing into the
425442 // accumulator so subsequent branches see it.
426- c .applyRefinement (c .refine (cl .Condition , false ))
443+ negR := c .refine (cl .Condition , false )
444+ c .applyRefinement (negR )
445+
446+ if prefixTerminates {
447+ if blockTerminates (cl .Body ) {
448+ persist = append (persist , negR )
449+ } else {
450+ prefixTerminates = false
451+ }
452+ }
427453 }
428454
429455 if s .Else != nil {
430456 c .env .push ()
431457 c .walkBlock (s .Else )
432458 c .env .pop ()
433459 }
460+
461+ c .env .pop ()
462+ for _ , r := range persist {
463+ c .applyRefinement (r )
464+ }
434465}
435466
436467func (c * checker ) walkNumericFor (s * ast.NumericForStatement ) {
@@ -934,7 +965,26 @@ func (c *checker) checkNamedStructCall(call *ast.CallExpression, sc *StructCtor)
934965
935966func (c * checker ) typeOfBinary (e * ast.BinaryExpression ) * Type {
936967 left := c .typeOfExpression (e .Left )
937- right := c .typeOfExpression (e .Right )
968+
969+ // and/or short-circuit, so their RHS only evaluates under the LHS's
970+ // truthy (and) / falsy (or) outcome — type it in a frame carrying that
971+ // narrowing: `s ~= nil and #s`, `x or default`.
972+ var right * Type
973+ switch e .Op {
974+ case "and" :
975+ c .env .push ()
976+ c .applyRefinement (c .refine (e .Left , true ))
977+ right = c .typeOfExpression (e .Right )
978+ c .env .pop ()
979+ case "or" :
980+ c .env .push ()
981+ c .applyRefinement (c .refine (e .Left , false ))
982+ right = c .typeOfExpression (e .Right )
983+ c .env .pop ()
984+ default :
985+ right = c .typeOfExpression (e .Right )
986+ }
987+
938988 switch e .Op {
939989 case "+" , "-" , "*" , "/" , "//" , "%" , "^" , "&" , "|" , "~" , "<<" , ">>" :
940990 c .requireNumber (e .Line (), left , right )
@@ -965,11 +1015,22 @@ func (c *checker) typeOfBinary(e *ast.BinaryExpression) *Type {
9651015 }
9661016 return booleanT
9671017 case "and" :
968- // `a and b` returns a if falsy, else b. The result type is the
969- // union; for a typed-correctness perspective this is good enough.
970- return NewUnion (left , right )
1018+ // `a and b` yields a only when a is falsy — the truthy members of
1019+ // a's type can't reach the result. (false can't be split off from
1020+ // boolean, so a boolean member survives whole.)
1021+ falsy := keepKinds (left , KindNil , KindBoolean )
1022+ if falsy .Kind == KindNever {
1023+ return right
1024+ }
1025+ return NewUnion (falsy , right )
9711026 case "or" :
972- return NewUnion (left , right )
1027+ // `a or b` yields a only when a is truthy — nil can't survive,
1028+ // which is what makes `x or default` a non-optional.
1029+ truthy := removeKind (left , KindNil )
1030+ if truthy .Kind == KindNever {
1031+ return right
1032+ }
1033+ return NewUnion (truthy , right )
9731034 }
9741035 return anyT
9751036}
0 commit comments