Don't warn about an inaccessible `undefined`

This is the "Hello world!" of dependent types (safe indexing) in GHC:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data Nat where
  Zero :: Nat
  Suc :: Nat -> Nat

data Vec a n where
  Nil  :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Suc n)

data Fin n where
  FZero :: Fin (Suc n)
  FSuc  :: Fin n -> Fin (Suc n)

look :: Vec a n -> Fin n -> a
look (Cons x xs) FZero    = x
look (Cons x xs) (FSuc i) = look xs i
look !_ !_ = undefined

The last clause indicates that the pattern matching is complete. Without it, I get an incomplete-patterns warning.

However, with it, I get:

 warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘look’: look !_ !_ = ...
   |
25 | look !_ !_ = undefined
   | ^^^^^^^^^^^^^^^^^^^^^^

It would be nice if exception raisers like undefined or error as rhs would silence this warning. I mean, the user indicates with a undefined rhs their awareness that this case is impossible.

The alternative would be a special syntax that allows to omit the rhs altogether in contradictory cases. (That's what Agda's absurd clauses do.) However, detecting undefined might be less invasive to the language.