Any type shadows type error in match expressions

[In-Veritas]

Reproducing the behavior

Issue Description

When defining functions that operate on Maybe(A) types, the type checker seems to behave inconsistently, particularly when the unreachable() function is used in a pattern match. Here's an example to illustrate the problem:

Problematic Code

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()

def main():
    return Maybe/bug(Maybe/Some(12))

Result:

The above code executes without type errors, producing the following result:

λa (a Maybe/Some/tag λb (b Maybe/Some/tag 12))

This is unexpected, as the function violates the intended type constraints of Maybe(A).

---

Correct Behavior

When the function avoids using unreachable() and handles the Maybe/None case with a valid return, the type checker properly enforces the constraints, as seen in the code below:

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

def Maybe/bug2(maybe: Maybe(A), x: A) -> Maybe(A):
    match maybe:
        case Maybe/Some:
            return Maybe/Some(Maybe/Some(maybe.val))
        case Maybe/None:
            return Maybe/Some(x)

def main():
    return Maybe/bug2(Maybe/Some(12), 24)

Result:

Running the above code correctly triggers a type error:

Type Error: Expected function type '((Maybe A) -> A -> (Maybe A))' 
but found '((Maybe h) -> (Maybe h) -> (Maybe (Maybe h)))'. 
Variable 'a' occurs in '(Maybe a)'

---

Analysis

• Function with unreachable() (Maybe/bug): The type checker does not enforce type correctness, allowing invalid types to pass through and the function to execute.
• Function without unreachable() (Maybe/bug2): The type checker properly identifies type mismatches and raises an error, preventing invalid behavior.

This inconsistency demonstrates that using unreachable() somehow bypasses type-checking mechanisms.

---

Expected Behavior

The type checker should raise an error for Maybe/bug, similar to the behavior observed in Maybe/bug2, since the return type violates the Maybe(A) constraint.

---

Steps to Reproduce

1. Define the functions Maybe/bug and Maybe/bug2 as described above.
2. Run the main() function for each case.
3. Observe the behavior:
   • Maybe/bug: No type error, invalid output.
   • Maybe/bug2: Type error, expected behavior.

System Settings

Environment:

• HVM: [hvm 2.0.22]
• Bend: [bend-lang 0.2.37]
• OS: [Ubuntu 22.04.3 LTS]
• CPU: [Intel i7-10700KF]
• GPU: [RTX 2070]

Additional context

No response

[developedby]

It seems that the type checker is unifying the Any type of the unreachable too eagearly.

When checking a match, it infers the type of all match arms, unifies them all and then at the end unifies against the type annotation. Since Any forcefully casts everything into it, the incorrect type of the first arm (Maybe(Maybe(T))) is erased and replaced by Any which will type check without issues when unifiying against the Maybe(T) annotation.

A better checking algorithm would be to check each arm separately against the annotation, but that will require substantial changes to how the type checking algorithm is structured.