{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}


module Exinst.Internal
 ( -- * 1 type index
   Some1(Some1)
 , some1
 , fromSome1
 , _Some1
 , withSome1
 , withSome1Sing
 , some1SingRep
 , same1
 , Dict1(dict1)

   -- * 2 type indexes
 , Some2(Some2)
 , some2
 , fromSome2
 , _Some2
 , withSome2
 , withSome2Sing
 , some2SingRep
 , same2
 , Dict2(dict2)

   -- * 3 type indexes
 , Some3(Some3)
 , some3
 , fromSome3
 , _Some3
 , withSome3
 , withSome3Sing
 , some3SingRep
 , same3
 , Dict3(dict3)

   -- * 4 type indexes
 , Some4(Some4)
 , some4
 , fromSome4
 , _Some4
 , withSome4
 , withSome4Sing
 , some4SingRep
 , same4
 , Dict4(dict4)

   -- * Miscellaneous
 , Dict0(dict0)
 ) where

import Data.Constraint
import Data.Kind (Type)
import Data.Profunctor (dimap, Choice(right'))
import Data.Singletons
import Data.Singletons.Decide
import Prelude

--------------------------------------------------------------------------------

data Some1 (f1 :: k1 -> Type) = forall a1.
  Some1 !(Sing a1) !(f1 a1)

data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.
  Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)

data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.
  Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)

data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.
  Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)

--------------------------------------------------------------------------------

some1
  :: forall k1 (f1 :: k1 -> Type) a1
  .  SingI a1
  => f1 a1
  -> Some1 f1 -- ^
