Skip to content

fix: prevent Any type from shadowing type errors in match arms#761

Open
Aletheia-Prime wants to merge 1 commit intoHigherOrderCO:mainfrom
Aletheia-Prime:main
Open

fix: prevent Any type from shadowing type errors in match arms#761
Aletheia-Prime wants to merge 1 commit intoHigherOrderCO:mainfrom
Aletheia-Prime:main

Conversation

@Aletheia-Prime
Copy link
Copy Markdown

Summary

When unreachable() is used in a match arm, the type checker infers Any as the return type. Since Any can unify with anything in the unification function, it absorbs type constraints from other arms, allowing invalid types to pass without error.

Fix

Modified infer_match_cases in type_check.rs to preserve the type constraints from non-Any arms. When the final unified type is Any but a previous arm has free type variables, we use the previous arm's type to preserve those constraints.

Test

The fix was verified against the test case from issue #742:

type Maybe(T):
  Some{val: T}
  None

def Maybe/bug(maybe: Maybe(A)) -> Maybe(A):
  match maybe:
    case Maybe/Some:
      return Maybe/Some(Maybe/Some(maybe.val))
    case Maybe/None:
      return unreachable()

Before fix: No type error (incorrect)
After fix: Type error as expected

All existing tests pass (20 passed, 2 ignored).

When unreachable() was used in a match arm, the type checker would infer Any
as the return type. Since Any can unify with anything, it would absorb
type constraints from other arms, allowing invalid types to pass without error.

This fix preserves type constraints from non-Any arms when the final unified type
is Any but a previous arm has free type variables.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant