coincidencia de patrones Haskell en GADTs con tipos de datos

Question

Descubrí que realmente me gusta combinar GADT con Data Kinds, ya que me proporciona mayor seguridad de tipo que antes (para la mayoría de los usos, casi tan bueno como Coq, Agda y otros). Tristemente, la coincidencia de patrones falla en los ejemplos más simples, y no se me ocurre la forma de escribir mis funciones, excepto las clases de tipos.

He aquí un ejemplo para explicar mi dolor:

data Nat = Z | S Nat deriving Eq 

data Le :: Nat -> Nat -> * where 
    Le_base :: Le a a 
    Le_S :: Le a b -> Le a (S b) 

class ReformOp n m where 
    reform :: Le (S n) (S m) -> Le n m 

instance ReformOp a a where 
    reform Le_base = Le_base 

instance ReformOp a b => ReformOp a (S b) where 
    reform (Le_S p) = Le_S $ reform p 

class TransThm a b c where 
    trans :: Le a b -> Le b c -> Le a c 

instance TransThm a a a where 
    trans = const 

instance TransThm a a b => TransThm a a (S b) where 
    trans Le_base (Le_S p) = Le_S $ trans Le_base p 

instance (TransThm a b c, ReformOp b c) => TransThm a (S b) (S c) where 
    trans (Le_S p) q = Le_S $ trans p $ reform q 

Tenemos 2 clases de tipos (uno para el teorema, una por una operación de utilidad) y 5 casos - sólo por un teorema trivial. Idealmente, Haskell podría mirar a esta función:

-- not working, I understand why 
trans :: Le a b -> Le b c -> Le a c 
trans Le_base Le_base = Le_base 
trans Le_base (Le_S p) = Le_S $ trans Le_base p 
trans (Le_S p) q = Le_S $ trans p $ reform q 

y tipo a comprobar cada cláusula por sí mismo, y por llamada decidir qué casos son posibles (por lo tanto vale la pena probar para que coincida) y cuáles no, por lo que al llamar trans Le_base Le_base Haskell notará que solo el primer caso permite que las tres variables sean iguales, y solo intenta hacer coincidir la primera cláusula.

Answer 1

No veo cómo funcionaría su definición de coincidencia de patrones de trans en Agda o Coq.

Si se escribe el siguiente lugar, funciona:

reform :: Le (S n) (S m) -> Le n m 
reform Le_base   = Le_base 
reform (Le_S Le_base) = Le_S Le_base 
reform (Le_S (Le_S p)) = Le_S (reform (Le_S p)) 

trans :: Le a b -> Le b c -> Le a c 
trans Le_base q  = q 
trans (Le_S p) Le_base = Le_S p 
trans (Le_S p) (Le_S q) = Le_S (trans p (reform (Le_S q))) 

Por supuesto, también se puede definir de manera más directa:

trans :: Le a b -> Le b c -> Le a c 
trans p Le_base = p 
trans p (Le_S q) = Le_S (trans p q)