{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
module Language.Symantic.Typing.Constraint where

import Control.Applicative ((<|>))
import Data.Proxy

import Language.Symantic.Parsing
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Constant

-- * Type 'TyCon'
-- | Captures the proof of a 'Constraint'
-- (and its dictionaries when it contains type classes):
-- pattern matching on the 'Dict' constructor
-- brings the 'Constraint' into scope.
data TyCon c where
	Dict :: c => TyCon c

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

-- | Project the 'Constraint' indexed by the given 'Type'
-- onto its proof, captured by 'TyCon' when it holds.
proj_TyCon
 :: forall src ctx ss cs q.
    Source src
 => Proj_TyCon cs
 => Type src ctx ss cs q
 -> Maybe (TyCon q)
proj_TyCon = proj_TyConR (Proxy @cs)

-- ** Class 'Proj_TyConR'
-- | Intermediate type class to construct an instance of 'Proj_TyCon'
-- from many instances of 'Proj_TyConC', one for each item of @cs@.
--
-- * @cs@: starting  list of /type constants/.
-- * @rs@: remaining list of /type constants/.
class Proj_TyConR cs rs where
	proj_TyConR :: Source src => Proxy rs -> Type src ctx ss cs q -> Maybe (TyCon q)
	proj_TyConR _rs _q = Nothing

-- | Test whether @c@ handles the work of 'Proj_TyCon' or not,
-- or recurse on @rs@, preserving the starting list of /type constants/.
instance
 ( Proj_TyConC cs c
 , Proj_TyConR cs rs
 ) => Proj_TyConR cs (Proxy c ': rs) where
	proj_TyConR _rs q =
		proj_TyConC (Proxy @c)  q <|>
		proj_TyConR (Proxy @rs) q
-- | End the recursion.
instance Proj_TyConR cs '[]

-- ** Class 'Proj_TyConC'
-- | Handle the work of 'Proj_TyCon' for a given /type constant/ @c@,
-- that is: maybe it handles the given 'Constraint',
-- and if so, maybe the 'Constraint' holds.
class Proj_TyConC cs c where
	proj_TyConC :: Source src => Proxy c -> Type src ctx ss cs q -> Maybe (TyCon q)
	proj_TyConC _c _q = Nothing

-- * Class @(#)@
-- | 'Constraint' union.
class (x, y) => x # y

(#) :: Source src
    => Inj_TyConst cs (#)
    => Type src ctx ss cs qx
    -> Type src ctx ss cs qy
    -> Type src ctx ss cs (qx # qy)
(#) a b = (ty @(#) `tyApp` a) `tyApp` b
infixr 2 #

instance Fixity_TyConstC (#) where
	fixity_TyConstC _ = FixityInfix $ infixB L 0

tyQual
 :: Source src
 => Proj_TyCon cs
 => Inj_TyConst cs (#>)
 => Type src ctx ss cs q
 -> Type src ctx ss cs h
 -> (TyCon q -> Type src ctx ss cs h -> Type src ctx ss cs h)
 -> Type src ctx ss cs (q #> h)
tyQual q h f =
	TyApp sourceLess (TyApp sourceLess (ty @(#>)) q) $
	case proj_TyCon q of
	 Just Dict -> f Dict h
	 Nothing   -> h
infix 1 `tyQual`