{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Constraint where

import Data.Maybe (fromMaybe)
import Data.Proxy
import Data.Type.Equality
import GHC.Prim (Constraint)

import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Constant
import Language.Symantic.Typing.Type

-- * Type 'Dict'
-- | 'Dict' captures the dictionary of a 'Constraint':
-- pattern matching on the 'Dict' constructor
-- brings the 'Constraint' into scope.
data Dict :: Constraint -> * where
	Dict :: c => Dict c

-- * Type family 'Consts_imported_by'
-- | Return the /type constant/s that a given /type constant/
-- wants to be part of the final list of /type constants/.
type family Consts_imported_by (c::k) :: [*]
type instance Consts_imported_by [] =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Traversable
 ]
type instance Consts_imported_by (->) =
 [ Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 ]
type instance Consts_imported_by Applicative = '[]
type instance Consts_imported_by Bool =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Ord
 ]
type instance Consts_imported_by Bounded = '[]
type instance Consts_imported_by Eq = '[]
type instance Consts_imported_by Enum = '[]
type instance Consts_imported_by Foldable = '[]
type instance Consts_imported_by Functor = '[]
type instance Consts_imported_by Int =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 ]
type instance Consts_imported_by Integer =
 [ Proxy Enum
 , Proxy Eq
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 ]
type instance Consts_imported_by Integral =
 [ Proxy Enum
 , Proxy Real
 ]
type instance Consts_imported_by IO =
 [ Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 ]
type instance Consts_imported_by Maybe =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Traversable
 ]
type instance Consts_imported_by Monad = '[]
type instance Consts_imported_by Monoid = '[]
type instance Consts_imported_by Num = '[]
type instance Consts_imported_by Ord = '[]
type instance Consts_imported_by Real = '[]
type instance Consts_imported_by Traversable = '[]

-- * Type 'Proj_Con'
-- | Convenient type synonym wrapping 'Proj_ConR'
-- initiating its recursion.
type Proj_Con cs = Proj_ConR cs cs

-- | Project a /type class/ constructor
-- applied to a parameter onto a 'Constraint'.
proj_con
 :: forall cs q x ki_x. Proj_Con cs
 => Type cs (ki_x ':> 'KiCon) q -- ^ 'Constraint' constructor.
 -> Type cs ki_x x -- ^ Parameter for the 'Constraint' constructor.
 -> Maybe (Dict (Con q x)) -- ^ 'Constraint' projected onto.
proj_con = proj_conR (Proxy::Proxy cs)

-- ** Class 'Proj_ConR'
-- | Intermediate type class to construct an instance of 'Proj_Con'
-- from many instances of 'Proj_ConC', one for each 'Const' of @cs@.
--
-- * @cs@: starting  list of /type constants/.
-- * @rs@: remaining list of /type constants/.
class Proj_ConR cs rs where
	proj_conR
	 :: Proxy rs
	 -> Type cs (ki_x ':> 'KiCon) q
	 -> Type cs ki_x x
	 -> Maybe (Dict (Con q x))
	proj_conR _c _x _y = Nothing

-- | Test whether @c@ handles the work of 'Proj_Con' or not,
-- or recurse on @rs@, preserving the starting list of /type constants/.
instance
 ( Proj_ConC cs c
 , Proj_ConR cs rs
 ) => Proj_ConR cs (c ': rs) where
	proj_conR _cs x y =
		proj_conR (Proxy::Proxy rs) x y `fromMaybe`
		proj_conC (Proxy::Proxy c)  x y
-- | End the recursion.
instance Proj_ConR cs '[] where
	proj_conR _cs _x _y = Nothing

-- ** Class 'Proj_ConC'
class Proj_ConC cs c where
	proj_conC
	 :: Proxy c
	 -> Type cs (ki_x ':> 'KiCon) q
	 -> Type cs ki_x x
	 -> Maybe (Maybe (Dict (Con q x)))
	proj_conC _c _x _y = Nothing

instance -- []
 ( Proj_Const cs (Proxy [])
 , Proj_Consts cs (Consts_imported_by [])
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy []) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy [])
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Dict
		 _ -> Nothing
	proj_conC _ x (TyConst c :$ a)
	 | Just Refl <- proj_const c (Proxy::Proxy [])
	 = Just $ case x of
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Eq)
		  , Just Dict <- proj_con t a -> Just Dict
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		  , Just Dict <- proj_con t a -> Just Dict
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Ord)
		  , Just Dict <- proj_con t a -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- (->)
 ( Proj_Const cs (Proxy (->))
 , Proj_Consts cs (Consts_imported_by (->))
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy (->)) where
	proj_conC _ x (TyConst c :$ _r)
	 | Just Refl <- proj_const c (Proxy::Proxy (->))
	 = Just $ case x of
		 (TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
		 _ -> Nothing
	proj_conC _ x (TyConst c :$ _a :$ b)
	 | Just Refl <- proj_const c (Proxy::Proxy (->))
	 = Just $ case x of
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		  , Just Dict <- proj_con t b
		  -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Applicative
 ( Proj_Const cs (Proxy Applicative)
 , Proj_Consts cs (Consts_imported_by Applicative)
 ) => Proj_ConC cs (Proxy Applicative)
instance -- Bool
 ( Proj_Const cs (Proxy Bool)
 , Proj_Consts cs (Consts_imported_by Bool)
 ) => Proj_ConC cs (Proxy Bool) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy Bool)
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Bounded) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Enum)    -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Eq)      -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Ord)     -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Bounded
 ( Proj_Const cs (Proxy Bounded)
 , Proj_Consts cs (Consts_imported_by Bounded)
 ) => Proj_ConC cs (Proxy Bounded)
