content: {-# OPTIONS_HADDOCK not-home #-}
  
  {-# LANGUAGE DataKinds            #-}
  {-# LANGUAGE GADTs                #-}
  {-# LANGUAGE TypeFamilies         #-}
  {-# LANGUAGE TypeOperators        #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  {-|
  Module      : OneOf.Types
  Description : The 'OneOf' type and its instances.
  Copyright   : (c) Tom Harding, 2018
  License     : MIT
  Maintainer  : tom.harding@habito.com
  Stability   : experimental
  
  'OneOf' is @Eq@, @Ord@, @Show@, and @Semigroup@. In all cases, we require all
  elements within the 'OneOf' to have these intsances, as we effectively just
  delegate to them.
  
  >>> Here "hello" :: OneOf '[String, Bool, [()]]
  Here "hello"
  
  >>> There (Here True) :: OneOf '[String, Bool, [()]]
  There (Here True)
  
  >>> There (There (Here [])) :: OneOf '[String, Bool, [()]]
  There (There (Here []))
  -}
  module OneOf.Types where
  
  import Data.Kind (Type)
  import Utils     (Every)
  
  -- | The 'OneOf' type is effectively a generalised @Either@, in the sense that
  -- @Either a b@ is isomorphic to @OneOf '[a, b]@. 'OneOf', however, will hold
  -- one of any number of greater-than-zero possible types.
  data OneOf (xs :: [Type]) where
    Here  :: x -> OneOf (x ': xs)
    There :: OneOf xs -> OneOf (y ': xs)
  
  instance Every xs Show => Show (OneOf xs) where
  
    -- | We can @Show@ a @OneOf xs@ as long as @Every@ member of @xs@ can @Show@.
    -- What @Every@ does is bring evidence for this into scope for all the types.
  
    show (Here  x) = "Here "   <> show x
    show (There x) = "There (" <> show x <> ")"
  
  instance Every xs Eq => Eq (OneOf xs) where
  
    -- | We can @Eq@ a @OneOf xs@ in the same way as we can @Show@: if all things
    -- are @Eq@, then the 'OneOf' is @Eq@.
  
    Here  x == Here  y = x == y
    There x == There y = x == y
    _       == _       = False
  
  instance (Every xs Eq, Every xs Ord) => Ord (OneOf xs) where
  
    -- | We can have @Ord@ if all of our 'OneOf' members are @Ord@. Interesting
    -- quirk of GHC here: we can't magically get @Every xs Eq@ given @Every xs
    -- Ord@ here (maybe this is that entailment thing Kmett talks about?)
    -- because, while @Ord@ might imply @Eq@, @Every xs Ord@ is a very different
    -- constraint.
  
    Here  _ <= There _ = True
    There _ <= Here  _ = False
  
    Here  x <= Here  y = x <= y
    There x <= There y = x <= y
  
  instance Every xs Semigroup => Semigroup (OneOf xs) where
  
    -- | The @Semigroup@ instance is slightly different to that of @Either@: if
    -- we were using @OneOf '[a, b]@ as an analogue to @Either a b@, the
    -- difference in behaviour is that we're requiring @Semigroup@ of the @a@,
    -- and will @mappend@ two @a@ values if we're given them. In the case of
    -- differing values, we'll prefer the one latest in the list.
  
    Here  x <> Here  y = Here  (x <> y)
    There x <> Here  _ = There  x
    Here  _ <> There y = There       y
    There x <> There y = There (x <> y)
  