Deshacerse de "Patten no exhaustiva coincide" advertencia cuando la restricción GADTs con las familias de tipo

Question

Dado el siguiente programa:

{-# 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 

consigo esta advertencia de GHC 7.4.2 cuando se utiliza -fwarn-incomplete-patterns para la función total de f definido arriba:

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

por supuesto, no tiene sentido intentar siquiera añadiendo a la altura de 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 } 

¿Hay alguna manera de convencer a GHC de que f es total? Además, ¿esto es un error de GHC, o simplemente una limitación conocida? o ¿existe realmente una muy buena razón por la cual no hay forma de ver que la coincidencia de patrón en f está completa?

Answer 1

Es molesto, sí. GHC tiene la suposición de que las familias de tipo (y las clases) se abren al horno profundamente en sus algoritmos en todo el lugar; sin embargo, está escribiendo una familia de tipos parametrizada por un tipo cerrado. Esta tensión explica el malentendido entre usted y GHC. Creo que se pensó un poco sobre cómo manejar clases y familias de tipo cerrado, pero es un área difícil.

Mientras tanto, puede evitar la apertura de las familias de caracteres para convencer al verificador de totalidad.

{-# 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 

Answer 2

Siempre puede usar _ para que coincida con cualquier otro patrón en la última condición de la caja.

So _ -> undefined en lugar de BarB _ -> undefined.

Esto hará que el total de casos en su argumento.

También hay un library de Neil Mitchell que comprueba patrones no exhaustivos para evitar fallas en el tiempo de ejecución debido a patrones que no coinciden.