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

import Data.Proxy
import GHC.Prim (Constraint)

import Language.Symantic.Type.Root
import Language.Symantic.Type.Alt
import Language.Symantic.Type.Error
import Language.Symantic.Type.Type0

-- * 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

-- * Class 'Type0_Constraint'
-- | Test if a type satisfies a given 'Constraint',
-- returning an Haskell type-level proof
-- of that satisfaction when it holds.
class Type0_Constraint (c:: * -> Constraint) (ty:: * -> *) where
	type0_constraint :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
	type0_constraint _c _ = Nothing
instance -- Type_Root
 Type0_Constraint c (ty (Type_Root ty)) =>
 Type0_Constraint c (Type_Root ty) where
	type0_constraint c (Type_Root ty) = type0_constraint c ty
instance -- Type_Alt
 ( Type0_Constraint c (curr root)
 , Type0_Constraint c (next root)
 ) => Type0_Constraint c (Type_Alt curr next root) where
	type0_constraint c (Type_Alt_Curr ty) = type0_constraint c ty
	type0_constraint c (Type_Alt_Next ty) = type0_constraint c ty

-- | Parsing utility to check that a type is an instance of a given 'Constraint',
-- or raise 'Error_Type_Constraint_missing'.
check_type_type0_constraint
 :: forall ast c root ty h ret.
 ( root ~ Root_of_Type ty
 , Error_Type_Lift (Error_Type ast) (Error_of_Type ast root)
 , Type0_Constraint c ty
 ) => Proxy c -> ast -> ty h
 -> (Dict (c h) -> Either (Error_of_Type ast root) ret)
 -> Either (Error_of_Type ast root) ret
check_type_type0_constraint c ast ty k =
	case type0_constraint c ty of
	 Just Dict -> k Dict
	 Nothing -> Left $ error_type_lift $
		Error_Type_Constraint_missing ast -- (Exists_Type0 ty_k)

-- * Class 'Type1_Constraint'
-- | Test if a type constructor satisfies a given 'Constraint',
-- returning an Haskell type-level proof
-- of that satisfaction when it holds.
class Type1_Constraint (c:: (* -> *) -> Constraint) (ty:: * -> *) where
	type1_constraint :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
	type1_constraint _c _ = Nothing
instance -- Type_Root
 Type1_Constraint c (ty (Type_Root ty)) =>
 Type1_Constraint c (Type_Root ty) where
	type1_constraint c (Type_Root ty) = type1_constraint c ty
instance -- Type_Alt
 ( Type1_Constraint c (curr root)
 , Type1_Constraint c (next root)
 ) => Type1_Constraint c (Type_Alt curr next root) where
	type1_constraint c (Type_Alt_Curr ty) = type1_constraint c ty
	type1_constraint c (Type_Alt_Next ty) = type1_constraint c ty
instance Type1_Constraint c (Type0 px root)