{-# LANGUAGE DataKinds, GADTs #-}
module Type.Reflection.List (
typeRepList, typeRepListKind,
) where
import Type.Reflection
import Data.SOP.NP
typeRepListKind :: TypeRep @[k] xs -> TypeRep k
typeRepListKind :: forall k (xs :: [k]). TypeRep xs -> TypeRep k
typeRepListKind TypeRep xs
tr
| App TypeRep a
_list TypeRep b
tr_k <- forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep xs
tr
= TypeRep b
tr_k
typeRepList :: forall {k} (xs :: [k]). TypeRep xs -> NP TypeRep xs
typeRepList :: forall {k} (xs :: [k]). TypeRep xs -> NP TypeRep xs
typeRepList TypeRep xs
tr_list
| App (App TypeRep a
cons TypeRep b
tr) TypeRep b
trs <- TypeRep xs
tr_list
, Just a :~~: (':)
HRefl <- forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
cons (forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep k
tr_k forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). Typeable a => TypeRep a
typeRep @((:) @k))
= TypeRep b
tr forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (xs :: [k]). TypeRep xs -> NP TypeRep xs
typeRepList TypeRep b
trs
| Just xs :~~: '[]
HRefl <- forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep xs
tr_list (forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep k
tr_k forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). Typeable a => TypeRep a
typeRep @('[] @k))
= forall {k} (a :: k -> *). NP a '[]
Nil
| Bool
otherwise
= forall a. HasCallStack => [Char] -> a
error [Char]
"list is neither (:) nor []."
where
tr_k :: TypeRep k
tr_k = forall k (xs :: [k]). TypeRep xs -> TypeRep k
typeRepListKind TypeRep xs
tr_list