-
Notifications
You must be signed in to change notification settings - Fork 270
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
Allow parsing empty case-blocks #5249
base: trunk
Are you sure you want to change the base?
Conversation
# Conflicts: # parser-typechecker/src/Unison/Syntax/TermParser.hs
not sure why the `GiveA`/`GiveB` abilities are reversed here.
``` unison | ||
structural type Void = | ||
|
||
test : Void -> a | ||
test = cases | ||
``` | ||
|
||
``` ucm | ||
|
||
Loading changes detected in scratch.u. | ||
|
||
Pattern match doesn't cover all possible cases: | ||
4 | test = cases | ||
|
||
|
||
Patterns not matched: | ||
* () | ||
|
||
``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There seems to be a bug or missing special-case in TermParser.hs
-> lamCase
-> lamvarTerm
that is introducing ()
here.
@@ -1335,6 +1379,6 @@ result f = | |||
|
|||
ability GiveA a | |||
ability GiveB a | |||
result : '{e, GiveA V, GiveB V} r ->{e} r | |||
result : '{e, GiveB V, GiveA V} r ->{e} r |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not sure what's causing this, it wasn't in #5256 alone
``` unison | ||
structural type Void = | ||
|
||
test : Void -> a | ||
test x = match x with | ||
``` | ||
|
||
``` ucm | ||
|
||
Loading changes detected in scratch.u. | ||
|
||
I found and typechecked these definitions in scratch.u. If you | ||
do an `add` or `update`, here's how your codebase would | ||
change: | ||
|
||
⍟ These new definitions are ok to `add`: | ||
|
||
structural type Void | ||
test : Void -> a | ||
|
||
``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This case is fixed though.
NOTE: currently this breaks exhaustiveness checking :'(
It should provide an exhaustiveness failure for an inhabited type with zero cases, but it doesn't.
The exhaustiveness checker code is pretty complex, so would take a bit of digging into to solve.