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.