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

import Language.Symantic.Type

-- * Type 'Expr_Root'
-- | The root expression, passing itself as parameter to the given expression.
newtype Expr_Root (ex:: * -> *)
 =      Expr_Root (ex (Expr_Root ex))
type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
type instance Type_of_Expr (Expr_Root ex) = Type_of_Expr (ex (Expr_Root ex))

-- * Type family 'Root_of_Expr'
-- | The root expression of an expression.
type family Root_of_Expr (ex:: *) :: *

-- * Type family 'Type_of_Expr'
-- | The type of an expression, parameterized by a root type.
type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *

-- ** Type 'Type_Root_of_Expr'
-- | Convenient alias.
--
-- NOTE: include 'Type_Var' only to use it
-- within 'Error_Expr_Type_mismatch' so far.
type Type_Root_of_Expr (ex:: *)
 =   Type_Root (Type_Var0 :|: Type_Var1 :|: Type_of_Expr (Root_of_Expr ex))