    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE Safe #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE UndecidableSuperClasses #-}
    module Data.Dependent.Sum where

    import Control.Applicative

    import Data.Constraint.Extras
    import Data.Type.Equality ((:~:) (..))

    import Data.GADT.Show
    import Data.GADT.Compare

    import Data.Maybe (fromMaybe)

    import Text.Read

    -- | A basic dependent sum type where the first component is a tag
    -- that specifies the type of the second. For example, think of a GADT
    -- such as:
    --
    -- > data Tag a where
    -- >    AString :: Tag String
    -- >    AnInt   :: Tag Int
    -- >    Rec     :: Tag (DSum Tag Identity)
    --
    -- Then we can write expressions where the RHS of @(':=>')@ has
    -- different types depending on the @Tag@ constructor used. Here are
    -- some expressions of type @DSum Tag 'Identity'@:
    --
    -- > AString :=> Identity "hello!"
    -- > AnInt   :=> Identity 42
    --
    -- Often, the @f@ we choose has an 'Applicative' instance, and we can
    -- use the helper function @('==>')@. The following expressions all
    -- have the type @Applicative f => DSum Tag f@:
    --
    -- > AString ==> "hello!"
    -- > AnInt   ==> 42
    --
    -- We can write functions that consume @DSum Tag f@ values by
    -- matching, such as:
    --
    -- > toString :: DSum Tag Identity -> String
    -- > toString (AString :=> Identity str) = str
    -- > toString (AnInt   :=> Identity int) = show int
    -- > toString (Rec     :=> Identity sum) = toString sum
    --
    -- The @(':=>')@ constructor and @('==>')@ helper are chosen to
    -- resemble the @(key => value)@ construction for dictionary entries
    -- in many dynamic languages. The @:=>@ and @==>@ operators have very
    -- low precedence and bind to the right, making repeated use of these
    -- operators behave as you'd expect:
    --
    -- > -- Parses as: Rec ==> (AnInt ==> (3 + 4))
    -- > -- Has type: Applicative f => DSum Tag f
    -- > Rec ==> AnInt ==> 3 + 4
    --
    -- The precedence of these operators is just above that of '$', so
    -- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString
    -- ==> "eep")@.
    --
    -- To use the 'Eq', 'Ord', 'Read', and 'Show' instances for @'DSum'
    -- tag f@, you will need an 'ArgDict' instance for your tag type. Use
    -- 'Data.Constraint.Extras.TH.deriveArgDict' from the
    -- @constraints-extras@ package to generate this
    -- instance.
    data DSum tag f = forall a. !(tag a) :=> f a

    infixr 1 :=>, ==>

    -- | Convenience helper. Uses 'pure' to lift @a@ into @f a@.
    (==>) :: Applicative f => tag a -> a -> DSum tag f
    tag a
    k ==> :: forall (f :: * -> *) (tag :: * -> *) a.
    Applicative f =>
    tag a -> a -> DSum tag f
    ==> a
    v = tag a
    k tag a -> f a -> DSum tag f
    forall {k} (tag :: k -> *) (f :: k -> *) (a :: k).
    tag a -> f a -> DSum tag f
    :=> a -> f a
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    v

    instance forall tag f. (GShow tag, Has' Show tag f) => Show (DSum tag f) where
        showsPrec :: Int -> DSum tag f -> ShowS
    showsPrec Int
    p (tag a
    tag :=> f a
    value) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    10)
            ( Int -> tag a -> ShowS
    forall (a :: k). Int -> tag a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    0 tag a
    tag
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :=> "
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k -> *) (f :: k -> *) (a :: k)
           r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Show @f tag a
    tag (Int -> f a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    1 f a
    value)
            )

    instance forall tag f. (GRead tag, Has' Read tag f) => Read (DSum tag f) where
        readsPrec :: Int -> ReadS (DSum tag f)
    readsPrec Int
    p = Bool -> ReadS (DSum tag f) -> ReadS (DSum tag f)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    1) (ReadS (DSum tag f) -> ReadS (DSum tag f))
    -> ReadS (DSum tag f) -> ReadS (DSum tag f)
    forall a b. (a -> b) -> a -> b
    $ \String
    s ->
            [[(DSum tag f, String)]] -> [(DSum tag f, String)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
                [ Some tag
    -> (forall (a :: k). tag a -> [(DSum tag f, String)])
    -> [(DSum tag f, String)]
    forall {k} (tag :: k -> *) b.
    Some tag -> (forall (a :: k). tag a -> b) -> b
    getGReadResult Some tag
    withTag ((forall (a :: k). tag a -> [(DSum tag f, String)])
     -> [(DSum tag f, String)])
    -> (forall (a :: k). tag a -> [(DSum tag f, String)])
    -> [(DSum tag f, String)]
    forall a b. (a -> b) -> a -> b
    $ \tag a
    tag ->
                    [ (tag a
    tag tag a -> f a -> DSum tag f
    forall {k} (tag :: k -> *) (f :: k -> *) (a :: k).
    tag a -> f a -> DSum tag f
    :=> f a
    val, String
    rest'')
                    | (f a
    val, String
    rest'') <- forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k -> *) (f :: k -> *) (a :: k)
           r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Read @f tag a
    tag (Int -> ReadS (f a)
    forall a. Read a => Int -> ReadS a
    readsPrec Int
    1 String
    rest')
                    ]
                | (Some tag
    withTag, String
    rest) <- Int -> GReadS tag
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    p String
    s
                , let (String
    con, String
    rest') = Int -> String -> (String, String)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    5 String
    rest
                , String
    con String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    " :=> "
                ]

    instance forall tag f. (GEq tag, Has' Eq tag f) => Eq (DSum tag f) where
        (tag a
    t1 :=> f a
    x1) == :: DSum tag f -> DSum tag f -> Bool
    == (tag a
    t2 :=> f a
    x2)  = Bool -> Maybe Bool -> Bool
    forall a. a -> Maybe a -> a
    fromMaybe Bool
    False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ do
            Refl <- tag a -> tag a -> Maybe (a :~: a)
    forall (a :: k) (b :: k). tag a -> tag b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq tag a
    t1 tag a
    t2
            return $ has' @Eq @f t1 (x1 == x2)

    instance forall tag f. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) where
        compare :: DSum tag f -> DSum tag f -> Ordering
    compare (tag a
    t1 :=> f a
    x1) (tag a
    t2 :=> f a
    x2)  = case tag a -> tag a -> GOrdering a a
    forall (a :: k) (b :: k). tag a -> tag b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare tag a
    t1 tag a
    t2 of
            GOrdering a a
    GLT -> Ordering
    LT
            GOrdering a a
    GGT -> Ordering
    GT
            GOrdering a a
    GEQ -> forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k -> *) (f :: k -> *) (a :: k)
           r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Eq @f tag a
    t1 ((Eq (f a) => Ordering) -> Ordering)
    -> (Eq (f a) => Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k -> *) (f :: k -> *) (a :: k)
           r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Ord @f tag a
    t1 (f a
    x1 f a -> f a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` f a
    f a
    x2)

    {-# DEPRECATED ShowTag "Instead of 'ShowTag tag f', use '(GShow tag, Has' Show tag f)'" #-}
    type ShowTag tag f = (GShow tag, Has' Show tag f)

    showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS
    showTaggedPrec :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    (GShow tag, Has' Show tag f) =>
    tag a -> Int -> f a -> ShowS
    showTaggedPrec tag a
    tag = forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Show @f tag a
    tag Show (f a) => Int -> f a -> ShowS
    Int -> f a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec

    {-# DEPRECATED ReadTag "Instead of 'ReadTag tag f', use '(GRead tag, Has' Read tag f)'" #-}
    type ReadTag tag f = (GRead tag, Has' Read tag f)

    readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)
    readTaggedPrec :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    (GRead tag, Has' Read tag f) =>
    tag a -> Int -> ReadS (f a)
    readTaggedPrec tag a
    tag = forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Read @f tag a
    tag Read (f a) => Int -> ReadS (f a)
    Int -> ReadS (f a)
    forall a. Read a => Int -> ReadS a
    readsPrec

    {-# DEPRECATED EqTag "Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag f)'" #-}
    type EqTag tag f = (GEq tag, Has' Eq tag f)

    eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool
    eqTaggedPrec :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    (GEq tag, Has' Eq tag f) =>
    tag a -> tag a -> f a -> f a -> Bool
    eqTaggedPrec tag a
    tag1 tag a
    tag2 f a
    f1 f a
    f2 = case tag a
    tag1 tag a -> tag a -> Maybe (a :~: a)
    forall (a :: k') (b :: k'). tag a -> tag b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    `geq` tag a
    tag2 of
      Maybe (a :~: a)
    Nothing -> Bool
    False
      Just a :~: a
    Refl -> forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Eq @f tag a
    tag1 ((Eq (f a) => Bool) -> Bool) -> (Eq (f a) => Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ f a
    f1 f a -> f a -> Bool
    forall a. Eq a => a -> a -> Bool
    == f a
    f2

    eqTagged :: forall tag f a. EqTag tag f => tag a -> tag a -> f a -> f a -> Bool
    eqTagged :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    EqTag tag f =>
    tag a -> tag a -> f a -> f a -> Bool
    eqTagged tag a
    k tag a
    _ f a
    x0 f a
    x1 = forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Eq @f tag a
    k (f a
    x0 f a -> f a -> Bool
    forall a. Eq a => a -> a -> Bool
    == f a
    x1)

    {-# DEPRECATED OrdTag "Instead of 'OrdTag tag f', use '(GCompare tag, Has' Eq tag f, Has' Ord tag f)'" #-}
    type OrdTag tag f = (GCompare tag, Has' Eq tag f, Has' Ord tag f)

    compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering
    compareTaggedPrec :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    (GCompare tag, Has' Eq tag f, Has' Ord tag f) =>
    tag a -> tag a -> f a -> f a -> Ordering
    compareTaggedPrec tag a
    tag1 tag a
    tag2 f a
    f1 f a
    f2 = case tag a
    tag1 tag a -> tag a -> GOrdering a a
    forall (a :: k') (b :: k'). tag a -> tag b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    `gcompare` tag a
    tag2 of
      GOrdering a a
    GLT -> Ordering
    LT
      GOrdering a a
    GEQ -> forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Eq @f tag a
    tag1 ((Eq (f a) => Ordering) -> Ordering)
    -> (Eq (f a) => Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Ord @f tag a
    tag1 ((Ord (f a) => Ordering) -> Ordering)
    -> (Ord (f a) => Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ f a
    f1 f a -> f a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` f a
    f2
      GOrdering a a
    GGT -> Ordering
    GT

    compareTagged :: forall tag f a. OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering
    compareTagged :: forall {k'} (tag :: k' -> *) (f :: k' -> *) (a :: k').
    OrdTag tag f =>
    tag a -> tag a -> f a -> f a -> Ordering
    compareTagged tag a
    k tag a
    _ f a
    x0 f a
    x1 = forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Eq @f tag a
    k ((Eq (f a) => Ordering) -> Ordering)
    -> (Eq (f a) => Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ forall {k} {k'} (c :: k -> Constraint) (g :: k' -> k)
           (f :: k' -> *) (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    forall (c :: * -> Constraint) (g :: k' -> *) (f :: k' -> *)
           (a :: k') r.
    Has' c f g =>
    f a -> (c (g a) => r) -> r
    has' @Ord @f tag a
    k (f a -> f a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare f a
    x0 f a
    x1)