{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Ouroboros.Consensus.HardFork.Combinator.Lifting (
    LiftMismatch (..)
  , LiftNP (..)
  , LiftNS (..)
  , LiftNamedMismatch (..)
  , LiftNamedNP (..)
  , LiftNamedNS (..)
  , LiftNamedTelescope (..)
  , LiftOptNP (..)
  , LiftTelescope (..)
  ) where

import           Data.List (intercalate)
import           Data.Proxy
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Dict (Dict (..), all_NP, unAll_NP)
import           Data.SOP.Match (Mismatch)
import           Data.SOP.OptNP (OptNP (..))
import           Data.SOP.Sing
import           Data.SOP.Strict
import           Data.SOP.Telescope (Telescope)
import           Data.Typeable
import           GHC.TypeLits
import           NoThunks.Class (NoThunks (..))
import           Ouroboros.Consensus.HardFork.Combinator.Abstract

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

proofAll :: SListI xs
         => (forall x . Dict c x -> Dict d x)
         -> Dict (All c) xs -> Dict (All d) xs
proofAll :: forall (xs :: [*]) (c :: * -> Constraint) (d :: * -> Constraint).
SListI xs =>
(forall x. Dict c x -> Dict d x)
-> Dict (All c) xs -> Dict (All d) xs
proofAll forall x. Dict c x -> Dict d x
f Dict (All c) xs
dict = NP (Dict d) xs -> Dict (All d) xs
forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall x. Dict c x -> Dict d x)
-> NP (Dict c) xs -> NP (Dict d) xs
forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap Dict c a -> Dict d a
forall x. Dict c x -> Dict d x
f (Dict (All c) xs -> NP (Dict c) xs
forall {k} (c :: k -> Constraint) (xs :: [k]).
Dict (All c) xs -> NP (Dict c) xs
unAll_NP Dict (All c) xs
dict))

proofLift :: (SingleEraBlock x => c (f x))
          => Dict SingleEraBlock x -> Dict (Compose c f) x
proofLift :: forall x (c :: * -> Constraint) (f :: * -> *).
(SingleEraBlock x => c (f x)) =>
Dict SingleEraBlock x -> Dict (Compose c f) x
proofLift Dict SingleEraBlock x
Dict = Dict (Compose c f) x
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

liftEras :: (All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x))
         => Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras :: forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras Proxy xs
_ Proxy c
_ Proxy f
_ = (forall x. Dict SingleEraBlock x -> Dict (Compose c f) x)
-> Dict (All SingleEraBlock) xs -> Dict (All (Compose c f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (d :: * -> Constraint).
SListI xs =>
(forall x. Dict c x -> Dict d x)
-> Dict (All c) xs -> Dict (All d) xs
proofAll Dict SingleEraBlock x -> Dict (Compose c f) x
forall x. Dict SingleEraBlock x -> Dict (Compose c f) x
forall x (c :: * -> Constraint) (f :: * -> *).
(SingleEraBlock x => c (f x)) =>
Dict SingleEraBlock x -> Dict (Compose c f) x
proofLift Dict (All SingleEraBlock) xs
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

{-------------------------------------------------------------------------------
  LiftNS
-------------------------------------------------------------------------------}

newtype LiftNS f xs = LiftNS (NS f xs)

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Eq (f x))
      => Eq (LiftNS f xs) where
  LiftNS NS f xs
x == :: LiftNS f xs -> LiftNS f xs -> Bool
== LiftNS NS f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
          NS f xs
x NS f xs -> NS f xs -> Bool
forall a. Eq a => a -> a -> Bool
== NS f xs
y
        }

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Ord (f x))
      => Ord (LiftNS f xs) where
  LiftNS NS f xs
x compare :: LiftNS f xs -> LiftNS f xs -> Ordering
`compare` LiftNS NS f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy f -> Dict (All (Compose Ord f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Ord f)) xs
Dict ->
          NS f xs
