{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs, TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.TypeLevel.ParMaybe (M(..), Map, maybe, map, nil) where

import Prelude hiding (map, maybe)
import Data.Kind

data M (t :: k -> Type) (m :: Maybe k) where
	N :: M t 'Nothing
	J :: t a -> M t ('Just a)

deriving instance Show (M t 'Nothing)
deriving instance Show (t a) => Show (M t ('Just a))

deriving instance Eq (M t 'Nothing)
deriving instance Eq (t a) => Eq (M t ('Just a))

deriving instance Ord (M t 'Nothing)
deriving instance Ord (t a) => Ord (M t ('Just a))

type family Map (f :: k -> l) (m :: Maybe k) where
	Map _f 'Nothing = 'Nothing
	Map f ('Just x) = 'Just (f x)

maybe :: a -> (forall s . t s -> a) -> M t ms -> a
maybe :: forall {k} a (t :: k -> *) (ms :: Maybe k).
a -> (forall (s :: k). t s -> a) -> M t ms -> a
maybe a
d forall (s :: k). t s -> a
_ M t ms
N = a
d
maybe a
_ forall (s :: k). t s -> a
f (J t a
x) = t a -> a
forall (s :: k). t s -> a
f t a
x

map :: (forall s . t s -> t' (f s)) -> M t ms -> M t' (Map f ms)
map :: forall {k} {k} (t :: k -> *) (t' :: k -> *) (f :: k -> k)
       (ms :: Maybe k).
(forall (s :: k). t s -> t' (f s)) -> M t ms -> M t' (Map f ms)
map forall (s :: k). t s -> t' (f s)
_ M t ms
N = M t' 'Nothing
M t' (Map f ms)
forall {k} (t :: k -> *). M t 'Nothing
N
map forall (s :: k). t s -> t' (f s)
f (J t a
x) = t' (f a) -> M t' ('Just (f a))
forall {k} (t :: k -> *) (a :: k). t a -> M t ('Just a)
J (t' (f a) -> M t' ('Just (f a))) -> t' (f a) -> M t' ('Just (f a))
forall a b. (a -> b) -> a -> b
$ t a -> t' (f a)
forall (s :: k). t s -> t' (f s)
f t a
x

nil :: M (t :: k -> Type) 'Nothing
nil :: forall {k} (t :: k -> *). M t 'Nothing
nil = M t 'Nothing
forall {k} (t :: k -> *). M t 'Nothing
N