{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | This module exports 'Show', 'Read', 'Eq', 'Ord' and 'Generic'  instances for 'Exinst.Some1',
-- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst", provided situable
-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available.
--
-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme
module Exinst.Base () where

import Data.Constraint
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Base.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound))
import Data.Bool.Singletons (SBool(STrue, SFalse))
import qualified Data.List.Singletons as List
import Data.Tuple.Singletons (Tuple2Sym1)
import Data.Singletons.Decide
import qualified GHC.Generics as G
import Prelude
import qualified Text.Read as Read

import Exinst hiding (Some1(..), Some2(..), Some3(..), Some4(..))
import qualified Exinst as Exinst

--------------------------------------------------------------------------------
-- Show

-- Internal wrappers used to avoid writing the string manipulation in 'Show'.
data Some1'Show r1 x = Some1 r1 x deriving (Int -> Some1'Show r1 x -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r1 x. (Show r1, Show x) => Int -> Some1'Show r1 x -> ShowS
forall r1 x. (Show r1, Show x) => [Some1'Show r1 x] -> ShowS
forall r1 x. (Show r1, Show x) => Some1'Show r1 x -> String
showList :: [Some1'Show r1 x] -> ShowS
$cshowList :: forall r1 x. (Show r1, Show x) => [Some1'Show r1 x] -> ShowS
show :: Some1'Show r1 x -> String
$cshow :: forall r1 x. (Show r1, Show x) => Some1'Show r1 x -> String
showsPrec :: Int -> Some1'Show r1 x -> ShowS
$cshowsPrec :: forall r1 x. (Show r1, Show x) => Int -> Some1'Show r1 x -> ShowS
Show)
data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Int -> Some2'Show r2 r1 x -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r2 r1 x.
(Show r2, Show r1, Show x) =>
Int -> Some2'Show r2 r1 x -> ShowS
forall r2 r1 x.
(Show r2, Show r1, Show x) =>
[Some2'Show r2 r1 x] -> ShowS
forall r2 r1 x.
(Show r2, Show r1, Show x) =>
Some2'Show r2 r1 x -> String
showList :: [Some2'Show r2 r1 x] -> ShowS
$cshowList :: forall r2 r1 x.
(Show r2, Show r1, Show x) =>
[Some2'Show r2 r1 x] -> ShowS
show :: Some2'Show r2 r1 x -> String
$cshow :: forall r2 r1 x.
(Show r2, Show r1, Show x) =>
Some2'Show r2 r1 x -> String
showsPrec :: Int -> Some2'Show r2 r1 x -> ShowS
$cshowsPrec :: forall r2 r1 x.
(Show r2, Show r1, Show x) =>
Int -> Some2'Show r2 r1 x -> ShowS
Show)
data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Int -> Some3'Show r3 r2 r1 x -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
Int -> Some3'Show r3 r2 r1 x -> ShowS
forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
[Some3'Show r3 r2 r1 x] -> ShowS
forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
Some3'Show r3 r2 r1 x -> String
showList :: [Some3'Show r3 r2 r1 x] -> ShowS
$cshowList :: forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
[Some3'Show r3 r2 r1 x] -> ShowS
show :: Some3'Show r3 r2 r1 x -> String
$cshow :: forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
Some3'Show r3 r2 r1 x -> String
showsPrec :: Int -> Some3'Show r3 r2 r1 x -> ShowS
$cshowsPrec :: forall r3 r2 r1 x.
(Show r3, Show r2, Show r1, Show x) =>
Int -> Some3'Show r3 r2 r1 x -> ShowS
Show)
data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Int -> Some4'Show r4 r3 r2 r1 x -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
Int -> Some4'Show r4 r3 r2 r1 x -> ShowS
forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
[Some4'Show r4 r3 r2 r1 x] -> ShowS
forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
Some4'Show r4 r3 r2 r1 x -> String
showList :: [Some4'Show r4 r3 r2 r1 x] -> ShowS
$cshowList :: forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
[Some4'Show r4 r3 r2 r1 x] -> ShowS
show :: Some4'Show r4 r3 r2 r1 x -> String
$cshow :: forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
Some4'Show r4 r3 r2 r1 x -> String
showsPrec :: Int -> Some4'Show r4 r3 r2 r1 x -> ShowS
$cshowsPrec :: forall r4 r3 r2 r1 x.
(Show r4, Show r3, Show r2, Show r1, Show x) =>
Int -> Some4'Show r4 r3 r2 r1 x -> ShowS
Show)

instance forall k1 (f :: k1 -> Type)
  . ( SingKind k1
    , Show (Demote k1)
    , Dict1 Show f
    ) => Show (Exinst.Some1 f)
  where
    {-# INLINABLE showsPrec #-}
    showsPrec :: Int -> Some1 f -> ShowS
showsPrec Int
n = \Some1 f
some1x -> forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
some1x forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1 (f a1
x :: f a1) ->
       case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1 :: Dict (Show (f a1)) of
          Dict (Show (f a1))
Dict -> forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (forall r1 x. r1 -> x -> Some1'Show r1 x
Some1 (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1) f a1
x)

instance forall k2 k1 (f :: k2 -> k1 -> Type)
  . ( SingKind k2
    , SingKind k1
    , Show (Demote k2)
    , Show (Demote k1)
    , Dict2 Show f
    ) => Show (Exinst.Some2 f)
  where
    {-# INLINABLE showsPrec #-}
    showsPrec :: Int -> Some2 f -> ShowS
showsPrec Int
n = \Some2 f
some2x -> 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
some2x forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2 Sing a1
sa1 (f a2 a1
x :: f a2 a1) ->
       case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2 Sing a1
sa1 :: Dict (Show (f a2 a1)) of
          Dict (Show (f a2 a1))
Dict -> forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (forall r2 r1 x. r2 -> r1 -> x -> Some2'Show r2 r1 x
Some2 (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) f a2 a1
x)

instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
  . ( SingKind k3
    , SingKind k2
    , SingKind k1
    , Show (Demote k3)
    , Show (Demote k2)
    , Show (Demote k1)
    , Dict3 Show f
    ) => Show (Exinst.Some3 f)
  where
    {-# INLINABLE showsPrec #-}
    showsPrec :: Int -> Some3 f -> ShowS
showsPrec Int
n = \Some3 f
some3x -> 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
some3x forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a3 a2 a1
x :: f a3 a2 a1) ->
       case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Show (f a3 a2 a1)) of
          Dict (Show (f a3 a2 a1))
Dict -> forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (forall r3 r2 r1 x. r3 -> r2 -> r1 -> x -> Some3'Show r3 r2 r1 x
Some3 (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) f a3 a2 a1
x)

instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  . ( SingKind k4
    , SingKind k3
    , SingKind k2
    , SingKind k1
    , Show (Demote k4)
    , Show (Demote k3)
    , Show (Demote k2)
    , Show (Demote k1)
    , Dict4 Show f
    ) => Show (Exinst.Some4 f)
  where
    {-# INLINABLE showsPrec #-}
    showsPrec :: Int -> Some4 f -> ShowS
showsPrec Int
n = \Some4 f
some4x -> 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
some4x forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a4 a3 a2 a1
x :: f a4 a3 a2 a1) ->
       case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Show (f a4 a3 a2 a1)) of
          Dict (Show (f a4 a3 a2 a1))
Dict -> forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (forall r4 r3 r2 r1 x.
r4 -> r3 -> r2 -> r1 -> x -> Some4'Show r4 r3 r2 r1 x
Some4 (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) f a4 a3 a2 a1
x)

--------------------------------------------------------------------------------
-- Read

instance forall k1 (f :: k1 -> Type)
  . ( SingKind k1
    , Read (Demote k1)
    , Dict1 Read f
    ) => Read (Exinst.Some1 f)
  where
    {-# INLINABLE readPrec #-}
    readPrec :: ReadPrec (Some1 f)
readPrec = do
      Read.Ident String
"Some1" <- ReadPrec Lexeme
Read.lexP
      Demote k1
rsa1 <- forall a. Read a => ReadPrec a
Read.readPrec
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
         case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a
sa1 :: Dict (Read (f a1)) of
            Dict (Read (f a))
Dict -> do
               f a
x :: f a1 <- forall a. Read a => ReadPrec a
Read.readPrec
               forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k1 (f1 :: k1 -> *) (a1 :: k1). Sing a1 -> f1 a1 -> Some1 f1
Exinst.Some1 Sing a
sa1 f a
x)

instance forall k2 k1 (f :: k2 -> k1 -> Type)
  . ( SingKind k2
    , SingKind k1
    , Read (Demote k2)
    , Read (Demote k1)
    , Dict2 Read f
    ) => Read (Exinst.Some2 f)
  where
    {-# INLINABLE readPrec #-}
    readPrec :: ReadPrec (Some2 f)
readPrec = do
      Read.Ident String
"Some2" <- ReadPrec Lexeme
Read.lexP
      Demote k2
rsa2 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k1
rsa1 <- forall a. Read a => ReadPrec a
Read.readPrec
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
         forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
            case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a
sa2 Sing a
sa1 :: Dict (Read (f a2 a1)) of
               Dict (Read (f a a))
Dict -> do
                  f a a
x :: f a2 a1 <- forall a. Read a => ReadPrec a
Read.readPrec
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
Sing a2 -> Sing a1 -> f2 a2 a1 -> Some2 f2
Exinst.Some2 Sing a
sa2 Sing a
sa1 f a a
x)

instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
  . ( SingKind k3
    , SingKind k2
    , SingKind k1
    , Read (Demote k3)
    , Read (Demote k2)
    , Read (Demote k1)
    , Dict3 Read f
    ) => Read (Exinst.Some3 f)
  where
    {-# INLINABLE readPrec #-}
    readPrec :: ReadPrec (Some3 f)
readPrec = do
      Read.Ident String
"Some3" <- ReadPrec Lexeme
Read.lexP
      Demote k3
rsa3 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k2
rsa2 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k1
rsa1 <- forall a. Read a => ReadPrec a
Read.readPrec
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
rsa3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
         forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
            forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
               case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Read (f a3 a2 a1)) of
                  Dict (Read (f a a a))
Dict -> do
                     f a a a
x :: f a3 a2 a1 <- forall a. Read a => ReadPrec a
Read.readPrec
                     forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
Exinst.Some3 Sing a
sa3 Sing a
sa2 Sing a
sa1 f a a a
x)

instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  . ( SingKind k4
    , SingKind k3
    , SingKind k2
    , SingKind k1
    , Read (Demote k4)
    , Read (Demote k3)
    , Read (Demote k2)
    , Read (Demote k1)
    , Dict4 Read f
    ) => Read (Exinst.Some4 f)
  where
    {-# INLINABLE readPrec #-}
    readPrec :: ReadPrec (Some4 f)
readPrec = do
      Read.Ident String
"Some4" <- ReadPrec Lexeme
Read.lexP
      Demote k4
rsa4 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k3
rsa3 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k2
rsa2 <- forall a. Read a => ReadPrec a
Read.readPrec
      Demote k1
rsa1 <- forall a. Read a => ReadPrec a
Read.readPrec
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k4
rsa4 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa4 :: Sing (a4 :: k4)) ->
         forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
rsa3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
            forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
               forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
                  case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Read (f a4 a3 a2 a1)) of
                     Dict (Read (f a a a a))
Dict -> do
                        f a a a a
x :: f a4 a3 a2 a1 <- forall a. Read a => ReadPrec a
Read.readPrec
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
Exinst.Some4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 f a a a a
x)

--------------------------------------------------------------------------------
-- Eq

instance forall k1 (f :: k1 -> Type).
  ( SDecide k1
  , Dict1 Eq f
  ) => Eq (Exinst.Some1 f)
  where
  {-# INLINABLE (==) #-}
  == :: Some1 f -> Some1 f -> Bool
(==) = \Some1 f
som1x Some1 f
som1y ->
     forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
som1x forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1x (f a1
x :: f a1x) ->
        forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
som1y forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1y (f a1
y :: f a1y) ->
           forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
              a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
              case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1x :: Dict (Eq (f a1x)) of
                 Dict (Eq (f a1))
Dict -> forall a. a -> Maybe a
Just (f a1
x forall a. Eq a => a -> a -> Bool
== f a1
y)

instance forall k2 k1 (f :: k2 -> k1 -> Type)
  . ( SDecide k2
    , SDecide k1
    , Dict2 Eq f
    ) => Eq (Exinst.Some2 f)
  where
    {-# INLINABLE (==) #-}
    == :: Some2 f -> Some2 f -> Bool
(==) = \Some2 f
som2x Some2 f
som2y ->
       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
som2x forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2x Sing a1
sa1x (f a2 a1
x :: f a2x a1x) ->
          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
som2y forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2y Sing a1
sa1y (f a2 a1
y :: f a2y a1y) ->
             forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2x Sing a1
sa1x :: Dict (Eq (f a2x a1x)) of
                   Dict (Eq (f a2 a1))
Dict -> forall a. a -> Maybe a
Just (f a2 a1
x forall a. Eq a => a -> a -> Bool
== f a2 a1
y)

instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
  . ( SDecide k3
    , SDecide k2
    , SDecide k1
    , Dict3 Eq f
    ) => Eq (Exinst.Some3 f)
  where
    {-# INLINABLE (==) #-}
    == :: Some3 f -> Some3 f -> Bool
(==) = \Some3 f
som3x Some3 f
som3y ->
       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
som3x forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x (f a3 a2 a1
x :: f a3x a2x a1x) ->
          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
som3y forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3y Sing a2
sa2y Sing a1
sa1y (f a3 a2 a1
y :: f a3y a2y a1y) ->
             forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3x Sing a3
sa3y
                a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x :: Dict (Eq (f a3x a2x a1x)) of
                   Dict (Eq (f a3 a2 a1))
Dict -> forall a. a -> Maybe a
Just (f a3 a2 a1
x forall a. Eq a => a -> a -> Bool
== f a3 a2 a1
y)

instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  . ( SDecide k4
    , SDecide k3
    , SDecide k2
    , SDecide k1
    , Dict4 Eq f
    ) => Eq (Exinst.Some4 f)
  where
    {-# INLINABLE (==) #-}
    == :: Some4 f -> Some4 f -> Bool
(==) = \Some4 f
som4x Some4 f
som4y ->
       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
som4x forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4x Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x (f a4 a3 a2 a1
x :: f a4x a3x a2x a1x) ->
          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
som4y forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4y Sing a3
sa3y Sing a2
sa2y Sing a1
sa1y (f a4 a3 a2 a1
y :: f a4y a3y a2y a1y) ->
             forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                a4 :~: a4
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a4
sa4x Sing a4
sa4y
                a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3x Sing a3
sa3y
                a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4x Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of
                   Dict (Eq (f a4 a3 a2 a1))
Dict -> forall a. a -> Maybe a
Just (f a4 a3 a2 a1
x forall a. Eq a => a -> a -> Bool
== f a4 a3 a2 a1
y)

--------------------------------------------------------------------------------
-- Ord

instance forall k1 (f :: k1 -> Type)
  . ( SingKind k1
    , SDecide k1
    , Ord (Demote k1)
    , Dict1 Ord f
    , Eq (Exinst.Some1 f)
    ) => Ord (Exinst.Some1 f)
  where
    {-# INLINABLE compare #-}
    compare :: Some1 f -> Some1 f -> Ordering
compare = \Some1 f
som1x Some1 f
som1y ->
       forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
som1x forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1x (f a1
x :: f a1x) ->
          forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
som1y forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1y (f a1
y :: f a1y) ->
             let termCompare :: Ordering
termCompare = forall a. Ord a => a -> a -> Ordering
compare (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1x) (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1y)
             in forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ordering
termCompare forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                  a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                  case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1x :: Dict (Ord (f a1x)) of
                     Dict (Ord (f a1))
Dict -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> Ordering
compare f a1
x f a1
y)

instance forall k2 k1 (f :: k2 -> k1 -> Type)
  . ( SingKind k2
    , SingKind k1
    , SDecide k2
    , SDecide k1
    , Ord (Demote k2)
    , Ord (Demote k1)
    , Dict2 Ord f
    , Eq (Exinst.Some2 f)
    ) => Ord (Exinst.Some2 f)
  where
    {-# INLINABLE compare #-}
    compare :: Some2 f -> Some2 f -> Ordering
compare = \Some2 f
som2x Some2 f
som2y ->
       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
som2x forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2x Sing a1
sa1x (f a2 a1
x :: f a2x a1x) ->
          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
som2y forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2y Sing a1
sa1y (f a2 a1
y :: f a2y a1y) ->
             let termCompare :: Ordering
termCompare = forall a. Ord a => a -> a -> Ordering
compare (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1x)
                                       (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1y)
             in forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ordering
termCompare forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                   a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                   a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                   case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2x Sing a1
sa1x :: Dict (Ord (f a2x a1x)) of
                      Dict (Ord (f a2 a1))
Dict -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> Ordering
compare f a2 a1
x f a2 a1
y)

instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
  . ( SingKind k3
    , SingKind k2
    , SingKind k1
    , SDecide k3
    , SDecide k2
    , SDecide k1
    , Ord (Demote k3)
    , Ord (Demote k2)
    , Ord (Demote k1)
    , Dict3 Ord f
    , Eq (Exinst.Some3 f)
    ) => Ord (Exinst.Some3 f)
  where
    {-# INLINABLE compare #-}
    compare :: Some3 f -> Some3 f -> Ordering
compare = \Some3 f
som3x Some3 f
som3y ->
       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
som3x forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x (f a3 a2 a1
x :: f a3x a2x a1x) ->
          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
som3y forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3y Sing a2
sa2y Sing a1
sa1y (f a3 a2 a1
y :: f a3y a2y a1y) ->
             let termCompare :: Ordering
termCompare = forall a. Ord a => a -> a -> Ordering
compare
                   (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1x)
                   (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1y)
             in forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ordering
termCompare forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                  a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3x Sing a3
sa3y
                  a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                  a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                  case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x :: Dict (Ord (f a3x a2x a1x)) of
                     Dict (Ord (f a3 a2 a1))
Dict -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> Ordering
compare f a3 a2 a1
x f a3 a2 a1
y)

instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  . ( SingKind k4
    , SingKind k3
    , SingKind k2
    , SingKind k1
    , SDecide k4
    , SDecide k3
    , SDecide k2
    , SDecide k1
    , Ord (Demote k4)
    , Ord (Demote k3)
    , Ord (Demote k2)
    , Ord (Demote k1)
    , Dict4 Ord f
    , Eq (Exinst.Some4 f)
    ) => Ord (Exinst.Some4 f)
  where
    {-# INLINABLE compare #-}
    compare :: Some4 f -> Some4 f -> Ordering
compare = \Some4 f
som4x Some4 f
som4y ->
       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
som4x forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4x Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x (f a4 a3 a2 a1
x :: f a4x a3x a2x a1x) ->
          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
som4y forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4y Sing a3
sa3y Sing a2
sa2y Sing a1
sa1y (f a4 a3 a2 a1
y :: f a4y a3y a2y a1y) ->
             let termCompare :: Ordering
termCompare = forall a. Ord a => a -> a -> Ordering
compare
                   (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a4
sa4x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2x, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1x)
                   (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a4
sa4y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2y, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1y)
             in forall b a. b -> (a -> b) -> Maybe a -> b
maybe Ordering
termCompare forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ do
                  a4 :~: a4
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a4
sa4x Sing a4
sa4y
                  a3 :~: a3
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a3
sa3x Sing a3
sa3y
                  a2 :~: a2
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a2
sa2x Sing a2
sa2y
                  a1 :~: a1
Refl <- forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality Sing a1
sa1x Sing a1
sa1y
                  case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4x Sing a3
sa3x Sing a2
sa2x Sing a1
sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of
                     Dict (Ord (f a4 a3 a2 a1))
Dict -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> Ordering
compare f a4 a3 a2 a1
x f a4 a3 a2 a1
y)

--------------------------------------------------------------------------------
-- Generic

type Eithers1 (f :: k1 -> Type) =
  Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f

-- | TODO: Mak1e this logarithmic.
type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where
  Eithers1' (x ': '[]) f = f x
  Eithers1' (x ': xs)  f = Either (f x) (Eithers1' xs f)

instance forall k1 (f :: k1 -> Type)
  . ( SingKind k1
    , PEnum (Demote k1)
    , PBounded (Demote k1)
    , G.Generic (Demote k1)
    , Dict1 G.Generic f
    , Dict1 (Inj (Eithers1 f)) f
    ) => G.Generic (Exinst.Some1 f)
  where
    type Rep (Exinst.Some1 (f :: k1 -> Type)) =
      G.Rep (Demote k1, Eithers1 f)
    {-# INLINABLE from #-}
    from :: forall x. Some1 f -> Rep (Some1 f) x
from = \Some1 f
s1x -> forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
s1x forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1 (f a1
x :: f a1) ->
      case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1 :: Dict (G.Generic (f a1)) of
        Dict (Generic (f a1))
Dict -> case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1 :: Dict (Inj (Eithers1 f) (f a1)) of
          Dict (Inj (Eithers1 f) (f a1))
Dict -> forall a x. Generic a => a -> Rep a x
G.from (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1, forall b a. Inj b a => a -> b
inj f a1
x)
    {-# INLINABLE to #-}
    to :: forall x. Rep (Some1 f) x -> Some1 f
to = \(G.M1 (G.M1 (G.M1 (G.K1 Demote k1
da1) G.:*: G.M1 (G.K1 Eithers1 f
ex)))) ->
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
da1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
        case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a
sa1 :: Dict (Inj (Eithers1 f) (f a1)) of
          Dict (Inj (Eithers1 f) (f a))
Dict -> case forall b a. Inj b a => b -> Maybe a
prj Eithers1 f
ex of
            Just f a
x -> forall k1 (f1 :: k1 -> *) (a1 :: k1). Sing a1 -> f1 a1 -> Some1 f1
Exinst.Some1 Sing a
sa1 (f a
x :: f a1)
            Maybe (f a)
Nothing -> forall a. HasCallStack => String -> a
error String
"Generic Some1: Malformed Rep"

---
type Eithers2 (f :: k2 -> k1 -> Type) =
  Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f

-- | TODO: Mak1e this logarithmic.
type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where
  Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1
  Eithers2' ( '(x2, x1) ': xs)  f = Either (f x2 x1) (Eithers2' xs f)

type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where
  Cartesian2 '[] xs1 = '[]
  Cartesian2 (x2 ': xs2) xs1 =
    List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1]


instance forall k2 k1 (f :: k2 -> k1 -> Type)
  . ( SingKind k2
    , SingKind k1
    , PEnum (Demote k2)
    , PEnum (Demote k1)
    , PBounded (Demote k2)
    , PBounded (Demote k1)
    , G.Generic (Demote k2)
    , G.Generic (Demote k1)
    , Dict2 G.Generic f
    , Dict2 (Inj (Eithers2 f)) f
    ) => G.Generic (Exinst.Some2 f)
  where
    type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) =
      G.Rep ((Demote k2, Demote k1), Eithers2 f)
    {-# INLINABLE from #-}
    from :: forall x. Some2 f -> Rep (Some2 f) x
from = \Some2 f
s2x -> 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
s2x forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2 Sing a1
sa1 (f a2 a1
x :: f a2 a1) ->
      case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2 Sing a1
sa1 :: Dict (G.Generic (f a2 a1)) of
        Dict (Generic (f a2 a1))
Dict -> case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2 Sing a1
sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of
          Dict (Inj (Eithers2 f) (f a2 a1))
Dict -> forall a x. Generic a => a -> Rep a x
G.from ((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), forall b a. Inj b a => a -> b
inj f a2 a1
x)
    {-# INLINABLE to #-}
    to :: forall x. Rep (Some2 f) x -> Some2 f
to = \(G.M1 (G.M1 (G.M1 (G.K1 (Demote k2
da2, Demote k1
da1)) G.:*: G.M1 (G.K1 Eithers2 f
ex)))) ->
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
da2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
        forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
da1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
          case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a
sa2 Sing a
sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of
            Dict (Inj (Eithers2 f) (f a a))
Dict -> case forall b a. Inj b a => b -> Maybe a
prj Eithers2 f
ex of
              Just f a a
x -> forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
Sing a2 -> Sing a1 -> f2 a2 a1 -> Some2 f2
Exinst.Some2 Sing a
sa2 Sing a
sa1 (f a a
x :: f a2 a1)
              Maybe (f a a)
Nothing -> forall a. HasCallStack => String -> a
error String
"Generic Some2: Malformed Rep"


---
type Eithers3 (f :: k3 -> k2 -> k1 -> Type) =
  Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3))
                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f

-- | TODO: Mak1e this logarithmic.
type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where
  Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1
  Eithers3' ( '(x3, '(x2, x1)) ': xs)  f = Either (f x3 x2 x1) (Eithers3' xs f)

-- | We use nested 2-tuples instead of 3-tuples because it's easier to implement.
type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where
  Cartesian3 '[] xs2 xs1 = '[]
  Cartesian3 (x3 ': xs3) xs2 xs1 =
    List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1)
                , Cartesian3 xs3 xs2 xs1 ]


instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
  . ( SingKind k3
    , SingKind k2
    , SingKind k1
    , PEnum (Demote k3)
    , PEnum (Demote k2)
    , PEnum (Demote k1)
    , PBounded (Demote k3)
    , PBounded (Demote k2)
    , PBounded (Demote k1)
    , G.Generic (Demote k3)
    , G.Generic (Demote k2)
    , G.Generic (Demote k1)
    , Dict3 G.Generic f
    , Dict3 (Inj (Eithers3 f)) f
    ) => G.Generic (Exinst.Some3 f)
  where
    type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) =
      G.Rep ((Demote k3, Demote k2, Demote k1), Eithers3 f)
    {-# INLINABLE from #-}
    from :: forall x. Some3 f -> Rep (Some3 f) x
from = \Some3 f
s3x -> 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
s3x forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a3 a2 a1
x :: f a3 a2 a1) ->
      case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (G.Generic (f a3 a2 a1)) of
        Dict (Generic (f a3 a2 a1))
Dict -> case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of
          Dict (Inj (Eithers3 f) (f a3 a2 a1))
Dict -> forall a x. Generic a => a -> Rep a x
G.from ((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), forall b a. Inj b a => a -> b
inj f a3 a2 a1
x)
    {-# INLINABLE to #-}
    to :: forall x. Rep (Some3 f) x -> Some3 f
to = \(G.M1 (G.M1 (G.M1 (G.K1 (Demote k3
da3, Demote k2
da2, Demote k1
da1)) G.:*: G.M1 (G.K1 Eithers3 f
ex)))) ->
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
da3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
        forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
da2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
          forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
da1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
            case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of
              Dict (Inj (Eithers3 f) (f a a a))
Dict -> case forall b a. Inj b a => b -> Maybe a
prj Eithers3 f
ex of
                Just f a a a
x -> 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
Exinst.Some3 Sing a
sa3 Sing a
sa2 Sing a
sa1 (f a a a
x :: f a3 a2 a1)
                Maybe (f a a a)
Nothing -> forall a. HasCallStack => String -> a
error String
"Generic Some3: Malformed Rep"


---
type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) =
  Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4))
                        (EnumFromTo (MinBound :: k3) (MaxBound :: k3))
                        (EnumFromTo (MinBound :: k2) (MaxBound :: k2))
                        (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f

-- | TODO: Mak1e this logarithmic.
type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where
  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1
  Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs)  f = Either (f x4 x3 x2 x1) (Eithers4' xs f)

-- | We use nested 2-tuples instead of 4-tuples because it's easier to implement.
type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where
  Cartesian4 '[] xs3 xs2 xs1 = '[]
  Cartesian4 (x4 ': xs4) xs3 xs2 xs1 =
    List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1)
                , Cartesian4 xs4 xs3 xs2 xs1 ]


instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
  . ( SingKind k4
    , SingKind k3
    , SingKind k2
    , SingKind k1
    , PEnum (Demote k4)
    , PEnum (Demote k3)
    , PEnum (Demote k2)
    , PEnum (Demote k1)
    , PBounded (Demote k4)
    , PBounded (Demote k3)
    , PBounded (Demote k2)
    , PBounded (Demote k1)
    , G.Generic (Demote k4)
    , G.Generic (Demote k3)
    , G.Generic (Demote k2)
    , G.Generic (Demote k1)
    , Dict4 G.Generic f
    , Dict4 (Inj (Eithers4 f)) f
    ) => G.Generic (Exinst.Some4 f)
  where
    type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) =
      G.Rep ((Demote k4, Demote k3, Demote k2, Demote k1), Eithers4 f)
    {-# INLINABLE from #-}
    from :: forall x. Some4 f -> Rep (Some4 f) x
from = \Some4 f
s4x -> 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
s4x forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a4 a3 a2 a1
x :: f a4 a3 a2 a1) ->
      case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of
        Dict (Generic (f a4 a3 a2 a1))
Dict -> case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of
          Dict (Inj (Eithers4 f) (f a4 a3 a2 a1))
Dict -> forall a x. Generic a => a -> Rep a x
G.from ((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), forall b a. Inj b a => a -> b
inj f a4 a3 a2 a1
x)
    {-# INLINABLE to #-}
    to :: forall x. Rep (Some4 f) x -> Some4 f
to = \(G.M1 (G.M1 (G.M1 (G.K1 (Demote k4
da4, Demote k3
da3, Demote k2
da2, Demote k1
da1)) G.:*: G.M1 (G.K1 Eithers4 f
ex)))) ->
      forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k4
da4 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa4 :: Sing (a4 :: k4)) ->
        forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
da3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
          forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
da2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
            forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
da1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
              case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
       (f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
       (a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of
                Dict (Inj (Eithers4 f) (f a a a a))
Dict -> case forall b a. Inj b a => b -> Maybe a
prj Eithers4 f
ex of
                  Just f a a a a
x -> 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
Exinst.Some4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 (f a a a a
x :: f a4 a3 a2 a1)
                  Maybe (f a a a a)
Nothing -> forall a. HasCallStack => String -> a
error String
"Generic Some4: Malformed Rep"

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- Out of the box 'DictX' instances for some @base@ types

instance forall c.
  (c 'False, c 'True
  ) => Dict0 (c :: Bool -> Constraint) where
  {-# INLINABLE dict0 #-}
  dict0 :: forall (a0 :: Bool). Sing a0 -> Dict (c a0)
dict0 = \case { Sing a0
SBool a0
SFalse -> forall (a :: Constraint). a => Dict a
Dict; Sing a0
SBool a0
STrue -> forall (a :: Constraint). a => Dict a
Dict }

instance forall k0 c f.
  ( c (f 'False), c (f 'True)
  ) => Dict1 c (f :: Bool -> k0) where
  {-# INLINABLE dict1 #-}
  dict1 :: forall (a1 :: Bool). Sing a1 -> Dict (c (f a1))
dict1 = \case { Sing a1
SBool a1
SFalse -> forall (a :: Constraint). a => Dict a
Dict; Sing a1
SBool a1
STrue -> forall (a :: Constraint). a => Dict a
Dict }

instance forall k1 k0 c f.
  ( Dict1 c (f 'False), Dict1 c (f 'True)
  ) => Dict2 c (f :: Bool -> k1 -> k0) where
  {-# INLINABLE dict2 #-}
  dict2 :: forall (a2 :: Bool) (a1 :: k1).
Sing a2 -> Sing a1 -> Dict (c (f a2 a1))
dict2 = \Sing a2
x -> case Sing a2
x of { Sing a2
SBool a2
SFalse -> forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1; Sing a2
SBool a2
STrue -> forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 }

instance forall k2 k1 k0 c f.
  ( Dict2 c (f 'False), Dict2 c (f 'True)
  ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where
  {-# INLINABLE dict3 #-}
  dict3 :: forall (a3 :: Bool) (a2 :: k2) (a1 :: k1).
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f a3 a2 a1))
dict3 = \Sing a3
x -> case Sing a3
x of { Sing a3
SBool a3
SFalse -> forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2; Sing a3
SBool a3
STrue -> forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
       (a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 }

instance forall k3 k2 k1 k0 c f.
  ( Dict3 c (f 'False), Dict3 c (f 'True)
  ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where
  {-# INLINABLE dict4 #-}
  dict4 :: forall (a4 :: Bool) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f a4 a3 a2 a1))
dict4 = \Sing a4
x -> case Sing a4
x of { Sing a4
SBool a4
SFalse -> forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3; Sing a4
SBool a4
STrue -> forall k0 k3 k2 k1 (c :: k0 -> Constraint)
       (f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 }

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- Misc

class Inj b a where
  inj :: a -> b
  prj :: b -> Maybe a
instance Inj a a where
  {-# INLINE inj #-}
  inj :: a -> a
inj = forall a. a -> a
id
  {-# INLINE prj #-}
  prj :: a -> Maybe a
prj = forall a. a -> Maybe a
Just
instance Inj (Either a b) a where
  {-# INLINE inj #-}
  inj :: a -> Either a b
inj = forall a b. a -> Either a b
Left
  {-# INLINE prj #-}
  prj :: Either a b -> Maybe a
prj = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> Maybe a
Just (forall a b. a -> b -> a
const forall a. Maybe a
Nothing)
-- | TODO: Make this logarithmic.
instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where
  {-# INLINE inj #-}
  inj :: a -> Either b x
inj = forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Inj b a => a -> b
inj
  {-# INLINE prj #-}
  prj :: Either b x -> Maybe a
prj = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall b a. Inj b a => b -> Maybe a
prj