Haskell pattern matching on GADTs with Data Kinds

data-kinds, gadt, haskell, pattern-matching

Solution

I don't see how your pattern-matching definition of `trans` would work in Agda or Coq.

If you write the following instead, it works:

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)))

Of course, you could also more directly define:

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)

Problem

I have found that I really like combining GADTs with Data Kinds, as it gives me further type safety than before (for most uses, almost as good as Coq, Agda et al.). Sadly, pattern matching fails on the simplest of examples, and I could think of no way to write my functions except for type classes. Here's an example to explain my sorrow: ``` 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 ``` We have 2 type classes (one for the theorem, one for a utility operation) and 5 instances - just for a trivial theorem. Ideally, Haskell could look at this function: ``` -- 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 ``` And type-check each clause on its own, and per-call decide which cases are possible (thus worth trying to match) and which are not, so when calling `trans Le_base Le_base` Haskell will notice that only the first case allows for the three variables to be the same, and only attempt matching on the first clause.

Original source