{-# OPTIONS_HADDOCK hide, prune #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Type.List.Internal
( UnreachableConstraint (..)
, type (=->) (..), runMagic, unsafeEqTypes
) where
import Data.Constraint (Dict (..))
import Data.Constraint.Bare
import Data.Kind
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
class UnreachableConstraint (ctx :: Constraint) (msg :: Symbol) where
unreachable :: BareConstraint ctx
instance KnownSymbol msg
=> UnreachableConstraint ctx msg where
unreachable :: BareConstraint ctx
unreachable = [Char] -> BareConstraint ctx
forall a. HasCallStack => [Char] -> a
error ([Char] -> BareConstraint ctx) -> [Char] -> BareConstraint ctx
forall a b. (a -> b) -> a -> b
$ [Char]
"Unreachable constraint:: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Proxy msg -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (Proxy msg
forall k (t :: k). Proxy t
Proxy @msg)
newtype c =-> r = Magic (c => r)
infixr 0 =->
runMagic :: (c =-> r) -> BareConstraint c -> r
runMagic :: (c =-> r) -> BareConstraint c -> r
runMagic = (c =-> r) -> BareConstraint c -> r
forall a b. a -> b
unsafeCoerce
{-# NOINLINE runMagic #-}
unsafeEqTypes :: forall a b
. Dict (a ~ b)
unsafeEqTypes :: Dict (a ~ b)
unsafeEqTypes = Dict (a ~ a) -> Dict (a ~ b)
forall a b. a -> b
unsafeCoerce (Dict (a ~ a)
forall (a :: Constraint). a => Dict a
Dict :: Dict (a ~ a))