8

我有以下代码

{-# 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 扩展配合使用？他们应该互相了解吗？此功能（考虑到扩展的警告）是否计划在未来版本中发布，或者实现此功能是否存在一些技术限制？

似乎解决方案很简单；编译器可以尝试将假定不匹配的模式添加到函数中，并再次询问类型检查器是否建议的模式类型正确。如果是，那么它确实可以作为缺失模式报告给用户。

4

1 回答 1

6

这看起来像一个错误——这是一个稍微简单的版本：

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。

于 2013-10-15T06:30:52.943 回答