У меня есть следующий код

{-# 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

При компиляции или интерпретации с-Wall выдается следующее предупреждение:

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

Обычно этого следовало ожидать. Обычно, даже если я могу предположить, что мои шаблоны будут охватывать все возможные случаи, компилятор не сможет узнать об этом без выполнения кода. Однако исчерпывающий характер предоставленных шаблонов обеспечивается средством проверки типов, которое выполняется во время компиляции. Добавление шаблонов, предложенных GHC, дает ошибку времени компиляции:

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

Итак, мой вопрос таков: предупреждения GHC просто не подходят для расширений GHC? Должны ли они знать друг о друге? Предусматривается ли эта функция (предупреждения с учетом расширений) для будущего выпуска или есть какие-то технические ограничения для реализации этой функции?

Кажется, что решение простое; компилятор может попытаться добавить предположительно несопоставимый шаблон в функцию и снова запросить средство проверки типа, правильно ли предложенный шаблон типизирован. Если это так, то это действительно может быть сообщено пользователю как отсутствующий шаблон.