some1 :: forall k1 (f1 :: k1 -> *) (a1 :: k1). SingI a1 => f1 a1 -> Some1 f1
some1 = forall k1 (f1 :: k1 -> *) (a1 :: k1). Sing a1 -> f1 a1 -> Some1 f1
Some1 (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
{-# INLINE some1 #-}

some2
  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
  .  (SingI a2, SingI a1)
  => f2 a2 a1
  -> Some2 f2 -- ^
some2 :: forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
(SingI a2, SingI a1) =>
f2 a2 a1 -> Some2 f2
some2 = forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
Sing a2 -> Sing a1 -> f2 a2 a1 -> Some2 f2
Some2 (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2) (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
{-# INLINE some2 #-}

some3
  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
  .  (SingI a3, SingI a2, SingI a1)
  => f3 a3 a2 a1
  -> Some3 f3 -- ^
some3 :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f3 a3 a2 a1 -> Some3 f3
some3 = forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> Some3 f3
Some3 (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a3) (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2) (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
{-# INLINE some3 #-}

some4
  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
  .  (SingI a4, SingI a3, SingI a2, SingI a1)
  => f4 a4 a3 a2 a1
  -> Some4 f4 -- ^
some4 :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f4 a4 a3 a2 a1 -> Some4 f4
some4 = forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> Some4 f4
Some4 (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a4) (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a3)
              (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2) (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
{-# INLINE some4 #-}

--------------------------------------------------------------------------------

withSome1
  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
   . Some1 f1
  -> (forall a1. SingI a1 => f1 a1 -> r)
  -> r -- ^
withSome1 :: forall k1 (f1 :: k1 -> *) r.
Some1 f1 -> (forall (a1 :: k1). SingI a1 => f1 a1 -> r) -> r
withSome1 Some1 f1
s1 forall (a1 :: k1). SingI a1 => f1 a1 -> r
g = forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f1
s1 (\Sing a1
_ -> forall (a1 :: k1). SingI a1 => f1 a1 -> r
g)
{-# INLINABLE withSome1 #-}

withSome2
  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
  .  Some2 f2
  -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
  -> r -- ^
withSome2 :: forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
    (SingI a2, SingI a1) =>
    f2 a2 a1 -> r)
-> r
withSome2 Some2 f2
s2 forall (a2 :: k2) (a1 :: k1). (SingI a2, SingI a1) => f2 a2 a1 -> r
g = forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
    (SingI a2, SingI a1) =>
    Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing Some2 f2
s2 (\Sing a2
_ Sing a1
_ -> forall (a2 :: k2) (a1 :: k1). (SingI a2, SingI a1) => f2 a2 a1 -> r
g)
{-# INLINABLE withSome2 #-}

withSome3
  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
  .  Some3 f3
  -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
  -> r -- ^
withSome3 :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a3, SingI a2, SingI a1) =>
    f3 a3 a2 a1 -> r)
-> r
withSome3 Some3 f3
s3 forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f3 a3 a2 a1 -> r
g = forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a3, SingI a2, SingI a1) =>
    Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing Some3 f3
s3 (\Sing a3
_ Sing a2
_ Sing a1
_ -> forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f3 a3 a2 a1 -> r
g)
{-# INLINABLE withSome3 #-}

withSome4
  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
  .  Some4 f4
  -> (forall a4 a3 a2 a1
        .  (SingI a4, SingI a3, SingI a2, SingI a1)
        => f4 a4 a3 a2 a1 -> r)
  -> r -- ^
withSome4 :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a4, SingI a3, SingI a2, SingI a1) =>
    f4 a4 a3 a2 a1 -> r)
-> r
withSome4 Some4 f4
s4 forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f4 a4 a3 a2 a1 -> r
g = forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a4, SingI a3, SingI a2, SingI a1) =>
    Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing Some4 f4
s4 (\Sing a4
_ Sing a3
_ Sing a2
_ Sing a1
_ -> forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f4 a4 a3 a2 a1 -> r
g)
{-# INLINABLE withSome4 #-}

--------------------------------------------------------------------------------

-- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.
withSome1Sing
  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
   . Some1 f1
  -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
  -> r -- ^
withSome1Sing :: forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing (Some1 Sing a1
sa1 f1 a1
x) forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r
g = forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a1
sa1 (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r
g Sing a1
sa1 f1 a1
x)
{-# INLINABLE withSome1Sing #-}

-- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.
withSome2Sing
  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
  .  Some2 f2
  -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
  -> r -- ^
withSome2Sing :: forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
    (SingI a2, SingI a1) =>
    Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing (Some2 Sing a2
sa2 Sing a1
sa1 f2 a2 a1
x) forall (a2 :: k2) (a1 :: k1).
(SingI a2, SingI a1) =>
Sing a2 -> Sing a1 -> f2 a2 a1 -> r
g = forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a2
sa2 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a1
sa1 (forall (a2 :: k2) (a1 :: k1).
(SingI a2, SingI a1) =>
Sing a2 -> Sing a1 -> f2 a2 a1 -> r
g Sing a2
sa2 Sing a1
sa1 f2 a2 a1
x))
{-# INLINABLE withSome2Sing #-}

-- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.
withSome3Sing
  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
  .  Some3 f3
  -> (forall a3 a2 a1
         .  (SingI a3, SingI a2, SingI a1)
         => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
  -> r -- ^
withSome3Sing :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a3, SingI a2, SingI a1) =>
    Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing (Some3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f3 a3 a2 a1
x) forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r
g =
  forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a3
sa3 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a2
sa2 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a1
sa1 (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r
g Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f3 a3 a2 a1
x)))
{-# INLINABLE withSome3Sing #-}

-- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.
withSome4Sing
  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
  .  Some4 f4
  -> (forall a4 a3 a2 a1
        .  (SingI a4, SingI a3, SingI a2, SingI a1)
        => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
  -> r -- ^
withSome4Sing :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a4, SingI a3, SingI a2, SingI a1) =>
    Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing (Some4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f4 a4 a3 a2 a1
x) forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r
g =
  forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a4
sa4 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a3
sa3 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a2
sa2 (forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a1
sa1
     (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r
g Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f4 a4 a3 a2 a1
x))))
{-# INLINABLE withSome4Sing #-}

--------------------------------------------------------------------------------

fromSome1
   :: forall k1 (f1 :: k1 -> Type) a1
    . (SingI a1, SDecide k1)
   => Some1 f1
   -> Maybe (f1 a1) -- ^
fromSome1 :: forall k1 (f1 :: k1 -> *) (a1 :: k1).
(SingI a1, SDecide k1) =>
Some1 f1 -> Maybe (f1 a1)
fromSome1 = \(Some1 Sing a1
sa1' f1 a1
x) -> do
   a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
   forall (m :: * -> *) a. Monad m => a -> m a
return f1 a1
x
{-# INLINABLE fromSome1 #-}

fromSome2
   :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
    . ( SingI a2, SDecide k2
      , SingI a1, SDecide k1 )
   => Some2 f2
   -> Maybe (f2 a2 a1) -- ^
fromSome2 :: forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
(SingI a2, SDecide k2, SingI a1, SDecide k1) =>
Some2 f2 -> Maybe (f2 a2 a1)
fromSome2 = \(Some2 Sing a2
sa2' Sing a1
sa1' f2 a2 a1
x) -> do
   a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2)
   a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
   forall (m :: * -> *) a. Monad m => a -> m a
return f2 a2 a1
x
{-# INLINABLE fromSome2 #-}

fromSome3
   :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
    . ( SingI a3, SDecide k3
      , SingI a2, SDecide k2
      , SingI a1, SDecide k1 )
   => Some3 f3
   -> Maybe (f3 a3 a2 a1) -- ^
fromSome3 :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
(SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1,
 SDecide k1) =>
Some3 f3 -> Maybe (f3 a3 a2 a1)
fromSome3 = \(Some3 Sing a3
sa3' Sing a2
sa2' Sing a1
sa1' f3 a3 a2 a1
x) -> do
   a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a3)
   a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2)
   a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
   forall (m :: * -> *) a. Monad m => a -> m a
return f3 a3 a2 a1
x
{-# INLINABLE fromSome3 #-}

fromSome4
   :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
    . ( SingI a4, SDecide k4
      , SingI a3, SDecide k3
      , SingI a2, SDecide k2
      , SingI a1, SDecide k1 )
   => Some4 f4
   -> Maybe (f4 a4 a3 a2 a1) -- ^
fromSome4 :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2,
 SingI a1, SDecide k1) =>
Some4 f4 -> Maybe (f4 a4 a3 a2 a1)
fromSome4 = \(Some4 Sing a4
sa4' Sing a3
sa3' Sing a2
sa2' Sing a1
sa1' f4 a4 a3 a2 a1
x) -> do
   a4 :~: a4
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a4
sa4' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a4)
   a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a3)
   a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a2)
   a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1' (forall {k} (a :: k). SingI a => Sing a
sing :: Sing a1)
   forall (m :: * -> *) a. Monad m => a -> m a
