content: {-# LANGUAGE DataKinds                  #-}
  {-# LANGUAGE DeriveFunctor              #-}
  {-# LANGUAGE DeriveTraversable          #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE OverloadedStrings          #-}
  {-# LANGUAGE PatternSynonyms            #-}
  {-# LANGUAGE PolyKinds                  #-}
  {-# LANGUAGE RankNTypes                 #-}
  {-# LANGUAGE TemplateHaskell            #-}
  
  module Camfort.Helpers.TypeLevel where
  
  import           Data.Functor.Identity
  
  import           Language.Expression.Pretty
  
  --------------------------------------------------------------------------------
  --  Types
  --------------------------------------------------------------------------------
  
  -- | An existential type containing @f a@ for some type @a@.
  data Some f where
    Some :: f a -> Some f
  
  -- | A pair of functorial values over the same ground type, where the first
  -- value is meant to add constraints rather than real semantic information. The
  -- 'Pretty1' instance ignores the first value.
  data PairOf f g a = PairOf (f a) (g a)
    deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
  
  type SomePair f g = Some (PairOf f g)
  
  --------------------------------------------------------------------------------
  --  Patterns
  --------------------------------------------------------------------------------
  
  pattern SomePair :: f a -> g a -> Some (PairOf f g)
  pattern SomePair x y = Some (PairOf x y)
  
  --------------------------------------------------------------------------------
  --  Combinators
  --------------------------------------------------------------------------------
  
  traverseSome
    :: Functor m
    => (forall a. f a -> m (g a))
    -> Some f -> m (Some g)
  traverseSome f (Some x) = Some <$> f x
  
  traversePairOf
    :: Functor m
    => (f a -> g a -> m (f' b, g' b))
    -> PairOf f g a -> m (PairOf f' g' b)
  traversePairOf f (PairOf x y) = uncurry PairOf <$> f x y
  
  mapSome :: (forall a. f a -> g a) -> Some f -> Some g
  mapSome f = runIdentity . traverseSome (Identity . f)
  
  --------------------------------------------------------------------------------
  --  Instances
  --------------------------------------------------------------------------------
  
  instance Pretty1 f => Pretty (Some f) where
    prettysPrec p = \case
      Some x -> prettys1Prec p x
  
  instance Pretty1 g => Pretty1 (PairOf f g) where
    prettys1Prec p = \case
      PairOf _ x -> prettys1Prec p x
  
  instance Pretty1 f => Show (Some f) where
    show = pretty
  