You can find other cases in spec.

@ysbaddaden I understand what you said. I want you to try to use this compiler to your project.

else nil for the old behaviour is hardly a lot of code to add, and this way is much more explicit. 👍

@asterite I'll fix it.

What I like in this PR is making the compiler smarter, so it knows that a case handles all possible cases, so I don't have to specify an else raise "unreachable" statement to avoid a nilable, for example. That's lovely.

What I don't like in this PR is trading implicit nilables and "I don't care for other values" for explicit noise with empty else statements (aka else # shut up crystal). This is pushing a burden to the developer.

I verified most of my applications and libraries, and this PR will help in... none. Quite the opposite, as it will require me to insert many empty else statements in each SDL2 samples for example.

The benefit, which is inexistant in all my projects (and it seems the compiler source too), isn't worth the burden. This is an unacceptable trade IMHO.

@asterite I can't help but think that without global type inference what would be the point of crystal at all. Global type inference with unions is the defining feature of Crystal. To me - at least - it's what makes Crystal, Crystal. I think it'd be a huge mistake to change Crystal's type system in such a radical way this late in development, and it'd be a huge mistake to throw away something which is so beautiful and easy to use. Yes the compile times for large program suck, perhaps we'll have to introduce some "module" concept with defined types for the interface, but languages like Scala managed to succeed despite long compile times. Perhaps people using crystal will create more microservices than other languages.

I'd rather have a discussion like this on the mailinglist though.

Maybe we can use some special keyword to check exhaustiveness

This code would compile ok:

enum FooBar
  Foo
  Bar
end

foo = FooBar::Foo

case foo
when .foo?
end

But this won't:

enum FooBar
  Foo
  Bar
end

foo = FooBar::Foo

@[Exhaustive]
case foo
when .foo?
end

See the @[Exhaustive] rule

$ ./bin/crystal run foo_bar.cr
Error in foo_bar.cr:7: found non-exhaustive pattern: Bar

case foo
     ^~~

I want the compiler to check exhaustiveness in default because exhaustiveness is important to prevent bugs, so I want you to consider about it at all times.

However many people need this, I suggest case! as keyword. (It breaks call of case! method, but I think this effects is very small.)

If we are going to be exhaustive by default then else nil should be how we describe non-exhaustiveness not another keyword. However, @ysbaddaden provided some evidence that being exhaustive by default actually might not help catch many bugs, so I would like more data on this. If you have a library or project, please try out this pr and report back how much code you had to change and if it found any bugs.

I think exhaustiveness check to existed project affects us not helpful because all non-exhaustive cases in this project are intentional if this project is well tested.

I actually prefer being exhaustive by default. It gives me peace of mind and most importantly a confidence to refactor and add {things to enums,types to unions} without worrying about every case clause it might touch.

We may need the attribute to drop exhaustiveness check from enum:

@[NotCheckExhaustiveness]
enum KeyCode
  A
  B
  # ...
end

key = KeyCode::A

# This `case` passes exhaustiveness check due to @[NotCheckExhaustiveness] attribute.
# Of course result type is nilable.
case key
when .w?
  go
when .a?
  turn_left
when .s?
  back
when .d?
  turn_right
end

/cc @ysbaddaden

@makenowjust The problem is that that makes case behaviour dependant on an attribute on enum which is unlikely to be visible to the programmer at the point the enum is used.

I found a failed exhaustiveness check in callstack.cr:205.

@straight-shoota I think it's already fixed. Your stdlib may be old.

@RX14 Exhaustiveness check to Char is impossible, and there are enums like Char (e.g. KeyCode I said.). I thought it is useful if we can define such enums.

Now it is working:

a = 42

loop do
  case a
  when Int32
  end

  a = "foo"
end

# Error in foo.cr:3: instantiating 'loop()'
#
# loop do
# ^~~~
#
# in foo.cr:3: instantiating 'loop()'
#
# loop do
# ^~~~
#
# in foo.cr:4: found non-exhaustive pattern: String
#
#   case a
#        ^

/cc @asterite

ping. I don't want to stop discussion about this.

I personally think having case be non-exhaustive and case! be exhaustive would work well. This could be stored as a boolean in the AST node (also for to_s). I don't know what others think, though.