return f4 a4 a3 a2 a1
x
{-# INLINABLE fromSome4 #-}

--------------------------------------------------------------------------------

-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.
_Some1
  :: forall k1 (f1 :: k1 -> Type) a1
  .  (SingI a1, SDecide k1)
  => Prism' (Some1 f1) (f1 a1)
_Some1 :: forall k1 (f1 :: k1 -> *) (a1 :: k1).
(SingI a1, SDecide k1) =>
Prism' (Some1 f1) (f1 a1)
_Some1 = forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' forall k1 (f1 :: k1 -> *) (a1 :: k1). SingI a1 => f1 a1 -> Some1 f1
some1 forall k1 (f1 :: k1 -> *) (a1 :: k1).
(SingI a1, SDecide k1) =>
Some1 f1 -> Maybe (f1 a1)
fromSome1
{-# INLINE _Some1 #-}

-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.
_Some2
  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
  .  ( SingI a2, SDecide k2
     , SingI a1, SDecide k1 )
  => Prism' (Some2 f2) (f2 a2 a1)
_Some2 :: forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
(SingI a2, SDecide k2, SingI a1, SDecide k1) =>
Prism' (Some2 f2) (f2 a2 a1)
_Some2 = forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
(SingI a2, SingI a1) =>
f2 a2 a1 -> Some2 f2
some2 forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
(SingI a2, SDecide k2, SingI a1, SDecide k1) =>
Some2 f2 -> Maybe (f2 a2 a1)
fromSome2
{-# INLINE _Some2 #-}

-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.
_Some3
  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
  .  ( SingI a3, SDecide k3
     , SingI a2, SDecide k2
     , SingI a1, SDecide k1 )
  => Prism' (Some3 f3) (f3 a3 a2 a1)
_Some3 :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
(SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1,
 SDecide k1) =>
Prism' (Some3 f3) (f3 a3 a2 a1)
_Some3 = forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f3 a3 a2 a1 -> Some3 f3
some3 forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
(SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1,
 SDecide k1) =>
Some3 f3 -> Maybe (f3 a3 a2 a1)
fromSome3
{-# INLINE _Some3 #-}

-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.
_Some4
  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
  .  ( SingI a4, SDecide k4
     , SingI a3, SDecide k3
     , SingI a2, SDecide k2
     , SingI a1, SDecide k1 )
  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)
_Some4 :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2,
 SingI a1, SDecide k1) =>
Prism' (Some4 f4) (f4 a4 a3 a2 a1)
_Some4 = forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f4 a4 a3 a2 a1 -> Some4 f4
some4 forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
       (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2,
 SingI a1, SDecide k1) =>
Some4 f4 -> Maybe (f4 a4 a3 a2 a1)
fromSome4
{-# INLINE _Some4 #-}

--------------------------------------------------------------------------------

some1SingRep
  :: SingKind k1
  => Some1 (f1 :: k1 -> Type)
  -> Demote k1 -- ^
some1SingRep :: forall k1 (f1 :: k1 -> *). SingKind k1 => Some1 f1 -> Demote k1
some1SingRep = \(Some1 Sing a1
sa1 f1 a1
_) -> forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1
{-# INLINE some1SingRep #-}

some2SingRep
  :: (SingKind k2, SingKind k1)
  => Some2 (f2 :: k2 -> k1 -> Type)
  -> (Demote k2, Demote k1) -- ^
some2SingRep :: forall k2 k1 (f2 :: k2 -> k1 -> *).
(SingKind k2, SingKind k1) =>
Some2 f2 -> (Demote k2, Demote k1)
some2SingRep = \(Some2 Sing a2
sa2 Sing a1
sa1 f2 a2 a1
_) -> (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1)
{-# INLINE some2SingRep #-}

some3SingRep
  :: (SingKind k3, SingKind k2, SingKind k1)
  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)
  -> (Demote k3, Demote k2, Demote k1) -- ^
some3SingRep :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *).
(SingKind k3, SingKind k2, SingKind k1) =>
Some3 f3 -> (Demote k3, Demote k2, Demote k1)
some3SingRep = \(Some3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f3 a3 a2 a1
_) ->
  (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1)
{-# INLINE some3SingRep #-}

some4SingRep
  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)
  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
  -> (Demote k4, Demote k3, Demote k2, Demote k1) -- ^
some4SingRep :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *).
(SingKind k4, SingKind k3, SingKind k2, SingKind k1) =>
Some4 f4 -> (Demote k4, Demote k3, Demote k2, Demote k1)
some4SingRep = \(Some4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f4 a4 a3 a2 a1
_) ->
  (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a4
sa4, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1)
{-# INLINE some4SingRep #-}

--------------------------------------------------------------------------------

-- | @'same1' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
-- indexes are equal.
--
-- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@
{-# INLINABLE same1 #-}
same1
  :: forall k1 f g x
  .  SDecide k1
  => (forall a1. SingI a1 => f a1 -> g a1 -> x)
  -> Some1 (f :: k1 -> Type)
  -> Some1 (g :: k1 -> Type)
  -> Maybe x  -- ^
same1 :: forall k1 (f :: k1 -> *) (g :: k1 -> *) x.
SDecide k1 =>
(forall (a1 :: k1). SingI a1 => f a1 -> g a1 -> x)
-> Some1 f -> Some1 g -> Maybe x
same1 forall (a1 :: k1). SingI a1 => f a1 -> g a1 -> x
z = \Some1 f
s1f Some1 g
s1g ->
  forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
s1f forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1 f a1
f ->
    forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 g
s1g forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1' g a1
g -> do
       a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1 Sing a1
sa1'
       forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (a1 :: k1). SingI a1 => f a1 -> g a1 -> x
z f a1
f g a1
g)

-- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
-- indexes are equal.
--
-- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@
{-# INLINABLE same2 #-}
same2
  :: forall k2 k1 f g x
  .  (SDecide k2, SDecide k1)
  => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x)
  -> Some2 (f :: k2 -> k1 -> Type)
  -> Some2 (g :: k2 -> k1 -> Type)
  -> Maybe x  -- ^
same2 :: forall k2 k1 (f :: k2 -> k1 -> *) (g :: k2 -> k1 -> *) x.
(SDecide k2, SDecide k1) =>
(forall (a2 :: k2) (a1 :: k1). SingI a1 => f a2 a1 -> g a2 a1 -> x)
-> Some2 f -> Some2 g -> Maybe x
same2 forall (a2 :: k2) (a1 :: k1). SingI a1 => f a2 a1 -> g a2 a1 -> x
z = \Some2 f
s2l Some2 g
s2g ->
  forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
    (SingI a2, SingI a1) =>
    Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing Some2 f
s2l forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2 Sing a1
sa1 f a2 a1
f ->
    forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
    (SingI a2, SingI a1) =>
    Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing Some2 g
s2g forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2' Sing a1
sa1' g a2 a1
g -> do
       a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2 Sing a2
sa2'
       a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1 Sing a1
sa1'
       forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (a2 :: k2) (a1 :: k1). SingI a1 => f a2 a1 -> g a2 a1 -> x
z f a2 a1
f g a2 a1
g)

-- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
-- indexes are equal.
--
-- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@
{-# INLINABLE same3 #-}
same3
  :: forall k3 k2 k1 f g x
  .  (SDecide k3, SDecide k2, SDecide k1)
  => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1)
        => f a3 a2 a1 -> g a3 a2 a1 -> x)
  -> Some3 (f :: k3 -> k2 -> k1 -> Type)
  -> Some3 (g :: k3 -> k2 -> k1 -> Type)
  -> Maybe x  -- ^
same3 :: forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> *)
       (g :: k3 -> k2 -> k1 -> *) x.
