{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
module Language.Symantic.Typing.Family where

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

import Language.Symantic.Typing.Type

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

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

-- | Project the 'Constraint' indexed by the given 'Type'
-- onto its proof, captured by 'Con' when it holds.
proj_fam
 :: forall fam cs hs. Proj_Fam cs fam
 => fam -> Types cs hs -> Maybe (Type cs (Fam fam hs))
proj_fam = proj_famR (Proxy::Proxy cs)

-- ** Class 'Proj_FamR'
-- | Intermediate type class to construct an instance of 'Proj_Fam'
-- from many instances of 'Proj_FamC', one for each item of @cs@.
--
-- * @cs@: starting  list of /type constants/.
-- * @rs@: remaining list of /type constants/.
class Proj_FamR cs rs fam where
	proj_famR
	 :: Proxy rs -> fam -> Types cs hs
	 -> Maybe (Type cs (Fam fam hs))
	proj_famR _rs _fam _ty = Nothing

-- | Test whether @c@ handles the work of 'Proj_Fam' or not,
-- or recurse on @rs@, preserving the starting list of /type constants/.
instance
 ( Proj_FamC cs    fam c
 , Proj_FamR cs rs fam
 ) => Proj_FamR cs (Proxy c ': rs) fam where
	proj_famR _rs fam ty =
		proj_famC (Proxy::Proxy c)  fam ty <|>
		proj_famR (Proxy::Proxy rs) fam ty
-- | End the recursion.
instance Proj_FamR cs '[] fam

-- ** Class 'Proj_FamC'
-- | Handle the work of 'Proj_Fam' 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_FamC cs fam c where
	proj_famC
	 :: Proxy c -> fam -> Types cs hs
	 -> Maybe (Type cs (Fam fam hs))
	proj_famC _c _fam _ty = Nothing