{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
module Language.Symantic.Typing.Family where

import Control.Applicative ((<|>))
import Data.Proxy
import Data.String (IsString(..))

import Language.Symantic.Parsing
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Type

-- * Type family 'TyFam'
-- | Apply the /type family/ selected by @fam@
-- to a list of types (within a 'Proxy').
type family TyFam fam (hs::[*]) :: *

-- * Type 'Proj_TyFam'
-- | Convenient type synonym wrapping 'Proj_TyFamR'
-- to initiate its recursion.
type Proj_TyFam cs = Proj_TyFamR cs cs

-- | Project the 'Constraint' indexed by the given 'Type'
-- onto its proof, captured by 'Dict' when it holds.
proj_TyFam
 :: forall fam src cs hs.
 Proj_TyFam cs fam
 => fam -> Types src cs hs
 -> Maybe (Type src cs (TyFam fam hs))
proj_TyFam = proj_TyFamR (Proxy @cs)

-- ** Class 'Proj_TyFamR'
-- | Intermediate type class to construct an instance of 'Proj_TyFam'
-- from many instances of 'Proj_TyFamC', one for each item of @cs@.
--
-- * @cs@: starting  list of /type constants/.
-- * @rs@: remaining list of /type constants/.
class Proj_TyFamR (cs::[*]) (rs::[*]) fam where
	proj_TyFamR
	 :: Proxy rs -> fam -> Types src cs hs
	 -> Maybe (Type src cs (TyFam fam hs))
	proj_TyFamR _rs _fam _ty = Nothing

-- | Test whether @c@ handles the work of 'Proj_TyFam' or not,
-- or recurse on @rs@, preserving the starting list of /type constants/.
instance
 ( Proj_TyFamC cs    fam c
 , Proj_TyFamR cs rs fam
 ) => Proj_TyFamR cs (Proxy c ': rs) fam where
	proj_TyFamR _rs fam typ =
		proj_TyFamC (Proxy @c)  fam typ <|>
		proj_TyFamR (Proxy @rs) fam typ
-- | End the recursion.
instance Proj_TyFamR cs '[] fam

-- ** Class 'Proj_TyFamC'
-- | Handle the work of 'Proj_TyFam' for a given /type family/ @fam@ and /type constant/ @c@,
-- that is: maybe it handles the given /type family/,
-- and if so, maybe the /type family/ has an instance for the given 'Type'.
class Proj_TyFamC cs fam (c::kc) where
	proj_TyFamC
	 :: Proxy c -> fam -> Types src cs hs
	 -> Maybe (Type src cs (TyFam fam hs))
	proj_TyFamC _c _fam _ty = Nothing

unTyFam
 :: ( Inj_Error (Con_Type src cs) err
    , Proj_TyFam cs fam
    , Show fam )
 => At src fam
 -> Types src cs hs
 -> (Type src cs (TyFam fam hs) -> Either err ret)
 -> Either err ret
unTyFam fam tys k =
	case proj_TyFam (unAt fam) tys of
	 Just t -> k t
	 Nothing -> Left $ inj_Error $
		Con_TyFam
		 (fromString . show <$> fam)
		 (eTypes tys)