(SDecide k3, SDecide k2, SDecide k1) =>
(forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
 (SingI a3, SingI a2, SingI a1) =>
 f a3 a2 a1 -> g a3 a2 a1 -> x)
-> Some3 f -> Some3 g -> Maybe x
same3 forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f a3 a2 a1 -> g a3 a2 a1 -> x
z = \Some3 f
s3l Some3 g
s3g ->
  forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a3, SingI a2, SingI a1) =>
    Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing Some3 f
s3l forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f a3 a2 a1
f ->
    forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a3, SingI a2, SingI a1) =>
    Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing Some3 g
s3g forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3' Sing a2
sa2' Sing a1
sa1' g a3 a2 a1
g -> do
       a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3 Sing a3
sa3'
       a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2 Sing a2
sa2'
       a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1 Sing a1
sa1'
       forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
f a3 a2 a1 -> g a3 a2 a1 -> x
z f a3 a2 a1
f g a3 a2 a1
g)

-- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
-- indexes are equal.
--
-- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@
{-# INLINABLE same4 #-}
same4
  :: forall k4 k3 k2 k1 f g x
  .  (SDecide k4, SDecide k3, SDecide k2, SDecide k1)
  => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1)
        => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x)
  -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  -> Some4 (g :: k4 -> k3 -> k2 -> k1 -> Type)
  -> Maybe x  -- ^
