@@ -383,7 +383,21 @@ class WellFormedChecker : public relax::ExprVisitor,
383383 auto inferred_struct_info = GetStructInfo (normalized.value ());
384384 auto current_struct_info = Downcast<StructInfo>(call->struct_info_ );
385385
386- if (!IsBaseOf (current_struct_info, inferred_struct_info)) {
386+ // An error should be raised if the annotated StructInfo is
387+ // provably incorrect. This check is done using
388+ // `StructInfoBaseCheck(...) < kFailL2`, because `kFailL2`
389+ // represents cases that are neither provably correct nor
390+ // provably incorrect. If this check were replaced with
391+ // `!IsBaseOf(...)`, cases that are correct but not provably
392+ // so would raise an exception.
393+ //
394+ // For example, if a dynamic size in the inferred StructInfo
395+ // is equivalent to the expression used in the annotated
396+ // StructInfo, but the TIR simplifications are not sufficient
397+ // to prove that the two expressions are equivalent, we should
398+ // not raise an error.
399+ if (StructInfoBaseCheck (current_struct_info, inferred_struct_info) <
400+ BaseCheckResult::kFailL2 ) {
387401 Malformed (Diagnostic::Error (call)
388402 << " All information in StructInfo annotations must be correct. "
389403 << " However, while the expression " << GetRef<Call>(call) << " is annotated as "
0 commit comments