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

import Data.Proxy

import Language.Symantic.Type.Common

-- * Type 'Type_Maybe'
type Type_Maybe = Type_Type1 Maybe
instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_Maybe root) where
	string_from_type (Type_Type1 _f a) =
		"Maybe" ++ " (" ++ string_from_type a ++ ")"

-- | Inject a 'Type_Maybe' within a root type.
type_maybe
 :: Type_Root_Lift Type_Maybe root
 => root h_a
 -> root (Maybe h_a)
type_maybe = type_root_lift . Type_Type1 (Proxy::Proxy Maybe)

is_type_maybe
 :: forall tys (root:: * -> *) h.
 Type_Unlift Type_Maybe tys =>
 tys root h -> Maybe (Type_Maybe root h)
is_type_maybe = type_unlift

instance
 ( Type_Root_Lift Type_Maybe root
 , Type_Unlift Type_Maybe root'
 , Error_Type_Lift (Error_Type (Type_Root root' h)) (Error_of_Type (Type_Root root' h) root)
 , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
 ) => Type1_from (Type_Root root' h) (Type_Maybe root) where
	type1_from ty root_x k =
		case is_type_maybe $ unType_Root root_x of
		 Just _ty_a -> k (Proxy::Proxy Maybe) type_maybe
		 Nothing -> Left $ error_type_unsupported ty root_x