{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}

module Web.Routes.Nested.Internal where

import Network.Wai
import Data.Constraint

-- Supported Type-level symbols representing different HTTP verbs / methods.
data HTTPMethod = GET
                | PUT
                | POST
                | DELETE

-- @Bottom@ in the category of the Haskell constraint system
type family Deducible (b :: Bool) :: Constraint where
  Deducible True = ()

-- @not . elem@ at the type level
type family NotElem (x :: k) (xs :: [k]) :: Constraint where
  NotElem x '[] = ()
  NotElem x (x ': xs) = Deducible False
  NotElem x (y ': xs) = NotElem x xs

-- /Exclusive/ HTTP-method list - exclusive / unique list of HTTP methods
data ExMethods a where
  ExMNil :: ExMethods '[]
  GETCons :: NotElem 'GET a =>
             ExResponses xs
          -> ExMethods a
          -> ExMethods ('GET ': a)
  PUTCons :: NotElem 'PUT a =>
             ExResponses xs
          -> ExMethods a
          -> ExMethods ('PUT ': a)
  POSTCons :: NotElem 'POST a =>
              ExResponses xs
           -> ExMethods a
           -> ExMethods ('POST ': a)
  DELETECons :: NotElem 'DELETE a =>
                ExResponses xs
             -> ExMethods a
             -> ExMethods ('DELETE ': a)

data ContentType = HTML
                 | JSON
                 | TEXT

data ExResponses a where
  ExRNil :: ExResponses '[]
  HTMLCons :: NotElem 'HTML a =>
              Response
           -> ExResponses a
           -> ExResponses ('HTML ': a)
  JSONCons :: NotElem 'JSON a =>
              Response
           -> ExResponses a
           -> ExResponses ('JSON ': a)
  TEXTCons :: NotElem 'TEXT a =>
              Response
           -> ExResponses a
           -> ExResponses ('TEXT ': a)