    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    module Data.Parameterized.BoolRepr
      ( module Data.Type.Bool
      , BoolRepr(..)
      , ifRepr, notRepr, (%&&), (%||)
      , KnownBool

      , someBool

      -- * Re-exports
      , TestEquality(..)
      , (:~:)(..)
      , Data.Parameterized.Some.Some
      )
    where

    import           Data.Parameterized.Classes
    import           Data.Parameterized.DecidableEq
    import           Data.Parameterized.Some

    import           Data.Type.Bool

    -- | A Boolean flag
    data BoolRepr (b :: Bool) where
      FalseRepr :: BoolRepr 'False
      TrueRepr  :: BoolRepr 'True

    -- | conditional
    ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
    ifRepr :: forall (a :: Bool) (b :: Bool) (c :: Bool).
    BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
    ifRepr BoolRepr a
    TrueRepr BoolRepr b
    b BoolRepr c
    _ = BoolRepr b
    BoolRepr (If a b c)
    b
    ifRepr BoolRepr a
    FalseRepr BoolRepr b
    _ BoolRepr c
    c = BoolRepr c
    BoolRepr (If a b c)
    c

    -- | negation
    notRepr :: BoolRepr b -> BoolRepr (Not b)
    notRepr :: forall (b :: Bool). BoolRepr b -> BoolRepr (Not b)
    notRepr BoolRepr b
    TrueRepr = BoolRepr 'False
    BoolRepr (Not b)
    FalseRepr
    notRepr BoolRepr b
    FalseRepr = BoolRepr 'True
    BoolRepr (Not b)
    TrueRepr

    -- | Conjunction
    (%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
    BoolRepr a
    FalseRepr %&& :: forall (a :: Bool) (b :: Bool).
    BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
    %&& BoolRepr b
    _ = BoolRepr 'False
    BoolRepr (a && b)
    FalseRepr
    BoolRepr a
    TrueRepr  %&& BoolRepr b
    a = BoolRepr b
    BoolRepr (a && b)
    a
    infixr 3 %&&

    -- | Disjunction
    (%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
    BoolRepr a
    FalseRepr %|| :: forall (a :: Bool) (b :: Bool).
    BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
    %|| BoolRepr b
    a = BoolRepr b
    BoolRepr (a || b)
    a
    BoolRepr a
    TrueRepr  %|| BoolRepr b
    _ = BoolRepr 'True
    BoolRepr (a || b)
    TrueRepr
    infixr 2 %||

    instance Hashable (BoolRepr n) where
      hashWithSalt :: Int -> BoolRepr n -> Int
    hashWithSalt Int
    i BoolRepr n
    TrueRepr  = Int -> Bool -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    i Bool
    True
      hashWithSalt Int
    i BoolRepr n
    FalseRepr = Int -> Bool -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    i Bool
    False

    instance Eq (BoolRepr m) where
      BoolRepr m
    _ == :: BoolRepr m -> BoolRepr m -> Bool
    == BoolRepr m
    _ = Bool
    True

    instance EqF BoolRepr where
      eqF :: forall (m :: Bool). BoolRepr m -> BoolRepr m -> Bool
    eqF BoolRepr a
    _ BoolRepr a
    _ = Bool
    True

    instance TestEquality BoolRepr where
      testEquality :: forall (a :: Bool) (b :: Bool).
    BoolRepr a -> BoolRepr b -> Maybe (a :~: b)
    testEquality BoolRepr a
    TrueRepr BoolRepr b
    TrueRepr   = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality BoolRepr a
    FalseRepr BoolRepr b
    FalseRepr = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      testEquality BoolRepr a
    _ BoolRepr b
    _ = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance DecidableEq BoolRepr where
      decEq :: forall (a :: Bool) (b :: Bool).
    BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void)
    decEq BoolRepr a
    TrueRepr  BoolRepr b
    TrueRepr  = (a :~: b) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. a -> Either a b
    Left a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      decEq BoolRepr a
    FalseRepr BoolRepr b
    FalseRepr = (a :~: b) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. a -> Either a b
    Left a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
      decEq BoolRepr a
    TrueRepr  BoolRepr b
    FalseRepr = ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. b -> Either a b
    Right (((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void))
    -> ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. (a -> b) -> a -> b
    $ \case {}
      decEq BoolRepr a
    FalseRepr BoolRepr b
    TrueRepr  = ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. b -> Either a b
    Right (((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void))
    -> ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. (a -> b) -> a -> b
    $ \case {}

    instance OrdF BoolRepr where
      compareF :: forall (x :: Bool) (y :: Bool).
    BoolRepr x -> BoolRepr y -> OrderingF x y
    compareF BoolRepr x
    TrueRepr  BoolRepr y
    TrueRepr  = OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
      compareF BoolRepr x
    FalseRepr BoolRepr y
    FalseRepr = OrderingF x x
    OrderingF x y
    forall {k} (x :: k). OrderingF x x
    EQF
      compareF BoolRepr x
    TrueRepr  BoolRepr y
    FalseRepr = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
      compareF BoolRepr x
    FalseRepr BoolRepr y
    TrueRepr  = OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF

    instance PolyEq (BoolRepr m) (BoolRepr n) where
      polyEqF :: BoolRepr m -> BoolRepr n -> Maybe (BoolRepr m :~: BoolRepr n)
    polyEqF BoolRepr m
    x BoolRepr n
    y = (\m :~: n
    Refl -> BoolRepr m :~: BoolRepr m
    BoolRepr m :~: BoolRepr n
    forall {k} (a :: k). a :~: a
    Refl) ((m :~: n) -> BoolRepr m :~: BoolRepr n)
    -> Maybe (m :~: n) -> Maybe (BoolRepr m :~: BoolRepr n)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BoolRepr m -> BoolRepr n -> Maybe (m :~: n)
    forall (a :: Bool) (b :: Bool).
    BoolRepr a -> BoolRepr b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality BoolRepr m
    x BoolRepr n
    y

    instance Show (BoolRepr m) where
      show :: BoolRepr m -> String
    show BoolRepr m
    FalseRepr = String
    "FalseRepr"
      show BoolRepr m
    TrueRepr  = String
    "TrueRepr"

    instance ShowF BoolRepr

    instance HashableF BoolRepr where
      hashWithSaltF :: forall (n :: Bool). Int -> BoolRepr n -> Int
    hashWithSaltF = Int -> BoolRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt

    ----------------------------------------------------------
    -- * Implicit runtime booleans

    type KnownBool = KnownRepr BoolRepr

    instance KnownRepr BoolRepr 'True where
      knownRepr :: BoolRepr 'True
    knownRepr = BoolRepr 'True
    TrueRepr
    instance KnownRepr BoolRepr 'False where
      knownRepr :: BoolRepr 'False
    knownRepr = BoolRepr 'False
    FalseRepr

    someBool :: Bool -> Some BoolRepr
    someBool :: Bool -> Some BoolRepr
    someBool Bool
    True  = BoolRepr 'True -> Some BoolRepr
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some BoolRepr 'True
    TrueRepr
    someBool Bool
    False = BoolRepr 'False -> Some BoolRepr
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some BoolRepr 'False
    FalseRepr