Избавление от предупреждения о неисчерпывающих сопоставлениях шаблонов при ограничении GADT семействами типов

Учитывая следующую программу:

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B
type family IsA (foo :: Foo) :: Bool

type instance IsA A = True
type instance IsA B = False

data Bar (foo :: Foo) where
    BarA :: (IsA foo ~ True) => Int -> Bar foo
    BarB :: (IsA foo ~ False) => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x

Я получаю это предупреждение от GHC 7.4.2 при использовании -fwarn-incomplete-patterns для общей функции f, определенной выше:

Warning: Pattern match(es) are non-exhaustive
         In a case alternative: Patterns not matched: BarB _

Конечно, нет смысла даже пытаться добавить совпадение для BarB:

Couldn't match type `'False' with `'True'
Inaccessible code in
  a pattern with constructor
    BarB :: forall (foo :: Foo). IsA foo ~ 'False => String -> Bar foo,
  in a case alternative
In the pattern: BarB _
In a case alternative: BarB _ -> undefined
In the expression:
  case bar of {
    BarA x -> x
    BarB _ -> undefined }

Есть ли способ убедить GHC, что f тотален? Кроме того, это ошибка GHC или просто известное ограничение; или на самом деле есть очень веская причина, по которой невозможно увидеть, что совпадение с образцом в f завершено?


warnings haskell pattern-matching ghc type-families
person Cactus    schedule 15.09.2012    source источник

Ответы (2)


arrow_upward
9
arrow_downward

Это раздражает, да. GHC исходит из предположения, что семейства типов (и классы) повсеместно и глубоко встроены в его алгоритмы; однако вы пишете семейство типов, параметризованное закрытым типом. Это напряжение объясняет непонимание между вами и GHC. Я думаю, что были некоторые мысли о том, как обращаться с классами и семействами закрытого типа, но это сложная область.

Тем временем вы можете избежать открытости семейств шрифтов, чтобы убедить средство проверки целостности.

{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Foo = A | B

data Bar (foo :: Foo) where
    BarA :: Int    -> Bar A -- or BarA :: foo ~ A => Int    -> Bar foo
    BarB :: String -> Bar B -- or BarB :: foo ~ B => String -> Bar foo

f :: Bar A -> Int
f bar = case bar of
    BarA x -> x
-- or f (BarA x) = x
person Daniel Wagner    schedule 15.09.2012
comment
К сожалению, я не могу этого сделать, потому что мой реальный вариант использования моделируется более подходящим образом, имея data Foo = A | B | C и два конструктора BarA и BarBC. - person Cactus; 16.09.2012
comment
@Кактус data BorC a where { IsB :: BorC B; IsC :: BorC C }; data Bar foo where BarBC :: BorC foo -> String -> Bar foo - person Daniel Wagner; 16.09.2012

arrow_upward
1
arrow_downward

Вы всегда можете использовать _ для сопоставления шаблона с чем-либо в качестве последнего условия случая.

Итак, _ -> undefined вместо BarB _ -> undefined.

Это сделает case total в его аргументе.

Существует также библиотека Нила Митчелла, которая проверяет наличие неисчерпывающих шаблонов для предотвращения сбоев во время выполнения из-за к несовпадающим шаблонам.

person Satvik    schedule 15.09.2012