{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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.Constant
import Language.Symantic.Typing.Type

-- * 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 ctx ss cs hs.
 Proj_TyFam cs fam
 => fam -> TypesKi src ctx ss cs hs
 -> Maybe (Type src ctx ss 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 -> TypesKi src ctx ss cs hs
	 -> Maybe (Type src ctx ss 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 the /type family/ has an instance for the given 'TypesKi'.
class Proj_TyFamC cs fam (c::kc) where
	proj_TyFamC
	 :: Proxy c -> fam -> TypesKi src ctx ss cs hs
	 -> Maybe (Type src ctx ss cs (TyFam fam hs))
	proj_TyFamC _c _fam _ty = Nothing

unTyFam
 :: ( Inj_Error (Con_Type src ctx ss cs) err
    , Proj_TyFam cs fam
    , Show fam )
 => At src fam
 -> TypesKi src ctx ss cs hs
 -> (Type src ctx ss 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)
		 (eTypesKi tys)

-- | Like 'TyFam', but 'sourceLess'.
--
-- NOTE: to be use with @TypeApplications@.
tyFam :: forall fam hs ss cs src ctx.
 Source src
 => Inj_TyConst cs fam
 => Types src ctx ss cs hs
 -> Type src ctx ss cs (TyFam fam hs)
tyFam = TyFam sourceLess (inj_TyConst @fam)
 -- NOTE: this requires @AllowAmbiguousTypes@.

{-
tyFam
 :: Source src
 => Proj_TyFam cs fam
 => fam -> TypesKi src ctx ss cs hs
 -> Type src ctx ss cs (TyFam fam hs)
tyFam fam hs =
	case proj_TyFam fam hs of
	 Just h  -> h
	 Nothing -> undefined
infix 1 `tyFam`

tyQuant
 :: forall src ctx ss cs kv k.
    Source src
 => Inj_Kind kv
 => NameHint
 -> (forall (v::kv). Type src ctx ss cs v -> KT src ctx ss cs k)
 -> KT src ctx ss cs k
tyQuant n f = KT $ TyQuant sourceLess n inj_Kind f
-}