{-# 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)