{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Type Families.
module Language.Symantic.Type.Family where

import Data.Proxy (Proxy(..))
import qualified Data.MonoTraversable as MT

import Language.Symantic.Type.Error
import Language.Symantic.Type.Root
import Language.Symantic.Type.Alt

-- * Type 'Host_of_Type0_Family'
type family Host_of_Type0_Family ta h0 :: *

-- * Type 'Type_Family_MonoElement'
-- | Proxy type for 'MT.Element'.
data Type_Family_MonoElement
type instance Host_of_Type0_Family Type_Family_MonoElement h = MT.Element h

-- * Class 'Type0_Family'
class Type0_Family (ta:: *) (ty:: * -> *) where
	type0_family
	 :: forall h0. Proxy ta -> ty h0
	 -> Maybe (Root_of_Type ty (Host_of_Type0_Family ta h0))
	type0_family _tf _ty = Nothing
instance -- Type_Root
 ( Type0_Family ta (ty (Type_Root ty))
 , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 ) => Type0_Family ta (Type_Root ty) where
	type0_family ta (Type_Root ty) = type0_family ta ty
instance -- Type_Alt
 ( Type0_Family ta (curr root)
 , Type0_Family ta (next root)
 , Root_of_Type (curr root) ~ root
 , Root_of_Type (next root) ~ root
 ) => Type0_Family ta (Type_Alt curr next root) where
	type0_family ta (Type_Alt_Curr ty) = type0_family ta ty
	type0_family ta (Type_Alt_Next ty) = type0_family ta ty

-- | Parsing utility to check that an associated type is supported,
-- or raise 'Error_Type_No_Type0_Family'.
check_type_type0_family
 :: forall ast ty ta h ret.
 ( Error_Type_Lift (Error_Type ast) (Error_of_Type ast ty)
 , Type0_Family ta ty
 , Root_of_Type ty ~ ty
 ) => Proxy ta -> ast -> ty h
 -> (ty (Host_of_Type0_Family ta h) -> Either (Error_of_Type ast ty) ret)
 -> Either (Error_of_Type ast ty) ret
check_type_type0_family ta ast ty k =
	case type0_family ta ty of
	 Just t -> k t
	 Nothing -> Left $ error_type_lift $
		Error_Type_No_Type_Family ast -- (Exists_Type0 ty)