Pattern reachability algorithm fails in the presence of uninhabited types

[glaebhoerl]

From check_match.rs:

// Algorithm from http://moscova.inria.fr/~maranget/papers/warn/index.html
//
// Whether a vector `v` of patterns is 'useful' in relation to a set of such
// vectors `m` is defined as there being a set of inputs that will match `v`
// but not any of the sets in `m`.
//
// This is used both for reachability checking (if a pattern isn't useful in
// relation to preceding patterns, it is not reachable) and exhaustiveness
// checking (if a wildcard pattern is useful in relation to a matrix, the
// matrix isn't exhaustive).

// Note: is_useful doesn't work on empty types, as the paper notes.
// So it assumes that v is non-empty.

This results in, most prominently (#4499), a match on an empty enum with a wildcard pattern being accepted:

enum X { }
fn x() -> X { unimplemented!() }
match x() {
    _ => println!("hi")
}

while if you add a variant to the enum and a corresponding arm to the match:

enum X { X }
fn x() -> X { unimplemented!() }
match x() {
    X => println!("hello"),
    _ => println!("hi")
}

rustc rejects the program with error: unreachable pattern.

Clearly a trailing wildcard pattern after you've already matched all possible values in preceding arms should always be considered unreachable, and this is true even when the number of potential values, and hence preceding arms, are both zero.

As the comment notes the algorithm we use relies on "no empty types" as an assumption, so this may not be an easy bug, but it's still a bug.

[glaebhoerl]

cc @brson @nikomatsakis @pcwalton (not really sure who I should be cc-ing): I think this is a backwards compatibility issue in the respect that fixing this bug will cause fewer programs to be accepted. We should make it clear that pattern matching uninhabited types with wildcard patterns is not legal according to the language spec, that it being currently accepted is a compiler bug, and that we reserve the right to fix the bug in the future (if/when we figure out how to).

See examples above if the rationale isn't clear.

[ghost]

Well, if anything, this would require extending the definition of an empty type to include sum types with all members being empty and product types with at least one empty operand.

[glaebhoerl]

Yes, this is implied by the term "uninhabited type". (Or do you mean that there's a definition of an "empty type" in some official spec that needs updating?)

[nikomatsakis]

I agree with @glaebhoerl, though this is clearly a corner case. I wonder if we should remove disallow uninhabited enums and make our lives easier?

[pnkfelix]

/me cannot help but point at #4499 (comment) (though arguably feature-gating is quite different from outright removal...)

[pnkfelix]

Nominating, P-backcompat-lang. See #12609 (comment) for the basis.

[pnkfelix]

Assigning P-backcompat-lang, 1.0 milestone.

(There are many interesting ways to resolve this, and some not-so-interesting ways.)

[sfackler]

Uninhabited enums are useful as phantom type parameters.

[pcwalton]

OCaml has the same behavior as Rust today:

type foo;;

let x: foo = Obj.magic 0 in
match x with
| _ -> print_endline "hello darkness my old friend";; (* OK *)

[pcwalton]

SML/NJ ICE's:

datatype foo = FOO of foo;

val x: foo = Unsafe.cast 0;
case x of _ => print "hello darkness my old friend";

Error: Compiler bug: PPObj: switch: none of the datacons matched

[brson]

@pcwalton that's hilarious

[pcwalton]

I was going to try Scala and Haskell but there is no such thing as an uninhabited type in Scala because of null, and Haskell has no exhaustiveness checking.

Given this exciting romp through languages, I'm going to vote that we go with the only other working compiler that handles this case, and close this as not a bug. Nominating for closure.

[glaebhoerl]

Why is that preferable to saying that it is a bug that we may, at our option, fix in the future? I mean, we can even change our minds later if we convince ourselves that it's impossible. But not vice versa.

[ghost]

GHC does check exhaustiveness but it produces a warning. And it indeed doesn't handle this properly:

import Unsafe.Coerce

data Void

f :: Maybe Void -> Int
f Nothing = 0

main :: IO ()
main = putStr . show . f . unsafeCoerce $ 0

complains with:

void.hs:6:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for `f': Patterns not matched: Just _

[huonw]

@jakub- Only when you compile with -Wall, right?

[glaebhoerl]

This survey of other languages is very interesting, but I don't see why it's very relevant. The correct behavior is not in question. Just because other implementations also have the bug, that doesn't mean it's not a bug.

[pnkfelix]

@pcwalton I'd rather feature-guard uninhabited enums than commit forever (or at least for 1.x) to our current implementation of how they are handled in match.

[huonw]

As a middle ground: would it be reasonable to just feature gate match x whenever x refers to an uninhabited enum? (in the best case ignoring it if the enum is a phantom type parameter, so the type-level state machines and FFI uses of uninhabited enums continue to work.)

[pnkfelix]

@huonw depending on how one interprets "whenever x refers to an uninhabited enum", I would be okay with that compromise. (Basically I want to ensure that examples like your

|x: Option<Uninhabited>| match x { ... }

is caught by the net.)

[ghost]

@pnkfelix Feature-gating uninhabited enums will not be sufficient as the same problem applies to !.

fn main() {
    let x: uint = match fail!() { x => x };
}

I think feature gating match against values of types that contain an empty type in their hierarchy would be ideal. And also removing the current ad-hoc fix for when the root value is of an empty type.

[pnkfelix]

@jakub- I do not think ! (bottom) is the same as an uninhabited type.

In the example you gave, bottom is unified with uint (because you are returning x which is assigned the type uint by the outer context of the expression, so the match makes sense.

If you revise your example to avoid unifying bottom with a concrete type, then it won't pass rustc since it has an unconstrained type.

[ghost]

Right, thanks! In that case, I don't have a strong opinion other than that
I think the current special casing should be removed.
On 4 Jul 2014 17:54, "Felix S Klock II" notifications@github.com wrote:

@jakub- https://github.com/jakub- I do not think ! (bottom) is the same
as an uninhabited type.

In the example you gave, bottom is unified with uint (because you are
returning x which is assigned the type uint by the outer context of the
expression, so the match makes sense.

If you revise your example to avoid unifying bottom with a concrete type,
then it won't pass rustc since it has an unconstrained type.

—
Reply to this email directly or view it on GitHub
#12609 (comment).

[glaebhoerl]

To pose the question once more:

It's safe to assume that the 1.0 compiler will have bugs. I hope it's also safe to assume that we won't hesitate to fix those bugs, even if doing so has the side effect of breaking programs which relied on the buggy behavior.

Why isn't the easiest and most appropriate solution to simply note that this is a bug, and move on?

We don't have to fix it before 1.0. We don't have to fix it next year. All we have to do is to say that it's a bug.

[pnkfelix]

Following similar reasoning to what @glaebhoerl presented above:

We are not going to block 1.0 on resolving this issue. It is a P-backcompat-lang issue, but it is one that we feel prepared to handle (or explicitly not handle, i.e. leave things as they are), post 1.0, in some manner.

P-backcompat-lang, not 1.0 milestone.

[aturon]

Lang team discussed, and we don't feel that this is a very serious issue -- in particular, this only comes up when matching against an empty type, which is very rare to begin with, and the lack of exhaustiveness checking there is unlikely to hide any serious bugs. P-low.

[glaebhoerl]

Not just matching directly on an empty (uninhabited) type, but also on a composite type involving one. In particular types like Result<Foo, !> might become more common if #1216 lands, and right now the exhaustiveness checker doesn't see that the Err variant is impossible. (Another example.)

(Not disputing the priority, which I have no opinion on, only the characterization.)

[aturon]

@glaebhoerl Yes, my summary was a little too brief -- the match against an empty type could occur in the context of another type.

It is a good point that the introduction of ! could make this situation more common, but I think that until we start hearing reports that the lack of exhaustiveness checking there is causing trouble in practice, we can safely leave this at P-low.

[canndrew]

I think this should be fixed before feature(never_type) can be considered stable. In particular, if someone has a Result<T, !>, they should be able to match on it with match res { Ok(v) => v }

[glaebhoerl]

Some concrete motivation for that: for user-defined uninhabited enums (enum Void { }), if we want the same behavior, we'd have to go through a warning-cycle or something, at least, before making the change. But Result<T, !> is not currently a legal type (in stable), so there would be no backwards compatibility concerns either (as long as we change this behavior before making it stable, as @canndrew proposes).

[nikomatsakis]

@canndrew I added this as a note to the ! tracking issue

[canndrew]

I've had a crack at implementing this here: #36476
It seems to work but definitely needs review from someone who actually understands the code I hacked on.

Also, the change I've implemented allows people to omit patterns that are unreachable due to uninhabited types but doesn't force them to. This is important for backwards-compatibility but also because I think code like this:

let res: Result<T, E> = ...;
match res {
    Ok(t) => ...,
    Err(e) => ...,
}

should be allowed to compile even when E (or T) is uninhabited. This might be important for someone who's (eg.) generating code with a macro.

[glaebhoerl]

So should this be closed, or do we wait for it to hit stable?

[nikomatsakis]

We can close.