{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Intended for qualified import -- -- > import Ouroboros.Consensus.HardFork.Combinator.Util.Match (Mismatch(..)) -- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match module Ouroboros.Consensus.HardFork.Combinator.Util.Match ( Mismatch (..) , flip , matchNS , matchTelescope -- * Utilities , mismatchNotEmpty , mismatchNotFirst , mismatchOne , mismatchToNS , mismatchTwo , mkMismatchTwo , mustMatchNS -- * SOP operators , bihap , bihcmap , bihmap ) where import Prelude hiding (flip) import Data.Bifunctor import Data.Functor.Product import Data.Kind (Type) import Data.SOP.Strict import Data.Void import GHC.Stack (HasCallStack) import NoThunks.Class (NoThunks (..), allNoThunks) import Ouroboros.Consensus.Util.SOP () import Ouroboros.Consensus.HardFork.Combinator.Util.Telescope (Telescope (..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope {------------------------------------------------------------------------------- Main API -------------------------------------------------------------------------------} data Mismatch :: (k -> Type) -> (k -> Type) -> [k] -> Type where ML :: f x -> NS g xs -> Mismatch f g (x ': xs) MR :: NS f xs -> g x -> Mismatch f g (x ': xs) MS :: Mismatch f g xs -> Mismatch f g (x ': xs) flip :: Mismatch f g xs -> Mismatch g f xs flip :: Mismatch f g xs -> Mismatch g f xs flip = Mismatch f g xs -> Mismatch g f xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Mismatch f g xs -> Mismatch g f xs go where go :: Mismatch f g xs -> Mismatch g f xs go :: Mismatch f g xs -> Mismatch g f xs go (ML f x fx NS g xs gy) = NS g xs -> f x -> Mismatch g f (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR NS g xs gy f x fx go (MR NS f xs fy g x gx) = g x -> NS f xs -> Mismatch g f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML g x gx NS f xs fy go (MS Mismatch f g xs m) = Mismatch g f xs -> Mismatch g f (x : xs) forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS (Mismatch f g xs -> Mismatch g f xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Mismatch f g xs -> Mismatch g f xs go Mismatch f g xs m) matchNS :: NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) matchNS :: NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) matchNS = NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall k (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) go where go :: NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) go :: NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) go (Z f x fx) (Z g x gx) = NS (Product f g) (x : xs) -> Either (Mismatch f g xs) (NS (Product f g) (x : xs)) forall a b. b -> Either a b Right (Product f g x -> NS (Product f g) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f x -> g x -> Product f g x forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair f x fx g x g x gx)) go (S NS f xs l) (S NS g xs r) = (Mismatch f g xs -> Mismatch f g (x : xs)) -> (NS (Product f g) xs -> NS (Product f g) (x : xs)) -> Either (Mismatch f g xs) (NS (Product f g) xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) (x : xs)) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap Mismatch f g xs -> Mismatch f g (x : xs) forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS NS (Product f g) xs -> NS (Product f g) (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (Either (Mismatch f g xs) (NS (Product f g) xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) (x : xs))) -> Either (Mismatch f g xs) (NS (Product f g) xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) (x : xs)) forall a b. (a -> b) -> a -> b $ NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall k (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) go NS f xs l NS g xs NS g xs r go (Z f x fx) (S NS g xs r) = Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs) forall a b. a -> Either a b Left (Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs)) -> Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs) forall a b. (a -> b) -> a -> b $ f x -> NS g xs -> Mismatch f g (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML f x fx NS g xs r go (S NS f xs l) (Z g x gx) = Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs) forall a b. a -> Either a b Left (Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs)) -> Mismatch f g (x : xs) -> Either (Mismatch f g (x : xs)) (NS (Product f g) xs) forall a b. (a -> b) -> a -> b $ NS f xs -> g x -> Mismatch f g (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR NS f xs l g x gx matchTelescope :: NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) matchTelescope :: NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) matchTelescope = NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall k (h :: k -> *) (xs :: [k]) (g :: k -> *) (f :: k -> *). NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) go where go :: NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) go :: NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) go (Z h x l) (TZ f x fx) = Telescope g (Product h f) (x : xs) -> Either (Mismatch h f xs) (Telescope g (Product h f) (x : xs)) forall a b. b -> Either a b Right (Product h f x -> Telescope g (Product h f) (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (h x -> f x -> Product h f x forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair h x l f x f x fx)) go (S NS h xs r) (TS g x gx Telescope g f xs t) = (Mismatch h f xs -> Mismatch h f (x : xs)) -> (Telescope g (Product h f) xs -> Telescope g (Product h f) (x : xs)) -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) (x : xs)) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap Mismatch h f xs -> Mismatch h f (x : xs) forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS (g x -> Telescope g (Product h f) xs -> Telescope g (Product h f) (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx) (Either (Mismatch h f xs) (Telescope g (Product h f) xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) (x : xs))) -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) (x : xs)) forall a b. (a -> b) -> a -> b $ NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall k (h :: k -> *) (xs :: [k]) (g :: k -> *) (f :: k -> *). NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) go NS h xs r Telescope g f xs Telescope g f xs t go (Z h x hx) (TS g x _gx Telescope g f xs t) = Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs) forall a b. a -> Either a b Left (Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs)) -> Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs) forall a b. (a -> b) -> a -> b $ h x -> NS f xs -> Mismatch h f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML h x hx (Telescope g f xs -> NS f xs forall k (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs Telescope.tip Telescope g f xs t) go (S NS h xs l) (TZ f x fx) = Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs) forall a b. a -> Either a b Left (Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs)) -> Mismatch h f (x : xs) -> Either (Mismatch h f (x : xs)) (Telescope g (Product h f) xs) forall a b. (a -> b) -> a -> b $ NS h xs -> f x -> Mismatch h f (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR NS h xs l f x fx {------------------------------------------------------------------------------- SOP class instances for 'Mismatch' -------------------------------------------------------------------------------} type instance Prod (Mismatch f) = NP type instance SListIN (Mismatch f) = SListI type instance AllN (Mismatch f) c = All c instance HAp (Mismatch f) where hap :: Prod (Mismatch f) (f -.-> g) xs -> Mismatch f f xs -> Mismatch f g xs hap = Prod (Mismatch f) (f -.-> g) xs -> Mismatch f f xs -> Mismatch f g xs forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *). NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go where go :: NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go :: NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go ((-.->) g g' x _ :* NP (g -.-> g') xs fs) (MS Mismatch f g xs m) = Mismatch f g' xs -> Mismatch f g' (x : xs) forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS (NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs forall k (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *). NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go NP (g -.-> g') xs fs Mismatch f g xs Mismatch f g xs m) go ((-.->) g g' x _ :* NP (g -.-> g') xs fs) (ML f x fx NS g xs gy) = f x -> NS g' xs -> Mismatch f g' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML f x fx (Prod NS (g -.-> g') xs -> NS g xs -> NS g' xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs hap Prod NS (g -.-> g') xs NP (g -.-> g') xs fs NS g xs gy) go ((-.->) g g' x f :* NP (g -.-> g') xs _) (MR NS f xs fy g x gx) = NS f xs -> g' x -> Mismatch f g' (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR NS f xs fy ((-.->) g g' x -> g x -> g' x forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) g g' x f g x g x gx) go NP (g -.-> g') xs Nil Mismatch f g xs m = case Mismatch f g xs m of {} {------------------------------------------------------------------------------- Utilities -------------------------------------------------------------------------------} -- | We cannot give a mismatch if we have only one type variable mismatchOne :: Mismatch f g '[x] -> Void mismatchOne :: Mismatch f g '[x] -> Void mismatchOne = (NS f '[] -> Void) -> (NS g '[] -> Void) -> Either (NS f '[]) (NS g '[]) -> Void forall a c b. (a -> c) -> (b -> c) -> Either a b -> c either NS f '[] -> Void forall k (f :: k -> *). NS f '[] -> Void aux NS g '[] -> Void forall k (f :: k -> *). NS f '[] -> Void aux (Either (NS f '[]) (NS g '[]) -> Void) -> (Mismatch f g '[x] -> Either (NS f '[]) (NS g '[])) -> Mismatch f g '[x] -> Void forall b c a. (b -> c) -> (a -> b) -> a -> c . Mismatch f g '[x] -> Either (NS f '[]) (NS g '[]) forall k (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) mismatchNotFirst where aux :: NS f '[] -> Void aux :: NS f '[] -> Void aux NS f '[] ns = case NS f '[] ns of {} -- | If we only have two eras, only two possibilities for a mismatch mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x) mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x) mismatchTwo (ML f x fx NS g xs gy) = (f x, g y) -> Either (f x, g y) (f y, g x) forall a b. a -> Either a b Left (f x fx, NS g '[y] -> g y forall k (f :: k -> *) (x :: k). NS f '[x] -> f x unZ NS g xs NS g '[y] gy) mismatchTwo (MR NS f xs fy g x gx) = (f y, g x) -> Either (f x, g y) (f y, g x) forall a b. b -> Either a b Right (NS f '[y] -> f y forall k (f :: k -> *) (x :: k). NS f '[x] -> f x unZ NS f xs NS f '[y] fy, g x gx) mismatchTwo (MS Mismatch f g xs m) = Void -> Either (f x, g y) (f y, g x) forall a. Void -> a absurd (Void -> Either (f x, g y) (f y, g x)) -> Void -> Either (f x, g y) (f y, g x) forall a b. (a -> b) -> a -> b $ Mismatch f g '[y] -> Void forall k (f :: k -> *) (g :: k -> *) (x :: k). Mismatch f g '[x] -> Void mismatchOne Mismatch f g xs Mismatch f g '[y] m mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y] mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y] mkMismatchTwo (Left (f x fx, g y gy)) = f x -> NS g '[y] -> Mismatch f g '[x, y] forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML f x fx (g y -> NS g '[y] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z g y gy) mkMismatchTwo (Right (f y fy, g x gx)) = NS f '[y] -> g x -> Mismatch f g '[x, y] forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR (f y -> NS f '[y] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z f y fy) g x gx -- | Project two 'NS' from a 'Mismatch' -- -- We should have the property that -- -- > uncurry matchNS (mismatchToNS m) == Left m mismatchToNS :: Mismatch f g xs -> (NS f xs, NS g xs) mismatchToNS :: Mismatch f g xs -> (NS f xs, NS g xs) mismatchToNS = Mismatch f g xs -> (NS f xs, NS g xs) forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Mismatch f g xs -> (NS f xs, NS g xs) go where go :: Mismatch f g xs -> (NS f xs, NS g xs) go :: Mismatch f g xs -> (NS f xs, NS g xs) go (ML f x fx NS g xs gy) = (f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z f x fx, NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S NS g xs gy) go (MR NS f xs fy g x gx) = (NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S NS f xs fy, g x -> NS g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z g x gx) go (MS Mismatch f g xs m) = (NS f xs -> NS f (x : xs)) -> (NS g xs -> NS g (x : xs)) -> (NS f xs, NS g xs) -> (NS f (x : xs), NS g (x : xs)) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S ((NS f xs, NS g xs) -> (NS f (x : xs), NS g (x : xs))) -> (NS f xs, NS g xs) -> (NS f (x : xs), NS g (x : xs)) forall a b. (a -> b) -> a -> b $ Mismatch f g xs -> (NS f xs, NS g xs) forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). Mismatch f g xs -> (NS f xs, NS g xs) go Mismatch f g xs m mismatchNotEmpty :: Mismatch f g xs -> (forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a mismatchNotEmpty :: Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a mismatchNotEmpty = Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) a. Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a go where go :: Mismatch f g xs -> (forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a go :: Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a go (ML f x fx NS g xs gy) forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k = Mismatch f g (x : xs) -> a forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k (f x -> NS g xs -> Mismatch f g (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML f x fx NS g xs gy) go (MR NS f xs fy g x gx) forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k = Mismatch f g (x : xs) -> a forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k (NS f xs -> g x -> Mismatch f g (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR NS f xs fy g x gx) go (MS Mismatch f g xs m) forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k = Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) a. Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a go Mismatch f g xs m (Mismatch f g (x : x : xs') -> a forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a k (Mismatch f g (x : x : xs') -> a) -> (Mismatch f g (x : xs') -> Mismatch f g (x : x : xs')) -> Mismatch f g (x : xs') -> a forall b c a. (b -> c) -> (a -> b) -> a -> c . Mismatch f g (x : xs') -> Mismatch f g (x : x : xs') forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS) mismatchNotFirst :: Mismatch f g (x ': xs) -> Either (NS f xs) (NS g xs) mismatchNotFirst :: Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) mismatchNotFirst = Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) forall k (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) go where go :: Mismatch f g (x' ': xs') -> Either (NS f xs') (NS g xs') go :: Mismatch f g (x' : xs') -> Either (NS f xs') (NS g xs') go (ML f x _ NS g xs gy) = NS g xs -> Either (NS f xs') (NS g xs) forall a b. b -> Either a b Right NS g xs gy go (MR NS f xs fy g x _ ) = NS f xs -> Either (NS f xs) (NS g xs') forall a b. a -> Either a b Left NS f xs fy go (MS Mismatch f g xs m) = Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> Either (NS f xs') (NS g xs')) -> Either (NS f xs') (NS g xs') forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) a. Mismatch f g xs -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> a) -> a mismatchNotEmpty Mismatch f g xs m ((forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> Either (NS f xs') (NS g xs')) -> Either (NS f xs') (NS g xs')) -> (forall (x :: k) (xs' :: [k]). (xs ~ (x : xs')) => Mismatch f g (x : xs') -> Either (NS f xs') (NS g xs')) -> Either (NS f xs') (NS g xs') forall a b. (a -> b) -> a -> b $ \Mismatch f g (x : xs') m' -> (NS f xs' -> NS f (x : xs')) -> (NS g xs' -> NS g (x : xs')) -> Either (NS f xs') (NS g xs') -> Either (NS f (x : xs')) (NS g (x : xs')) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap NS f xs' -> NS f (x : xs') forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S NS g xs' -> NS g (x : xs') forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (Either (NS f xs') (NS g xs') -> Either (NS f (x : xs')) (NS g (x : xs'))) -> Either (NS f xs') (NS g xs') -> Either (NS f (x : xs')) (NS g (x : xs')) forall a b. (a -> b) -> a -> b $ Mismatch f g (x : xs') -> Either (NS f xs') (NS g xs') forall k (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). Mismatch f g (x : xs) -> Either (NS f xs) (NS g xs) go Mismatch f g (x : xs') m' -- | Variant of 'matchNS' for when we know the two 'NS's must match. Otherwise -- an error, mentioning the given 'String', is thrown. mustMatchNS :: forall f g xs. HasCallStack => String -> NS f xs -> NS g xs -> NS (Product f g) xs mustMatchNS :: String -> NS f xs -> NS g xs -> NS (Product f g) xs mustMatchNS String lbl NS f xs f NS g xs g = case NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall k (f :: k -> *) (xs :: [k]) (g :: k -> *). NS f xs -> NS g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) matchNS NS f xs f NS g xs g of Left Mismatch f g xs _mismatch -> String -> NS (Product f g) xs forall a. HasCallStack => String -> a error (String -> NS (Product f g) xs) -> String -> NS (Product f g) xs forall a b. (a -> b) -> a -> b $ String lbl String -> String -> String forall a. Semigroup a => a -> a -> a <> String " from wrong era" Right NS (Product f g) xs matched -> NS (Product f g) xs matched {------------------------------------------------------------------------------- Subset of the (generalized) SOP operators -------------------------------------------------------------------------------} bihap :: NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs bihap :: NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs bihap = \NP (f -.-> f') xs gs NP (g -.-> g') xs fs Mismatch f g xs t -> Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (f' :: k -> *) (g' :: k -> *). Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs go Mismatch f g xs t NP (f -.-> f') xs gs NP (g -.-> g') xs fs where go :: Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs go :: Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs go (ML f x fx NS g xs r) ((-.->) f f' x f :* NP (f -.-> f') xs _) ((-.->) g g' x _ :* NP (g -.-> g') xs gs) = f' x -> NS g' xs -> Mismatch f' g' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> NS g xs -> Mismatch f g (x : xs) ML ((-.->) f f' x -> f x -> f' x forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f f' x f f x f x fx) (Prod NS (g -.-> g') xs -> NS g xs -> NS g' xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs hap Prod NS (g -.-> g') xs NP (g -.-> g') xs gs NS g xs r) go (MR NS f xs l g x gx) ((-.->) f f' x _ :* NP (f -.-> f') xs fs) ((-.->) g g' x g :* NP (g -.-> g') xs _) = NS f' xs -> g' x -> Mismatch f' g' (x : xs) forall a (f :: a -> *) (xs :: [a]) (g :: a -> *) (x :: a). NS f xs -> g x -> Mismatch f g (x : xs) MR (Prod NS (f -.-> f') xs -> NS f xs -> NS f' xs forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *) (xs :: l). HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs hap Prod NS (f -.-> f') xs NP (f -.-> f') xs fs NS f xs l) ((-.->) g g' x -> g x -> g' x forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) g g' x g g x g x gx) go (MS Mismatch f g xs m) ((-.->) f f' x _ :* NP (f -.-> f') xs fs) ((-.->) g g' x _ :* NP (g -.-> g') xs gs) = Mismatch f' g' xs -> Mismatch f' g' (x : xs) forall a (f :: a -> *) (g :: a -> *) (xs :: [a]) (x :: a). Mismatch f g xs -> Mismatch f g (x : xs) MS (Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (f' :: k -> *) (g' :: k -> *). Mismatch f g xs -> NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f' g' xs go Mismatch f g xs m NP (f -.-> f') xs NP (f -.-> f') xs fs NP (g -.-> g') xs NP (g -.-> g') xs gs) bihmap :: SListI xs => (forall x. f x -> f' x) -> (forall x. g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs bihmap :: (forall (x :: k). f x -> f' x) -> (forall (x :: k). g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs bihmap = Proxy Top -> (forall (x :: k). Top x => f x -> f' x) -> (forall (x :: k). Top x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs forall k (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *) (g :: k -> *) (g' :: k -> *). All c xs => proxy c -> (forall (x :: k). c x => f x -> f' x) -> (forall (x :: k). c x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs bihcmap (Proxy Top forall k (t :: k). Proxy t Proxy @Top) -- | Bifunctor analogue of 'hcmap' bihcmap :: All c xs => proxy c -> (forall x. c x => f x -> f' x) -> (forall x. c x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs bihcmap :: proxy c -> (forall (x :: k). c x => f x -> f' x) -> (forall (x :: k). c x => g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs bihcmap proxy c p forall (x :: k). c x => f x -> f' x g forall (x :: k). c x => g x -> g' x f = NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs forall k (f :: k -> *) (f' :: k -> *) (xs :: [k]) (g :: k -> *) (g' :: k -> *). NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs bihap (proxy c -> (forall (a :: k). c a => (-.->) f f' a) -> NP (f -.-> f') xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((f a -> f' a) -> (-.->) f f' a forall k (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn f a -> f' a forall (x :: k). c x => f x -> f' x g)) (proxy c -> (forall (a :: k). c a => (-.->) g g' a) -> NP (g -.-> g') xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p ((g a -> g' a) -> (-.->) g g' a forall k (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn g a -> g' a forall (x :: k). c x => g x -> g' x f)) {------------------------------------------------------------------------------- Standard type class instances -------------------------------------------------------------------------------} deriving stock instance ( All (Compose Eq f) xs , All (Compose Eq g) xs ) => Eq (Mismatch f g xs) deriving stock instance ( All (Compose Eq f) xs , All (Compose Ord f) xs , All (Compose Eq g) xs , All (Compose Ord g) xs ) => Ord (Mismatch f g xs) deriving stock instance ( All (Compose Show f) xs , All (Compose Show g) xs ) => Show (Mismatch f g xs) instance ( All (Compose NoThunks f) xs , All (Compose NoThunks g) xs ) => NoThunks (Mismatch f g xs) where showTypeOf :: Proxy (Mismatch f g xs) -> String showTypeOf Proxy (Mismatch f g xs) _ = String "Mismatch" wNoThunks :: Context -> Mismatch f g xs -> IO (Maybe ThunkInfo) wNoThunks Context ctxt = \case ML f x l NS g xs r -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo) allNoThunks [ Context -> f x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "l" String -> Context -> Context forall a. a -> [a] -> [a] : String "ML" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) f x l , Context -> NS g xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "r" String -> Context -> Context forall a. a -> [a] -> [a] : String "ML" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) NS g xs r ] MR NS f xs l g x r -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo) allNoThunks [ Context -> NS f xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "l" String -> Context -> Context forall a. a -> [a] -> [a] : String "MR" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) NS f xs l , Context -> g x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "r" String -> Context -> Context forall a. a -> [a] -> [a] : String "MR" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) g x r ] MS Mismatch f g xs m -> Context -> Mismatch f g xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "MS" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) Mismatch f g xs m