Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type checker and interpreter do not agree on @expected values #2130

Open
toinehartman opened this issue Jan 27, 2025 · 0 comments
Open

Type checker and interpreter do not agree on @expected values #2130

toinehartman opened this issue Jan 27, 2025 · 0 comments
Assignees

Comments

@toinehartman
Copy link
Contributor

Describe the bug

The type checker and the interpreter do not agree on valid values for the @expected test annotation.

  • The type checker allows the RuntimeException ADT type or any constructor of that type. It various raises errors on anything else.
  • The interpreter has a test succeed iff a constructor (of any ADT) is expected and the test throws that exact constructor.

To Reproduce

import Exception;

data CustomException
    = e()
    ;

// SUCCEED

@expected{NotImplemented}
test bool runtimeExceptionExpectConstructor() { throw NotImplemented("fail"); }

@expected{e} // type error : Expected `RuntimeException`, found `CustomException::e()`
test bool constructorExpectConstructor() { throw e(); }



// FAIL


@expected{RuntimeException}
test bool runtimeExceptionExpectADT() { throw NotImplemented("fail"); }

@expected{CustomException} // type error : Expected `RuntimeException`, found `CustomException::e()`
test bool constructorExpectADT() { throw e(); }

@expected{"someNode"()} // type error : Undefined constructor or data `"someNode"()`
test bool \node() { throw "someNode"(); }

@expected{"s"} // type error : Undefined constructor or data `"s"`
test bool \str() { throw "s"; }

@expected{8} // type error : Undefined constructor or data `8`
test bool \int() { throw 8; }

Expected behavior

  • No type errors on expected constructors of any ADT type (e.g. `data E = e(); @expected{e}).
  • Possibly type errors/warnings on an expected ADT type (e.g. @expected{RuntimeException}).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants