{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE CPP #-}
-- We need this otherwise GHC chokes on the export of
-- "type (*)"
#if MIN_VERSION_GLASGOW_HASKELL (8,6,0,0)
{-# LANGUAGE NoStarIsType #-}
#endif
-- | Common type functions
module Haskus.Utils.Types
( Nat
, Symbol
, natValue
, natValue'
, symbolValue
, KnownNat
, KnownSymbol
, CmpNat
, CmpSymbol
, type (<=?)
, type (<=)
, type (+)
, type (-)
, type (*)
, type (^)
, Assert
, If
, Modulo
, Same
, Proxy (..)
, TypeError
, ErrorMessage (..)
)
where
import GHC.TypeLits
import Data.Proxy
-- | Get a Nat value
natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a
{-# INLINE natValue #-}
natValue = fromIntegral (natVal (Proxy :: Proxy n))
-- | Get a Nat value
natValue' :: forall (n :: Nat). KnownNat n => Word
{-# INLINE natValue' #-}
natValue' = natValue @n
-- | Get a Symbol value
symbolValue :: forall (s :: Symbol). (KnownSymbol s) => String
{-# INLINE symbolValue #-}
symbolValue = symbolVal (Proxy :: Proxy s)
-- | If-then-else
type family If (c :: Bool) (t :: k) (e :: k) where
If 'True t e = t
If 'False t e = e
-- | Like: If cond t (TypeError msg)
--
-- The difference is that the TypeError doesn't appear in the RHS of the type
-- which leads to better error messages (see GHC #14771).
--
-- For instance:
-- type family F n where
-- F n = If (n <=? 8) Int8 (TypeError (Text "ERROR"))
--
-- type family G n where
-- G n = Assert (n <=? 8) Int8 (Text "ERROR")
--
-- If GHC cannot solve `F n ~ Word`, it shows: ERROR
-- If GHC cannot solve `G n ~ Word`, it shows:
-- can't match `Assert...` with `Word`
--
type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) where
Assert 'True val msg = val
Assert 'False val msg = TypeError msg
-- | Modulo
type family Modulo (a :: Nat) (b :: Nat) where
Modulo a b = Modulo' (a <=? b) a b
-- | Helper for Modulo
type family Modulo' c a b where
Modulo' 'True a b = a
Modulo' 'False a b = Modulo' ((a-b) <=? b) (a-b) b
-- | Type equality to Nat
type family Same a b :: Nat where
Same a a = 1
Same a b = 0