same4 :: forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> *)
       (g :: k4 -> k3 -> k2 -> k1 -> *) x.
(SDecide k4, SDecide k3, SDecide k2, SDecide k1) =>
(forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
 (SingI a4, SingI a3, SingI a2, SingI a1) =>
 f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x)
-> Some4 f -> Some4 g -> Maybe x
same4 forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x
z = \Some4 f
s4l Some4 g
s4g ->
  forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a4, SingI a3, SingI a2, SingI a1) =>
    Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing Some4 f
s4l forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 f a4 a3 a2 a1
f ->
    forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
    (SingI a4, SingI a3, SingI a2, SingI a1) =>
    Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing Some4 g
s4g forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4' Sing a3
sa3' Sing a2
sa2' Sing a1
sa1' g a4 a3 a2 a1
g -> do
       a4 :~: a4
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a4
sa4 Sing a4
sa4'
       a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3 Sing a3
sa3'
       a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2 Sing a2
sa2'
       a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1 Sing a1
sa1'
       forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x
z f a4 a3 a2 a1
f g a4 a3 a2 a1
g)

--------------------------------------------------------------------------------

-- | 'Dict0' is a bit different from 'Dict1', 'Dict2', etc. in that it looks up
-- an instance for the singleton type itself, and not for some other type
-- indexed by said singleton type.
class Dict0 (c :: k0 -> Constraint) where
  -- | Runtime lookup of the @c a0@ instance.
  dict0 :: Sing a0 -> Dict (c a0)

class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where
  -- | Runtime lookup of the @c (f1 a1)@ instance.
  dict1 :: Sing a1 -> Dict (c (f1 a1))

class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where
  -- Runtime lookup of the @c (f2 a2 a1)@ instance.
  dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))

class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where
  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.
  dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))

class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where
  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.
  dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))

--------------------------------------------------------------------------------
-- Miscelaneous @lens@-compatible stuff.

type Prism s t a b
  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)

type Prism' s a = Prism s s a a

prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
prism :: forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism b -> t
bt s -> Either t a
seta = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap s -> Either t a
seta (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> t
bt)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either c a) (Either c b)
right'
{-# INLINE prism #-}

prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' :: forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' b -> s
bs s -> Maybe a
sma = forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism b -> s
bs (\s
s -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a b. a -> Either a b
Left s
s) forall a b. b -> Either a b
Right (s -> Maybe a
sma s
s))
{-# INLINE prism' #-}