    ------------------------------------------------------------------------
    -- |
    -- Module           : Data.Parameterized.Some
    -- Copyright        : (c) Galois, Inc 2014-2019
    -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
    -- Description : a GADT that hides a type parameter
    --
    -- This module provides 'Some', a GADT that hides a type parameter.
    ------------------------------------------------------------------------
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    module Data.Parameterized.Some
      ( Some(..)
      , viewSome
      , mapSome
      , traverseSome
      , traverseSome_
      , someLens
      ) where

    import Control.Lens (Lens', lens, (&), (^.), (.~))
    import Data.Hashable
    import Data.Kind
    import Data.Parameterized.Classes
    import Data.Parameterized.TraversableF

    data Some (f:: k -> Type) = forall x . Some (f x)

    instance TestEquality f => Eq (Some f) where
      Some f x
    x == :: Some f -> Some f -> Bool
    == Some f x
    y = Maybe (x :~: x) -> Bool
    forall a. Maybe a -> Bool
    isJust (f x -> f x -> Maybe (x :~: x)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality f x
    x f x
    y)

    instance OrdF f => Ord (Some f) where
      compare :: Some f -> Some f -> Ordering
    compare (Some f x
    x) (Some f x
    y) = OrderingF x x -> Ordering
    forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
    toOrdering (f x -> f x -> OrderingF x x
    forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
    forall k (ktp :: k -> *) (x :: k) (y :: k).
    OrdF ktp =>
    ktp x -> ktp y -> OrderingF x y
    compareF f x
    x f x
    y)

    instance (HashableF f, TestEquality f) => Hashable (Some f) where
      hashWithSalt :: Int -> Some f -> Int
    hashWithSalt Int
    s (Some f x
    x) = Int -> f x -> Int
    forall (tp :: k). Int -> f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
    hashWithSaltF Int
    s f x
    x
      hash :: Some f -> Int
    hash (Some f x
    x) = f x -> Int
    forall (tp :: k). f tp -> Int
    forall k (f :: k -> *) (tp :: k). HashableF f => f tp -> Int
    hashF f x
    x

    instance ShowF f => Show (Some f) where
      show :: Some f -> String
    show (Some f x
    x) = f x -> String
    forall (tp :: k). f tp -> String
    forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
    showF f x
    x

    -- | Project out of Some.
    viewSome :: (forall tp . f tp -> r) -> Some f -> r
    viewSome :: forall {k} (f :: k -> *) r.
    (forall (tp :: k). f tp -> r) -> Some f -> r
    viewSome forall (tp :: k). f tp -> r
    f (Some f x
    x) = f x -> r
    forall (tp :: k). f tp -> r
    f f x
    x

    -- | Apply function to inner value.
    mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g
    mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
    (forall (tp :: k). f tp -> g tp) -> Some f -> Some g
    mapSome forall (tp :: k). f tp -> g tp
    f (Some f x
    x) = g x -> Some g
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (g x -> Some g) -> g x -> Some g
    forall a b. (a -> b) -> a -> b
    $! f x -> g x
    forall (tp :: k). f tp -> g tp
    f f x
    x

    {-# INLINE traverseSome #-}
    -- | Modify the inner value.
    traverseSome :: Functor m
                 => (forall tp . f tp -> m (g tp))
                 -> Some f
                 -> m (Some g)
    traverseSome :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
    Functor m =>
    (forall (tp :: k). f tp -> m (g tp)) -> Some f -> m (Some g)
    traverseSome forall (tp :: k). f tp -> m (g tp)
    f (Some f x
    x) = g x -> Some g
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (g x -> Some g) -> m (g x) -> m (Some g)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` f x -> m (g x)
    forall (tp :: k). f tp -> m (g tp)
    f f x
    x

    {-# INLINE traverseSome_ #-}
    -- | Modify the inner value.
    traverseSome_ :: Functor m => (forall tp . f tp -> m ()) -> Some f -> m ()
    traverseSome_ :: forall {k} (m :: * -> *) (f :: k -> *).
    Functor m =>
    (forall (tp :: k). f tp -> m ()) -> Some f -> m ()
    traverseSome_ forall (tp :: k). f tp -> m ()
    f (Some f x
    x) = (\()
    _ -> ()) (() -> ()) -> m () -> m ()
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` f x -> m ()
    forall (tp :: k). f tp -> m ()
    f f x
    x

    instance FunctorF     Some where fmapF :: forall (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x) -> Some f -> Some g
    fmapF     = (forall (tp :: k). f tp -> g tp) -> Some f -> Some g
    forall {k} (f :: k -> *) (g :: k -> *).
    (forall (tp :: k). f tp -> g tp) -> Some f -> Some g
    mapSome
    instance FoldableF    Some where foldMapF :: forall m (e :: k -> *).
    Monoid m =>
    (forall (s :: k). e s -> m) -> Some e -> m
    foldMapF  = (forall (s :: k). e s -> m) -> Some e -> m
    forall {k} (t :: (k -> *) -> *) m (e :: k -> *).
    (TraversableF t, Monoid m) =>
    (forall (s :: k). e s -> m) -> t e -> m
    foldMapFDefault
    instance TraversableF Some where traverseF :: forall (m :: * -> *) (e :: k -> *) (f :: k -> *).
    Applicative m =>
    (forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f)
    traverseF = (forall (tp :: k). e tp -> m (f tp)) -> Some e -> m (Some f)
    forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
    Functor m =>
    (forall (tp :: k). f tp -> m (g tp)) -> Some f -> m (Some g)
    traverseSome

    -- | A lens that is polymorphic in the index may be used on a value with an
    -- existentially-quantified index.
    someLens :: (forall tp. Lens' (f tp) a) -> Lens' (Some f) a
    someLens :: forall {k} (f :: k -> *) a.
    (forall (tp :: k) (f :: * -> *).
     Functor f =>
     (a -> f a) -> f tp -> f (f tp))
    -> Lens' (Some f) a
    someLens forall (tp :: k) (f :: * -> *).
    Functor f =>
    (a -> f a) -> f tp -> f (f tp)
    l = (Some f -> a)
    -> (Some f -> a -> Some f) -> Lens (Some f) (Some f) a a
    forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
    lens (\(Some f x
    x) -> f x
    x f x -> Getting a (f x) a -> a
    forall s a. s -> Getting a s a -> a
    ^. Getting a (f x) a
    forall (tp :: k) (f :: * -> *).
    Functor f =>
    (a -> f a) -> f tp -> f (f tp)
    l) (\(Some f x
    x) a
    v -> f x -> Some f
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (f x
    x f x -> (f x -> f x) -> f x
    forall a b. a -> (a -> b) -> b
    & (a -> Identity a) -> f x -> Identity (f x)
    forall (tp :: k) (f :: * -> *).
    Functor f =>
    (a -> f a) -> f tp -> f (f tp)
    l ((a -> Identity a) -> f x -> Identity (f x)) -> a -> f x -> f x
    forall s t a b. ASetter s t a b -> b -> s -> t
    .~ a
    v))