{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Type.Root where

-- * Type 'Type_Root'
-- | The root type, passing itself as parameter to the given type.
newtype Type_Root (ty:: (* -> *) -> * -> *) h
 =      Type_Root { unType_Root :: ty (Type_Root ty) h }
type instance Root_of_Type (Type_Root ty) = Type_Root ty

-- ** Type family 'Root_of_Type'
-- | Return the root type of a type.
type family Root_of_Type (ty:: * -> *) :: * -> *

-- ** Class 'Type_Root_Lift'
-- | Lift a given type to a given root type.
class Type_Root_Lift ty root where
	type_root_lift :: forall h. ty root h -> root h