x NS f xs -> NS f xs -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` NS f xs
y
        }}

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Show (f x))
      => Show (LiftNS f xs) where
  show :: LiftNS f xs -> String
show (LiftNS NS f xs
x) =
      case Proxy xs -> Proxy Show -> Proxy f -> Dict (All (Compose Show f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Show f)) xs
Dict ->
          NS f xs -> String
forall a. Show a => a -> String
show NS f xs
x
        }

{-------------------------------------------------------------------------------
  LiftNP
-------------------------------------------------------------------------------}

newtype LiftNP f xs = LiftNP (NP f xs)

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Eq (f x))
      => Eq (LiftNP f xs) where
  LiftNP NP f xs
x == :: LiftNP f xs -> LiftNP f xs -> Bool
== LiftNP NP f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
          NP f xs
x NP f xs -> NP f xs -> Bool
forall a. Eq a => a -> a -> Bool
== NP f xs
y
        }

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Ord (f x))
      => Ord (LiftNP f xs) where
  LiftNP NP f xs
x compare :: LiftNP f xs -> LiftNP f xs -> Ordering
`compare` LiftNP NP f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy f -> Dict (All (Compose Ord f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Ord f)) xs
Dict ->
          NP f xs
x NP f xs -> NP f xs -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` NP f xs
y
        }}

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Show (f x))
      => Show (LiftNP f xs) where
  show :: LiftNP f xs -> String
show (LiftNP NP f xs
x) =
      case Proxy xs -> Proxy Show -> Proxy f -> Dict (All (Compose Show f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Show f)) xs
Dict ->
          NP f xs -> String
forall a. Show a => a -> String
show NP f xs
x
        }

{-------------------------------------------------------------------------------
  LiftOptNP
-------------------------------------------------------------------------------}

newtype LiftOptNP empty f xs = LiftOptNP (OptNP empty f xs)

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Eq (f x))
      => Eq (LiftOptNP empty f xs) where
  LiftOptNP OptNP empty f xs
x == :: LiftOptNP empty f xs -> LiftOptNP empty f xs -> Bool
== LiftOptNP OptNP empty f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
          OptNP empty f xs
x OptNP empty f xs -> OptNP empty f xs -> Bool
forall a. Eq a => a -> a -> Bool
== OptNP empty f xs
y
        }

instance (All SingleEraBlock xs, forall x. SingleEraBlock x => Show (f x))
      => Show (LiftOptNP empty f xs) where
  show :: LiftOptNP empty f xs -> String
show (LiftOptNP OptNP empty f xs
x) =
      case Proxy xs -> Proxy Show -> Proxy f -> Dict (All (Compose Show f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Show f)) xs
Dict ->
          OptNP empty f xs -> String
forall a. Show a => a -> String
show OptNP empty f xs
x
        }

{-------------------------------------------------------------------------------
  LiftTelescope
-------------------------------------------------------------------------------}

newtype LiftTelescope g f xs = LiftTelescope (Telescope g f xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Eq (g x)
         , forall x. SingleEraBlock x => Eq (f x)
         ) => Eq (LiftTelescope g f xs) where
  LiftTelescope Telescope g f xs
x == :: LiftTelescope g f xs -> LiftTelescope g f xs -> Bool
== LiftTelescope Telescope g f xs
y =
      case Proxy xs -> Proxy Eq -> Proxy g -> Dict (All (Compose Eq g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Eq g)) xs
Dict ->
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
          Telescope g f xs
x Telescope g f xs -> Telescope g f xs -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope g f xs
y
        }}

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Ord (f x)
         , forall x. SingleEraBlock x => Ord (g x)
         ) => Ord (LiftTelescope g f xs) where
  compare :: LiftTelescope g f xs -> LiftTelescope g f xs -> Ordering
compare (LiftTelescope Telescope g f xs
x) (LiftTelescope Telescope g f xs
y) =
      case Proxy xs -> Proxy Eq -> Proxy g -> Dict (All (Compose Eq g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Eq g)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy g -> Dict (All (Compose Ord g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Ord g)) xs
Dict ->
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy f -> Dict (All (Compose Ord f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Ord f)) xs
Dict ->
          Telescope g f xs -> Telescope g f xs -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Telescope g f xs
x Telescope g f xs
y
        }}}}

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Show (g x)
         , forall x. SingleEraBlock x => Show (f x)
         ) => Show (LiftTelescope g f xs) where
  show :: LiftTelescope g f xs -> String
show (LiftTelescope Telescope g f xs
x) =
      case Proxy xs -> Proxy Show -> Proxy g -> Dict (All (Compose Show g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Show g)) xs
Dict ->
      case Proxy xs -> Proxy Show -> Proxy f -> Dict (All (Compose Show f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Show f)) xs
Dict ->
          Telescope g f xs -> String
forall a. Show a => a -> String
show Telescope g f xs
x
        }}

{-------------------------------------------------------------------------------
  LiftMismatch
-------------------------------------------------------------------------------}

newtype LiftMismatch f g xs = LiftMismatch (Mismatch f g xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Eq (f x)
         , forall x. SingleEraBlock x => Eq (g x)
         ) => Eq (LiftMismatch f g xs) where
  LiftMismatch Mismatch f g xs
