GHC жалуется на неисчерпывающие шаблоны, которые применяются средством проверки типов

Question

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

{-# 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? Должны ли они знать друг о друге? Предусматривается ли эта функция (предупреждения с учетом расширений) для будущего выпуска или есть какие-то технические ограничения для реализации этой функции?

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

Answer 1

Это похоже на ошибку - вот немного более простая версия:

data Foo :: Bool -> * where
    A :: Foo False
    B :: Foo True

hmm :: Foo b -> Foo b -> Bool
hmm A A = False
hmm B B = True

Кроме того, похоже, что это известная ошибка или часть семейства известных ошибок - ближайший, который я смог найти за несколько минут поиска, был # 3927.