haskell - 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 の拡張機能とうまく機能しませんか? 彼らはお互いを認識しているはずですか？この機能 (拡張機能を考慮した警告) は将来のリリースで予定されていますか? または、この機能の実装に技術的な制限はありますか?

解決策は単純なようです。コンパイラは、おそらく一致しないパターンを関数に追加し、提案されたパターンが適切に型付けされているかどうかを型チェッカーに再度問い合わせることができます。そうである場合は、実際にパターンの欠落としてユーザーに報告できます。