content: {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE DataKinds      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE GADTs                 #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PolyKinds             #-}
  {-# LANGUAGE TypeOperators         #-}
  
  -- | Co-records are sum types over an extensible set of options.
  module Serv.Wai.Corec where
  
  -- | A @'Corec' f rs@ is a value @f (r, s)@ for exactly one choice of @r@
  -- and @s@ such that @(r, s)@ is an element of @rs@.
  data Corec (f :: (k1, k2) -> *) (rs :: [(k1, k2)]) where
    Skip :: Corec f rs -> Corec f ( '(r, s) ': rs )
    Stop :: f '(r, s) -> Corec f ( '(r, s) ': rs )
  
  -- | The judgement @'ElemOf' rs (r, s)@ is satisified when there's an
  -- equality between @(r, s)@ and some element of @rs@. More than this,
  -- however, we assume that the first match of @r@ in @rs@ will work and
  -- then defer matching the @s@ component until later. This helps inference
  -- so long as the assumption that @r@ is "index-like" holds
  class ElemOf rs x where
    -- | Given a valid variant of a 'Corec' "forget" its identity into the
    -- larger 'Corec'.
    inject :: f x -> Corec f rs
  
  instance {-# OVERLAPS #-} (s' ~ s) => ElemOf ( '(r, s) ': rs ) '(r, s') where
    inject = Stop
  
  instance ElemOf rs '(r, s) => ElemOf ( '(r', s') ': rs) '(r, s) where
    inject = Skip . inject
  