x == :: LiftMismatch f g xs -> LiftMismatch f g xs -> Bool
== LiftMismatch Mismatch f g xs
y =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
      case Proxy xs -> Proxy Eq -> Proxy g -> Dict (All (Compose Eq g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Eq g)) xs
Dict ->
          Mismatch f g xs
x Mismatch f g xs -> Mismatch f g xs -> Bool
forall a. Eq a => a -> a -> Bool
== Mismatch f g xs
y
        }}

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Ord (f x)
         , forall x. SingleEraBlock x => Ord (g x)
         ) => Ord (LiftMismatch f g xs) where
  compare :: LiftMismatch f g xs -> LiftMismatch f g xs -> Ordering
compare (LiftMismatch Mismatch f g xs
x) (LiftMismatch Mismatch f g xs
y) =
      case Proxy xs -> Proxy Eq -> Proxy f -> Dict (All (Compose Eq f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Eq f)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy f -> Dict (All (Compose Ord f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Ord f)) xs
Dict ->
      case Proxy xs -> Proxy Eq -> Proxy g -> Dict (All (Compose Eq g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Eq)  (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Eq g)) xs
Dict ->
      case Proxy xs -> Proxy Ord -> Proxy g -> Dict (All (Compose Ord g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Ord) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Ord g)) xs
Dict ->
          Mismatch f g xs -> Mismatch f g xs -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Mismatch f g xs
x Mismatch f g xs
y
        }}}}

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => Show (f x)
         , forall x. SingleEraBlock x => Show (g x)
         ) => Show (LiftMismatch f g xs) where
  show :: LiftMismatch f g xs -> String
show (LiftMismatch Mismatch f g xs
x) =
      case Proxy xs -> Proxy Show -> Proxy f -> Dict (All (Compose Show f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose Show f)) xs
Dict ->
      case Proxy xs -> Proxy Show -> Proxy g -> Dict (All (Compose Show g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose Show g)) xs
Dict ->
          Mismatch f g xs -> String
forall a. Show a => a -> String
show Mismatch f g xs
x
        }}

{-------------------------------------------------------------------------------
  LiftNamedNS
-------------------------------------------------------------------------------}

newtype LiftNamedNS (name :: Symbol) f xs = LiftNamedNS (NS f xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => NoThunks (f x)
         , KnownSymbol name
         ) => NoThunks (LiftNamedNS name f xs) where
  showTypeOf :: Proxy (LiftNamedNS name f xs) -> String
showTypeOf Proxy (LiftNamedNS name f xs)
_ = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @name) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList xs -> String
forall (xs :: [*]). All SingleEraBlock xs => SList xs -> String
showBlockTypes (SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs)

  wNoThunks :: Context -> LiftNamedNS name f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (LiftNamedNS NS f xs
x) =
      case Proxy xs
-> Proxy NoThunks -> Proxy f -> Dict (All (Compose NoThunks f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose NoThunks f)) xs
Dict ->
          Context -> NS f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt NS f xs
x
        }

{-------------------------------------------------------------------------------
  LiftNamedNP
-------------------------------------------------------------------------------}

newtype LiftNamedNP (name :: Symbol) f xs = LiftNamedNP (NP f xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => NoThunks (f x)
         , KnownSymbol name
         ) => NoThunks (LiftNamedNP name f xs) where
  showTypeOf :: Proxy (LiftNamedNP name f xs) -> String
showTypeOf Proxy (LiftNamedNP name f xs)
_ = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @name) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList xs -> String
forall (xs :: [*]). All SingleEraBlock xs => SList xs -> String
showBlockTypes (SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs)

  wNoThunks :: Context -> LiftNamedNP name f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (LiftNamedNP NP f xs
x) =
      case Proxy xs
-> Proxy NoThunks -> Proxy f -> Dict (All (Compose NoThunks f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose NoThunks f)) xs
Dict ->
          Context -> NP f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt NP f xs
x
        }

{-------------------------------------------------------------------------------
  LiftNamedTelescope
-------------------------------------------------------------------------------}

newtype LiftNamedTelescope (name :: Symbol) f g xs = LiftNamedTelescope (Telescope f g xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => NoThunks (f x)
         , forall x. SingleEraBlock x => NoThunks (g x)
         , KnownSymbol name
         ) => NoThunks (LiftNamedTelescope name f g xs) where
  showTypeOf :: Proxy (LiftNamedTelescope name f g xs) -> String
