{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE PolyKinds #-}
module Numeric.Type.Evidence
( Evidence (..), withEvidence, sumEvs, (+!+)
, Evidence' (..), toEvidence, toEvidence'
) where
import GHC.Base (Type)
import GHC.Exts (Constraint)
data Evidence :: Constraint -> Type where
E :: a => Evidence a
sumEvs :: Evidence a -> Evidence b -> Evidence (a,b)
sumEvs E E = E
{-# INLINE sumEvs #-}
infixl 4 +!+
(+!+) :: Evidence a -> Evidence b -> Evidence (a,b)
(+!+) = sumEvs
{-# INLINE (+!+) #-}
withEvidence :: Evidence a -> (a => r) -> r
withEvidence d r = case d of E -> r
{-# INLINE withEvidence #-}
data Evidence' :: (k -> Constraint) -> k -> Type where
E' :: c a => Evidence' c a
toEvidence :: Evidence' c a -> Evidence (c a)
toEvidence E' = E
{-# INLINE toEvidence #-}
toEvidence' :: Evidence (c a) -> Evidence' c a
toEvidence' E = E'
{-# INLINE toEvidence' #-}