instance -- Enum
 ( Proj_Const cs (Proxy Enum)
 , Proj_Consts cs (Consts_imported_by Enum)
 ) => Proj_ConC cs (Proxy Enum)
instance -- Eq
 ( Proj_Const cs (Proxy Eq)
 , Proj_Consts cs (Consts_imported_by Eq)
 ) => Proj_ConC cs (Proxy Eq)
instance -- Foldable
 ( Proj_Const cs (Proxy Foldable)
 , Proj_Consts cs (Consts_imported_by Foldable)
 ) => Proj_ConC cs (Proxy Foldable)
instance -- Functor
 ( Proj_Const cs (Proxy Functor)
 , Proj_Consts cs (Consts_imported_by Functor)
 ) => Proj_ConC cs (Proxy Functor)
instance -- Int
 ( Proj_Const cs (Proxy Int)
 , Proj_Consts cs (Consts_imported_by Int)
 ) => Proj_ConC cs (Proxy Int) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy Int)
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Integer
 ( Proj_Const cs (Proxy Integer)
 , Proj_Consts cs (Consts_imported_by Integer)
 ) => Proj_ConC cs (Proxy Integer) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy Integer)
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Integral) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Num)      -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Real)     -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Integral
 ( Proj_Const cs (Proxy Integral)
 , Proj_Consts cs (Consts_imported_by Integral)
 ) => Proj_ConC cs (Proxy Integral)
instance -- IO
 ( Proj_Const cs (Proxy IO)
 , Proj_Consts cs (Consts_imported_by IO)
 ) => Proj_ConC cs (Proxy IO) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy IO)
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Maybe
 ( Proj_Const cs (Proxy Maybe)
 , Proj_Consts cs (Consts_imported_by Maybe)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy Maybe) where
	proj_conC _ x (TyConst c)
	 | Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = Just $ case x of
		 TyConst q
		  | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Dict
		  | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Dict
		 _ -> Nothing
	proj_conC _ x (TyConst c :$ a)
	 | Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = Just $ case x of
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Eq)
		  , Just Dict <- proj_con t a -> Just Dict
		 t@(TyConst q)
		  | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		  , Just Dict <- proj_con t a -> Just Dict
		 _ -> Nothing
	proj_conC _ _ _ = Nothing
instance -- Monad
 ( Proj_Const cs (Proxy Monad)
 , Proj_Consts cs (Consts_imported_by Monad)
 ) => Proj_ConC cs (Proxy Monad)
instance -- Monoid
 ( Proj_Const cs (Proxy Monoid)
 , Proj_Consts cs (Consts_imported_by Monoid)
 ) => Proj_ConC cs (Proxy Monoid)
instance -- Num
 ( Proj_Const cs (Proxy Num)
 , Proj_Consts cs (Consts_imported_by Num)
 ) => Proj_ConC cs (Proxy Num)
instance -- Ord
 ( Proj_Const cs (Proxy Ord)
 , Proj_Consts cs (Consts_imported_by Ord)
 ) => Proj_ConC cs (Proxy Ord)
instance -- Real
 ( Proj_Const cs (Proxy Real)
 , Proj_Consts cs (Consts_imported_by Real)
 ) => Proj_ConC cs (Proxy Real)
instance -- Traversable
 ( Proj_Const cs (Proxy Traversable)
 , Proj_Consts cs (Consts_imported_by Traversable)
 ) => Proj_ConC cs (Proxy Traversable)