{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
module Language.Symantic.Typing.Constraint where

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

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

-- * Type 'Con'
-- | Captures the proof of a 'Constraint'
-- (and its dictionary for a type class):
-- pattern matching on the 'Con' constructor
-- brings the 'Constraint' into scope.
data Con c where
	Con :: c => Con 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 Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Monoid
 , Proxy Ord
 ]

type instance Consts_imported_by Bounded = '[]
type instance Consts_imported_by Enum = '[]
type instance Consts_imported_by Real = '[]
type instance Consts_imported_by String = '[]

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

-- | Project the 'Constraint' indexed by the given 'Type'
-- onto its proof, captured by 'Con' when it holds.
proj_con
 :: forall cs q. Proj_Con cs
 => Type cs (q::Constraint)
 -> Maybe (Con q)
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 item 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 (q::Constraint) -> Maybe (Con q)
	proj_conR _rs _q = 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 _rs q =
		proj_conR (Proxy::Proxy rs) q `fromMaybe`
		proj_conC (Proxy::Proxy c)  q
-- | End the recursion.
instance Proj_ConR cs '[]

-- ** Class 'Proj_ConC'
-- | Handle the work of 'Proj_Con' for a given /type constant/ @c@,
-- that is: maybe it handles the given 'Constraint',
-- and if so, maybe the 'Constraint' holds.
class Proj_ConC cs c where
	proj_conC :: Proxy c -> Type cs (q::Constraint) -> Maybe (Maybe (Con q))
	proj_conC _c _q = Nothing

instance -- Bounded
 Proj_ConC cs (Proxy Bounded)
instance -- Enum
 Proj_ConC cs (Proxy Enum)
instance -- Real
 Proj_ConC cs (Proxy Real)
instance -- ()
 ( Proj_Const cs ()
 , Proj_Consts cs (Consts_imported_by ())
 ) => Proj_ConC cs (Proxy ()) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy ())
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)  -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Enum)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Eq)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid)   -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)      -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- String
 Proj_ConC cs (Proxy String)