GADTs and Kind

[shnarazk]

{-# LANGUAGE TypeFamilies, DataKinds, GADTs, StandaloneDeriving, FlexibleInstances #-}
module Clause where
-- import Unsafe.Coerce

data ClauseKind = OfNormal | NullCaluse | BinaryClause

data Clause (a :: ClauseKind) where
  MkClause :: [Int] -> Clause 'OfNormal
  MkBinaryClause :: Int -> Clause 'BinaryClause

instance Eq (Clause a) where
  (MkBinaryClause a) == (MkBinaryClause b) = a == b
  _ == _ = undefined

instance Show (Clause a) where
  show (MkBinaryClause l) = "B{" ++ show l ++ "}"
  show (MkClause _) = show "Clause"
  
-- data Clause (a :: ClauseKind) = Clause [Int] deriving (Eq, Show)

c :: [Clause 'OfNormal]
c = []