src/Data/Machine/Is.hs

{-# LANGUAGE GADTs, TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Machine.Is
-- Copyright : (C) 2012 Edward Kmett
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability : provisional
-- Portability : GADTs, Type Families
--
----------------------------------------------------------------------------
module Data.Machine.Is
 ( Is(..)
 ) where

import Control.Category
import Data.Monoid

-- | Witnessed type equality
data Is a b where
 Refl :: Is a a

instance Show (Is a b) where
 showsPrec _ Refl = showString "Refl"

instance Eq (Is a b) where
 Refl == Refl = True
 {-# INLINE (==) #-}

instance Ord (Is a b) where
 Refl `compare` Refl = EQ
 {-# INLINE compare #-}

instance (a ~ b) => Monoid (Is a b) where
 mempty = Refl
 {-# INLINE mempty #-}
 mappend Refl Refl = Refl
 {-# INLINE mappend #-}

instance (a ~ b) => Read (Is a b) where
 readsPrec d = readParen (d > 10) (\r -> [(Refl,s) | ("Refl",s) <- lex r ])

instance Category Is where
 id = Refl
 {-# INLINE id #-}
 Refl . Refl = Refl
 {-# INLINE (.) #-}