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.