Inconsistency in pattern matching over the never type ! as an associated trait type

[radrow]

I have found a weird inconsistency when ! is behind a trait and wrapped as a constructor field:

#![feature(never_type, exhaustive_patterns)]

trait Tag {
    type TagType;
}

enum Keep {}
enum Erase {}

impl Tag for Keep {
    type TagType = ();
}

impl Tag for Erase {
    type TagType = !;
}

enum TagInt<T: Tag> {
    Untagged(i32),
    Tagged(T::TagType, i32)
}

fn test(keep: TagInt<Keep>, erase: TagInt<Erase>) {
    // This is fine
    match keep {
        TagInt::Untagged(_) => (),
        TagInt::Tagged(_, _) => ()
    };

    match erase {
        TagInt::Untagged(_) => (),
        TagInt::Tagged(_, _) => ()  // unreachable pattern
    };

    match erase { // non-exhaustive patterns: `TagInt::Tagged(_, _)` not covered
        TagInt::Untagged(_) => ()
    };
}

Note the errors in the comments. I hoped for the typechecker to notice that Tagged could not be a value of TagInt<Erase>, and thus not demand covering that case. On the other hand, when I follow the advice and consider it, the typechecker suddenly realizes this is dead code and suggests removing it. Regardless whether Tagged should be covered or not , it feels incorrect that the typechecker contradicts itself.

The Tagged case for TagInt<Erase> is indeed unreachable, and the compiler manages to detect it. I would therefore expect the last match to be correct, and the previous one to be marked as it is. This bug breaks my way towards emulating GADTs in Rust's type system. At least I don't see any other hack for conditional constructors.

Meta

rustc --version --verbose:

rustc 1.72.0-nightly (22e9fe644 2023-06-23)
binary: rustc
commit-hash: 22e9fe644ea710eec50cb0aabcae7fa8dd9fd675
commit-date: 2023-06-23
host: x86_64-unknown-linux-gnu
release: 1.72.0-nightly
LLVM version: 16.0.5
    Finished dev [unoptimized + debuginfo] target(s) in 0.02s

Build output

    Checking rust-playground v0.1.0 (/home/radek/Programming/rust-playground)
warning: unreachable pattern
  --> src/main.rs:32:9
   |
32 |         TagInt::Tagged(_, _) => ()  // unreachable pattern
   |         ^^^^^^^^^^^^^^^^^^^^
   |
   = note: `#[warn(unreachable_patterns)]` on by default

error[E0004]: non-exhaustive patterns: `TagInt::Tagged(_, _)` not covered
  --> src/main.rs:35:11
   |
35 |     match erase { // non-exhaustive patterns: `TagInt::Tagged(_, _)` not covered
   |           ^^^^^ pattern `TagInt::Tagged(_, _)` not covered
   |
note: `TagInt<Erase>` defined here
  --> src/main.rs:20:5
   |
18 | enum TagInt<T: Tag> {
   |      ------
19 |     Untagged(i32),
20 |     Tagged(T::TagType, i32)
   |     ^^^^^^ not covered
   = note: the matched value is of type `TagInt<Erase>`
help: ensure that all possible cases are being handled by adding a match arm with a wildcard pattern or an explicit pattern as shown
   |
36 ~         TagInt::Untagged(_) => (),
37 +         TagInt::Tagged(_, _) => todo!()
   |

For more information about this error, try `rustc --explain E0004`.
warning: `rust-playground` (bin "rust-playground") generated 1 warning
error: could not compile `rust-playground` (bin "rust-playground") due to previous error; 1 warning emitted

[Jules-Bertholet]

@rustbot label F-exhaustive_patterns