Actually, about hierarchy type, maybe it's good not to check for exhaustiveness because code will break if a subclass is added in a separate library or application, and there's no way to fix that (you don't own the code that has the case). So probably with just unions and enums it's fine... Though with unions you could also have the same problem if someone redefines a method, but that's less common.

@makenowjust どうもありがとうございます！

Ship it!

Having this in 0.25.0 would be really nice, both because it improves the robustness of code, and because it can be tested early in the wild.

Letting the case have two different semantics it's hard to understand.
The users might not feel secure if the compiler is performing or not the exhaustive check.

So I think the exhaustive vs non-exhaustive check should be explicit.

Having different keywords it is a clear way to do it: case/case?, case!/case or some other combination. I have come to over/case or even forall/case that I think express more clearly that you want to cover all cases (over or forall). forall is already a keyword but is used in other context without ambiguity.

But I think there is a different approach that could be more powerful.
It has been discussed previously (in #4749) but implementing compile time checks for unreachable would be a more elementary way to achieve the exhaustive checks without diffrent case statements.

case expr
when Int32
when String
else unreachable
end

Then all the case statements would try to omit the codegen of the else branch (or any other branch that is sound to remove) and hence the unreachable wont be emitted.

It is longer to type that a different control structure keyword but is a feature that can be combined with other control structures eventually if redundant code is detected. Note: The implementation would probably not be that different from this PR. The compile time error needs to be deferred, but the exhaustive check is the hardest part.

For me is either unreachable or a different case statement (I prefer unreachable between those). Having to add else nil for the cases (no pun intended) when the compiler was able to compute exhaustive coverage if the user wanted the same behavior as in other cases is way to obscure and hard to understand.

So currently, this PR falls back to non-exhaustive case depending on the type of expr? That's not good.

I don't like else unreachable, I'll forget to type it everywhere.

Perhaps use case for exhaustive matching (you're looking at every case) and cond for non-exhaustive matching (you're just checking the condition, don't care about each case)?

As for how to implement case/cond, I'd introduce cond and print a warning on non-exhaustive case on one version, then make non-exhaustive case an error on version+1.

No. It checks exhaustiveness for any typed expr. A user cannot choice exhaustiveness or non-exhaustiveness.

If the case expr is other type than union or enum, the case is not exhaustive. I see that as implicit because there is nothing in the expression typed by the user that expresses his/her expectation.

@bcardiff Sorry. I forgot this specification. Oh I see. It is bad point of this. However it needs more and more (180+ cases) appending else # skip if it check exhaustive for single-type case...

else unreachable and case forall are interesting ideas. I prefer case forall because it appears in above of syntax. I feel intuitive.

It's a subtle thing and is hard to be everybody in the same page.

Maybe the else unreachable would come later and first we can have it's own control structure that could later when else unreachable is implemented be rewritten or left as an implementation detail.

Just to be clear, I was previously proposing the following constructs to allow exhaustive checks:

forall a
when String
end

over a
when String
end

@RX14 suggestions to leave case of exhaustive and cond for the current behaviour is good also. That will require a release of crystal where case and cond have the same semantic and later change the semantic of the case.

@asterite I think your opinion is needed to proceed with discussion. bcardiff opinion is right and his ideas are interesting to me. What do you think?

@bcardiff said:

Letting the case have two different semantics it's hard to understand.

But that's not true. case has only one semantic: it's always exhaustive. I mean, for types it's exhaustive. If the type is Int32 and you match with integers, you'll always need an else because there are many numbers (and I doubt one will list all of them). Same goes for symbol, etc. So case is always exhaustive, there's simply no confusion, no different semantics.

forall, cond, they are very confusing and add more keywords and noise to the language.

I personally don't mind having to add an else clasue to case for a few cases. It's more explicit that other cases are not considered.

So for me, this PR is perfect. And I would have liked it to be in 0.25.0.

But ultimately, I don't use Crystal anymore, so I shouldn't choose its future.

Agreed. As long as it’s exhaustive in all cases I think this should work great. I can hardly wait to try this :)

Yes, let's keep it simple, please.

I don't like having different keywords with subtle differences. People will be confused.
The concept of else is widely understood and should be capable of differentiating between exhaustiveness.

@asterite no, this PR isn't exhaustive in all cases, for example:

str = "bar"

case str
when "foo"
  1
end

will not produce a compile error and be type Int32?

This is what we meant by the exhaustiveness depending on the argument.

Let's try making case always exhaustive and see how big the diff is.

Oh, I thought that was already the case, because I see else over symbols in the diff, and other primitives.

So yes, either change it to always be exhaustive, or only exhaustive when it makes sense (I'm fine with that too, and I find it intuitive and user friendly, as forcing al else clause over something that the compiler can't verify is a bit useless)

I'd really love to see this PR merged. More correctness is great.

Note that this PR is incomplete and doesn't play nicely with the type flow inference.

For example:

a = 1 || "foo"
case a
when Int32
  b = 1
when String
  b = 2
end

puts typeof(b) # => Int32 | Nil

That is, the compiler correctly finds that it's an exhaustive match, but the type for b remains nilable because that logic goes in another place in the compiler. All of that should be unified but it's a bit hard to do.

(that's at least the last thing I remember when I tried this PR, now it needs a rebase but I'm pretty sure it'll still have that problem)

I think we really need to form a consensus on the design first before fixing the implmentation because there are some unresolved issues.

I think the current prevailing design is for case to always be exhaustive and not introduce a second kind of case. However there's still the question of types like String where the compiler will never be able to prove exhaustiveness. For these types the case can either keep being exhaustive and force you to always have an else clause, or the compiler can stop being exhaustive in these cases.

The benefits of being exhaustive in this case are:

• simplicity of semantics: the type of the case argument doesn't affect the semantics of case. Since types aren't explicit in crystal this makes case easier to understand on it's own.
• It's impossible to accidentally create a non-exhaustive case by accidentally creating a union of (for example) Enum | String instead of Enum in your case argument.

The benefits of not being exhaustive in this case are:

• not having to add verbose else nil clauses in the obvious case of case string.

There's also the option to make it so that case is exhaustive if just one of the types in the union can be exhaustively matched. This might make a better semantic in practice, but retains a lot of complexity.

Ideally we'll have a continued discussion of the pros and cons of these three choices of semantics below then a vote in a week or so. Merging any of those three semantics will be better than what we have currently.

This can probably be closed now that #8424 is merged?

Yes, but there is a lot of credit to go on this PR and the discussion 🙇.