{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RoleAnnotations #-}
#if !defined(__HLINT__)
{-# LANGUAGE StandaloneDeriving #-}
#endif
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module DependentLiterals.Bounds
(
OutOfRangeMsg
, ShowTypedNum, ShowRange
, OutOfRangeErr
, CheckLessThanMaxBound, CheckAtLeastMinBound, AssertEq, AssertNotApart
, ShowNum, AssertNotApart_, Eql, FailedToProveEq
) where
import Data.Kind (Constraint, Type)
import GHC.TypeLits (TypeError, ErrorMessage(..))
import Kinds.Integer (pattern Pos, pattern Neg)
import Kinds.Num (type (-))
import Kinds.Ord (type (>=?), type (<?), type (<), type (>=))
import qualified Kinds.Integer as K (Integer)
type family ShowNum (n :: K.Integer) where
ShowNum ('Pos n) = 'ShowType n
ShowNum ('Neg n) = 'Text "-" ':<>: 'ShowType n
type ShowTypedNum a n = ShowNum n ':<>: 'Text " :: " ':<>: 'ShowType a
type ShowRange min maxp1 =
'Text "(" ':<>: ShowNum min ':<>: 'Text ".." ':<>:
ShowNum (maxp1 - 'Pos 1) ':<>: 'Text ")"
type OutOfRangeMsg min maxp1 a n =
'Text "Literal out of range " ':<>: ShowRange min maxp1 ':<>: 'Text ":" ':$$:
'Text " " ':<>: ShowTypedNum a n
class OutOfRangeErr (min :: K.Integer) (maxp1 :: K.Integer) (a :: Type) (n :: K.Integer)
instance TypeError (OutOfRangeMsg min maxp1 a n) => OutOfRangeErr min maxp1 a n
type family Eql a b :: Bool where
Eql a a = 'True
Eql a b = 'False
class a ~ b => AssertEq (c :: Constraint) a b
instance AssertEq c a a
class a ~ b => FailedToProveEq (err :: Constraint) a b
class a ~ b => AssertNotApart_ (msg :: ErrorMessage) eq a b
instance a ~ b => AssertNotApart_ msg 'True a b
instance FailedToProveEq (TypeError msg) a b => AssertNotApart_ msg 'False a b
type AssertNotApart msg a b = AssertNotApart_ msg (Eql a b) a b
class (n < maxp1)
=> CheckLessThanMaxBound
(msg :: ErrorMessage)
(maxp1 :: K.Integer)
(a :: Type)
(n :: K.Integer)
instance AssertNotApart msg (n <? maxp1) 'True
=> CheckLessThanMaxBound msg maxp1 a n
class (n >= min)
=> CheckAtLeastMinBound
(msg :: ErrorMessage)
(min :: K.Integer)
(a :: Type)
(n :: K.Integer)
instance AssertNotApart msg (n >=? min) 'True
=> CheckAtLeastMinBound msg min a n