Haskell Not 98

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE KindSignatures #-}

data Zero
data Succ a
data Plus a b

data Id :: * -> * -> * where
    Refl :: a -> Id a a
    Symm :: (Id a b) -> Id b a
    Tran :: (Id a b) -> (Id b c) -> (Id a c)
    MapId :: (Id a b) -> (Id (Succ a) (Succ b))
    ZeroPlus :: Id (Plus Zero a) a
    SuccPlus :: Id (Plus (Succ a) b) (Succ (Plus a b))

class Lemma a where
    lemma :: Id (Plus a Zero) a

instance Lemma Zero where
    lemma = ZeroPlus

instance (Lemma a) => Lemma (Succ a) where
    lemma = goal
        where
          hypo :: (Lemma b) => Id (Plus b Zero) b
          hypo = lemma

          p1 :: (Lemma b) => Id (Succ (Plus b Zero)) (Succ b)
          p1 = MapId hypo

          p2 :: (Lemma b) => Id (Plus (Succ b) Zero) (Succ (Plus b Zero))
          p2 = SuccPlus

          goal :: (Lemma b) => Id (Plus (Succ b) Zero) (Succ b)
          goal = Tran p2 p1

クラウドコンピューティングの授業だったので。