Pattern match checker should treat TypeError as unsatisfiable
Consider this code from !6066 (closed)
type (<=?) :: Int -> Int -> Bool
type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
Assert 'True _errMsg = ()
Assert _check errMsg = errMsg
and this use:
data List n t where
Nil :: List 0 t
(:-) :: t -> List n t -> List (n+1) t
head' :: (1 <= n) => List n t -> t
head' (x :- _) = x -- No need for a Nil case!
The pattern match checker will want to check that the Nil case is unreachable.
In the Nil case, the (1 <= n)
constraint becomes 1 <= 0
, which simplifies
(via Assert
) to TypeError blah-blah
.
And that TypeError @Constraint blahblah
should be treated as unsatisfiable by the pattern match checker!
NB: there is some discussion here
about having an explicit Unsatisfiable
constraint, a more
principled cousin of TypeError
.
Actually this all came up in #11503 (closed), five years ago. Let's nail it!