{-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}
-----------------------------------------------------------------------------
-- |
-- 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.Semigroup
import Prelude

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

instance Show (Is a b) where
  showsPrec :: Int -> Is a b -> ShowS
showsPrec Int
_ Is a b
Refl = String -> ShowS
showString String
"Refl"

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

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

instance (a ~ b) => Semigroup (Is a b) where
  Is a b
Refl <> :: Is a b -> Is a b -> Is a b
<> Is a b
Refl = Is a b
forall a. Is a a
Refl
  {-# INLINE (<>) #-}

instance (a ~ b) => Monoid (Is a b) where
  mempty :: Is a b
mempty = Is a b
forall a. Is a a
Refl
  {-# INLINE mempty #-}
  mappend :: Is a b -> Is a b -> Is a b
mappend = Is a b -> Is a b -> Is a b
forall a. Semigroup a => a -> a -> a
(<>)
  {-# INLINE mappend #-}

instance (a ~ b) => Read (Is a b) where
  readsPrec :: Int -> ReadS (Is a b)
readsPrec Int
d = Bool -> ReadS (Is a a) -> ReadS (Is a a)
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (\String
r -> [(Is a a
forall a. Is a a
Refl,String
s) | (String
"Refl",String
s) <- ReadS String
lex String
r ])

instance Category Is where
  id :: Is a a
id = Is a a
forall a. Is a a
Refl
  {-# INLINE id #-}
  Is b c
Refl . :: Is b c -> Is a b -> Is a c
. Is a b
Refl = Is a c
forall a. Is a a
Refl
  {-# INLINE (.) #-}