Problem
In elaborate_let (checker/infer.rs), the simple-let path elaborates the type annotation with infer:
let (core_e, bind_ty_val) = if let Some(ann) = stmt.ret_ty {
let (ty, _) = infer(ctx, phase, ann)?;Since infer rejects match expressions ("cannot infer type of match expression"), any dependent type annotation on a plain let fails:
let y: (match b { 0 => u16, 1 => u0 }) = ...; -- rejected
even though the same annotation is accepted in def signatures and in the parameterized-let path, both of which correctly use check_universe (check against the phase's universe — the checkU pattern).
Fix
Use check_universe(ctx, phase, ann) in the simple-let path, mirroring the parameterized path. The annotation's own type is not needed — only the elaborated term — so infer-then-discard buys nothing and loses checked-mode coverage.
Problem
In
elaborate_let(checker/infer.rs), the simple-let path elaborates the type annotation withinfer:Since
inferrejectsmatchexpressions ("cannot infer type of match expression"), any dependent type annotation on a plainletfails:even though the same annotation is accepted in
defsignatures and in the parameterized-let path, both of which correctly usecheck_universe(check against the phase's universe — thecheckUpattern).Fix
Use
check_universe(ctx, phase, ann)in the simple-let path, mirroring the parameterized path. The annotation's own type is not needed — only the elaborated term — so infer-then-discard buys nothing and loses checked-mode coverage.