The case at the beginning, where we know our pattern is irrefutable but the compiler doesn't (let (x, 2) = (1, 1+1)) ,is something the compiler could easily prove (as long as the irrefutably could be proven locally as it is here). At first, I struggled to think of why that capability would ever be helpful. In the end, though, I came up with this example, which can (and does) come up:

  fn infallible() -> Result<u8, !>{
      Ok(1)
  }
  
  fn match_infallible(){
      let Ok(x) = infallible();
  }

The compiler here knows the `infallible` function will always return an `Ok` because of the return type. Here you could just `unwrap` the result, but what if it was inside a tuple, or something similar?