(original) (raw)

{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}

module Data.Type.Equality (

(:~:)(..), type (~~), (:~~:)(..),

sym, trans, castWith, gcastWith, apply, inner, outer,

TestEquality(..),

type (==) ) where

import Data.Maybe import GHC.Enum import GHC.Show import GHC.Read import GHC.Base import Data.Type.Bool

infix 4 :~:, :~~:

data a :~: b where
Refl :: a :~: a

sym :: (a :~: b) -> (b :~: a) sym :: forall {k} (a :: k) (b :: k). (a :: b) -> b :: a sym a :: b Refl = b :: a forall {k} (a :: k). a :~: a Refl

trans :: (a :~: b) -> (b :~: c) -> (a :~: c) trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :: b) -> (b :: c) -> a :: c trans a :: b Refl b :: c Refl = a :: c forall {k} (a :: k). a :~: a Refl

castWith :: (a :~: b) -> a -> b castWith :: forall a b. (a :: b) -> a -> b castWith a :: b Refl a x = a b x

gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r gcastWith :: forall {k} (a :: k) (b :: k) r. (a :: b) -> ((a ~ b) => r) -> r gcastWith a :: b Refl (a ~ b) => r x = r (a ~ b) => r x

apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b) apply :: forall {k} {k} (f :: k -> k) (g :: k -> k) (a :: k) (b :: k). (f :: g) -> (a :: b) -> f a :: g b apply f :: g Refl a :: b Refl = f a :: g b forall {k} (a :: k). a :~: a Refl

inner :: (f a :~: g b) -> (a :~: b) inner :: forall {k} {k} (f :: k -> k) (a :: k) (g :: k -> k) (b :: k). (f a :: g b) -> a :: b inner f a :: g b Refl = a :: b forall {k} (a :: k). a :~: a Refl

outer :: (f a :~: g b) -> (f :~: g) outer :: forall {k} {k} (f :: k -> k) (a :: k) (g :: k -> k) (b :: k). (f a :: g b) -> f :: g outer f a :: g b Refl = f :: g forall {k} (a :: k). a :~: a Refl

deriving instance Eq (a :~: b)

deriving instance Show (a :~: b)

deriving instance Ord (a :~: b)

deriving instance a ~ b => Read (a :~: b)

instance a ~ b => Enum (a :~: b) where toEnum :: Int -> a :: b toEnum Int 0 = a :: b forall {k} (a :: k). a :: a Refl toEnum Int _ = String -> a :: b forall a. String -> a errorWithoutStackTrace String "Data.Type.Equality.toEnum: bad argument"

fromEnum :: (a :: b) -> Int fromEnum a :: b Refl = Int 0

deriving instance a ~ b => Bounded (a :~: b)

type (:~~:) :: k1 -> k2 -> Type data a :~~: b where HRefl :: a :~~: a

deriving instance Eq (a :~~: b)

deriving instance Show (a :~~: b)

deriving instance Ord (a :~~: b)

deriving instance a ~~ b => Read (a :~~: b)

instance a ~~ b => Enum (a :~~: b) where toEnum :: Int -> a :: b toEnum Int 0 = a :: b forall {k2} (a :: k2). a :: a HRefl toEnum Int _ = String -> a :: b forall a. String -> a errorWithoutStackTrace String "Data.Type.Equality.toEnum: bad argument"

fromEnum :: (a :: b) -> Int fromEnum a :: b HRefl = Int 0

deriving instance a ~~ b => Bounded (a :~~: b)

class TestEquality f where

testEquality :: f a -> f b -> Maybe (a :~: b)

instance TestEquality ((:~:) a) where testEquality :: forall (a :: k) (b :: k). (a :: a) -> (a :: b) -> Maybe (a :: b) testEquality a :: a Refl a :: b Refl = (a :: b) -> Maybe (a :: b) forall a. a -> Maybe a Just a :: b forall {k} (a :: k). a :~: a Refl

instance TestEquality ((:~~:) a) where testEquality :: forall (a :: k) (b :: k). (a :: a) -> (a :: b) -> Maybe (a :: b) testEquality a :: a HRefl a :: b HRefl = (a :: b) -> Maybe (a :: b) forall a. a -> Maybe a Just a :: b forall {k} (a :: k). a :~: a Refl

infix 4 ==

type (==) :: k -> k -> Bool type family a == b where f a == g b = f == g && a == b a == a = 'True _ == _ = 'False