{-# 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 Data.Maybe (fromMaybe)
import Data.Proxy

import Language.Symantic.Typing.Type

type family Fam fam h0 :: *

-- * 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 h. Proj_Fam cs fam
 => Proxy fam
 -> Type cs h
 -> Maybe (Type cs (Fam fam h))
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 -> Proxy fam -> Type cs h -> Maybe (Type cs (Fam fam h))
	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 (c ': rs) fam where
	proj_famR _rs fam ty =
		proj_famR (Proxy::Proxy rs) fam ty `fromMaybe`
		proj_famC (Proxy::Proxy c)  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 -> Proxy fam -> Type cs h -> Maybe (Maybe (Type cs (Fam fam h)))
	proj_famC _c _fam _ty = Nothing