{-# LANGUAGE DataKinds, GADTs #-}

{-|
Description : Utilities for manipulating runtime representations of compile-time lists
Copyright   : Richard Eisenberg
License     : MIT
Maintainer  : rae@richarde.dev
Stability   : experimental

Provides utilities for manipulating a 'TypeRep' of compile-time lists.

-}

module Type.Reflection.List (
  typeRepList, typeRepListKind,
  ) where

import Type.Reflection
import Data.SOP.NP

-- | Given a representation of a list, get a representation of the kind of the list's
-- elements.
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

-- | Turn a representation of a list into a list of representations.
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