showTypeOf Proxy (LiftNamedTelescope name f g xs)
_ = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @name) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList xs -> String
forall (xs :: [*]). All SingleEraBlock xs => SList xs -> String
showBlockTypes (SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs)

  wNoThunks :: Context -> LiftNamedTelescope name f g xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (LiftNamedTelescope Telescope f g xs
x) =
      case Proxy xs
-> Proxy NoThunks -> Proxy f -> Dict (All (Compose NoThunks f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose NoThunks f)) xs
Dict ->
      case Proxy xs
-> Proxy NoThunks -> Proxy g -> Dict (All (Compose NoThunks g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose NoThunks g)) xs
Dict ->
          Context -> Telescope f g xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt Telescope f g xs
x
        }}

{-------------------------------------------------------------------------------
  LiftNamedTelescope
-------------------------------------------------------------------------------}

newtype LiftNamedMismatch (name :: Symbol) f g xs = LiftNamedMismatch (Mismatch f g xs)

instance ( All SingleEraBlock xs
         , forall x. SingleEraBlock x => NoThunks (f x)
         , forall x. SingleEraBlock x => NoThunks (g x)
         , KnownSymbol name
         ) => NoThunks (LiftNamedMismatch name f g xs) where
  showTypeOf :: Proxy (LiftNamedMismatch name f g xs) -> String
showTypeOf Proxy (LiftNamedMismatch name f g xs)
_ = Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @name) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SList xs -> String
forall (xs :: [*]). All SingleEraBlock xs => SList xs -> String
showBlockTypes (SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs)

  wNoThunks :: Context -> LiftNamedMismatch name f g xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt (LiftNamedMismatch Mismatch f g xs
x) =
      case Proxy xs
-> Proxy NoThunks -> Proxy f -> Dict (All (Compose NoThunks f)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) of { Dict (All (Compose NoThunks f)) xs
Dict ->
      case Proxy xs
-> Proxy NoThunks -> Proxy g -> Dict (All (Compose NoThunks g)) xs
forall (xs :: [*]) (c :: * -> Constraint) (f :: * -> *).
(All SingleEraBlock xs, forall x. SingleEraBlock x => c (f x)) =>
Proxy xs -> Proxy c -> Proxy f -> Dict (All (Compose c f)) xs
liftEras (forall (t :: [*]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @xs) (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @NoThunks) (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) of { Dict (All (Compose NoThunks g)) xs
Dict ->
          Context -> Mismatch f g xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt Mismatch f g xs
x
        }}

{-------------------------------------------------------------------------------
  Auxiliary
-------------------------------------------------------------------------------}

showBlockTypes :: All SingleEraBlock xs => SList xs -> String
showBlockTypes :: forall (xs :: [*]). All SingleEraBlock xs => SList xs -> String
showBlockTypes =
    (\Context
names -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Context -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," Context
names String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]") (Context -> String) -> (SList xs -> Context) -> SList xs -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K String) xs -> Context
NP (K String) xs -> CollapseTo NP String
forall (xs :: [*]) a.
SListIN NP xs =>
NP (K a) xs -> CollapseTo NP a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse (NP (K String) xs -> Context)
-> (SList xs -> NP (K String) xs) -> SList xs -> Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList xs -> NP (K String) xs
forall (xs' :: [*]).
All SingleEraBlock xs' =>
SList xs' -> NP (K String) xs'
go
  where
    go :: All SingleEraBlock xs' => SList xs' -> NP (K String) xs'
    go :: forall (xs' :: [*]).
All SingleEraBlock xs' =>
SList xs' -> NP (K String) xs'
go SList xs'
SNil  = NP (K String) xs'
NP (K String) '[]
forall {k} (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = K String x
forall blk. SingleEraBlock blk => K String blk
typeRep' K String x -> NP (K String) xs -> NP (K String) (x : xs)
forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* SList xs -> NP (K String) xs
forall (xs' :: [*]).
All SingleEraBlock xs' =>
SList xs' -> NP (K String) xs'
go SList xs
forall {k} (xs :: [k]). SListI xs => SList xs
sList

    typeRep' :: forall blk. SingleEraBlock blk => K String blk
    typeRep' :: forall blk. SingleEraBlock blk => K String blk
typeRep' = String -> K String blk
forall k a (b :: k). a -> K a b
K (String -> K String blk)
-> (TypeRep -> String) -> TypeRep -> K String blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> K String blk) -> TypeRep -> K String blk
forall a b. (a -> b) -> a -> b
$ Proxy blk -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @blk)