Tengo el siguiente 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

Al compilar o interpretar con-Wall se da la siguiente advertencia:

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

Normalmente esto es de esperar. Normalmente, incluso si puedo razonar que mis patrones cubrirán todos los casos posibles, no hay forma de que el compilador lo sepa sin ejecutar el código. Sin embargo, la exhaustividad de los patrones proporcionados se impone por el comprobador de tipos, que se ejecuta en tiempo de compilación. Agregar los patrones sugeridos por GHC da un error de tiempo de compilación:

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

Así que mi pregunta es esta: ¿las advertencias de GHC simplemente no funcionan bien con las extensiones de GHC? ¿Se supone que deben estar conscientes el uno del otro? ¿Esta funcionalidad (advertencias que tienen en cuenta las extensiones) está programada para una versión futura, o existe alguna limitación técnica para implementar esta función?

Parece que la solución es simple; el compilador puede intentar agregar el patrón supuestamente no coincidente a la función, y pedirle nuevamente al verificador de tipos si el patrón sugerido está bien escrito. Si es así, entonces puede informarse al usuario como un patrón perdido.