eu tenho o seguinte código

{-# LANGUAGE DataKinds, GADTs, TypeOperators #-}

data Vect v a where
    Nil :: Vect '[] a
    Vec :: a -> Vect v a -> Vect (() ': v) a 

instance Eq a => Eq (Vect v a) where
    (==) Nil Nil               = True
    (Vec e0 v0) == (Vec e1 v1) = e0 == e1 && v0 == v1

Ao compilar ou interpretar com-Wall o seguinte aviso é dado:

Pattern match(es) are non-exhaustive
In an equation for `==':
    Patterns not matched:
        Nil (Vec _ _)
        (Vec _ _) Nil

Normalmente isso é esperado. Normalmente, mesmo que eu possa argumentar que meus padrões cobrirão todos os casos possíveis, não há como o compilador saber isso sem executar o código. No entanto, a exaustividade dos padrões fornecidos é imposta pelo verificador de tipos, que é executado em tempo de compilação. Adicionando os padrões sugeridos pelo GHC dá um erro de tempo de compilação:

Couldn't match type '[] * with `(':) * () v1'

Então, minha pergunta é: os avisos do GHC não funcionam bem com as extensões do GHC? Eles deveriam estar cientes um do outro? Esta funcionalidade (avisos levando em consideração as extensões) está prevista para uma versão futura ou há alguma limitação técnica para implementar esse recurso?

Parece que a solução é simples; o compilador pode tentar adicionar o padrão supostamente incomparável à função e pedir novamente ao verificador de tipos se o padrão sugerido for bem digitado. Se estiver, então, de fato, ele pode ser relatado ao usuário como um padrão ausente.