{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Intended for qualified import -- -- > import Data.SOP.Match (Mismatch(..)) -- > import qualified Data.SOP.Match as Match module Data.SOP.Match ( Mismatch (..) , flipMatch , matchNS , matchTelescope -- * Utilities , mismatchNotEmpty , mismatchNotFirst , mismatchOne , mismatchToNS , mismatchTwo , mkMismatchTwo , mustMatchNS -- * SOP operators , bihap , bihcmap , bihmap ) where import Data.Bifunctor import Data.Coerce (coerce) import Data.Constraint (Dict (..)) import Data.Functor.Product import Data.Kind (Type) import Data.Proxy import Data.SOP.Constraint import Data.SOP.Sing import Data.SOP.Strict import Data.SOP.Telescope (Telescope (..)) import qualified Data.SOP.Telescope as Telescope import Data.Void import GHC.Stack (HasCallStack) import NoThunks.Class (NoThunks (..), allNoThunks) import Prelude hiding (flip) {------------------------------------------------------------------------------- Main API -------------------------------------------------------------------------------} -- | We have a mismatch in the index between two NS type Mismatch :: (k -> Type) -> (k -> Type) -> [k] -> Type data Mismatch f g xs where -- | The left is at the current @x@ and the right is somewhere in the later -- @xs@ ML :: f x -> NS g xs -> Mismatch f g (x ': xs) -- | The right is at the current @x@ and the left is somewhere in the later -- @xs@ MR :: NS f xs -> g x -> Mismatch f g (x ': xs) -- | There is a mismatch later on in the @xs@ MS :: Mismatch f g xs -> Mismatch f g (x ': xs) flipMatch :: Mismatch f g xs -> Mismatch g f xs flipMatch :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]). Mismatch f g xs -> Mismatch g f xs flipMatch = 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]). 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 {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). 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 {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) 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 {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). 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 :: 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 -> 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 :: 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 (Z f x fx) (Z g x gx) = NS (Product f g) xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. b -> Either a b Right (Product f g x -> NS (Product f g) (x : xs1) forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) 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 xs1 l) (S NS g xs1 r) = (Mismatch f g xs1 -> Mismatch f g xs) -> (NS (Product f g) xs1 -> NS (Product f g) xs) -> Either (Mismatch f g xs1) (NS (Product f g) xs1) -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap Mismatch f g xs1 -> Mismatch f g xs Mismatch f g xs1 -> Mismatch f g (x : xs1) forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). Mismatch f g xs -> Mismatch f g (x : xs) MS NS (Product f g) xs1 -> NS (Product f g) xs NS (Product f g) xs1 -> NS (Product f g) (x : xs1) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S (Either (Mismatch f g xs1) (NS (Product f g) xs1) -> Either (Mismatch f g xs) (NS (Product f g) xs)) -> Either (Mismatch f g xs1) (NS (Product f g) xs1) -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. (a -> b) -> a -> b $ NS f xs1 -> NS g xs1 -> Either (Mismatch f g xs1) (NS (Product f g) xs1) 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 xs1 l NS g xs1 NS g xs1 r go (Z f x fx) (S NS g xs1 r) = Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. a -> Either a b Left (Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)) -> Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. (a -> b) -> a -> b $ f x -> NS g xs1 -> Mismatch f g (x : xs1) forall {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) ML f x fx NS g xs1 r go (S NS f xs1 l) (Z g x gx) = Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. a -> Either a b Left (Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs)) -> Mismatch f g xs -> Either (Mismatch f g xs) (NS (Product f g) xs) forall a b. (a -> b) -> a -> b $ NS f xs1 -> g x -> Mismatch f g (x : xs1) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). NS f xs -> g x -> Mismatch f g (x : xs) MR NS f xs1 l g x gx matchTelescope :: NS h xs -> Telescope g f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) matchTelescope :: 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) 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 :: 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 (Z h x l) (TZ f x fx) = Telescope g (Product h f) xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. b -> Either a b Right (Product h f x -> Telescope g (Product h f) (x : xs1) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs1 :: [k]). f x -> Telescope g f (x : xs1) 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 xs1 r) (TS g x gx Telescope g f xs1 t) = (Mismatch h f xs1 -> Mismatch h f xs) -> (Telescope g (Product h f) xs1 -> Telescope g (Product h f) xs) -> Either (Mismatch h f xs1) (Telescope g (Product h f) xs1) -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap Mismatch h f xs1 -> Mismatch h f xs Mismatch h f xs1 -> Mismatch h f (x : xs1) forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). Mismatch f g xs -> Mismatch f g (x : xs) MS (g x -> Telescope g (Product h f) xs1 -> Telescope g (Product h f) (x : xs1) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs1 :: [k]). g x -> Telescope g f xs1 -> Telescope g f (x : xs1) TS g x gx) (Either (Mismatch h f xs1) (Telescope g (Product h f) xs1) -> Either (Mismatch h f xs) (Telescope g (Product h f) xs)) -> Either (Mismatch h f xs1) (Telescope g (Product h f) xs1) -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. (a -> b) -> a -> b $ NS h xs1 -> Telescope g f xs1 -> Either (Mismatch h f xs1) (Telescope g (Product h f) xs1) 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 xs1 r Telescope g f xs1 Telescope g f xs1 t go (Z h x hx) (TS g x _gx Telescope g f xs1 t) = Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. a -> Either a b Left (Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs)) -> Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. (a -> b) -> a -> b $ h x -> NS f xs1 -> Mismatch h f (x : xs1) forall {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) ML h x hx (Telescope g f xs1 -> NS f xs1 forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs Telescope.tip Telescope g f xs1 t) go (S NS h xs1 l) (TZ f x fx) = Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. a -> Either a b Left (Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs)) -> Mismatch h f xs -> Either (Mismatch h f xs) (Telescope g (Product h f) xs) forall a b. (a -> b) -> a -> b $ NS h xs1 -> f x -> Mismatch h f (x : xs1) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). NS f xs -> g x -> Mismatch f g (x : xs) MR NS h xs1 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 :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]). 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 NP (f -.-> g) xs -> Mismatch f f xs -> Mismatch f g xs forall (g :: k -> *) (g' :: k -> *) (xs :: [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 :: forall (g :: k -> *) (g' :: k -> *) (xs :: [k]). NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go ((-.->) g g' x _ :* NP (g -.-> g') xs1 fs) (MS Mismatch f g xs m) = Mismatch f g' xs1 -> Mismatch f g' (x : xs1) forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). Mismatch f g xs -> Mismatch f g (x : xs) MS (NP (g -.-> g') xs1 -> Mismatch f g xs1 -> Mismatch f g' xs1 forall (g :: k -> *) (g' :: k -> *) (xs :: [k]). NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f g' xs go NP (g -.-> g') xs1 fs Mismatch f g xs1 Mismatch f g xs m) go ((-.->) g g' x _ :* NP (g -.-> g') xs1 fs) (ML f x fx NS g xs gy) = f x -> NS g' xs -> Mismatch f g' (x : xs) forall {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) 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 forall (f :: k -> *) (g :: k -> *) (xs :: [k]). Prod NS (f -.-> g) xs -> NS f xs -> NS g xs hap Prod NS (g -.-> g') xs NP (g -.-> g') xs1 fs NS g xs gy) go ((-.->) g g' x f :* NP (g -.-> g') xs1 _) (MR NS f xs fy g x gx) = NS f xs -> g' x -> Mismatch f g' (x : xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). 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 {} type instance Same (Mismatch f) = Mismatch f instance (forall x y. LiftedCoercible p p x y) => HTrans (Mismatch p) (Mismatch p) where htrans :: forall proxy c f g xs ys. AllZipN (Prod (Mismatch p)) c xs ys => proxy c -> (forall x y. c x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g ys htrans :: forall (proxy :: (k2 -> k2 -> Constraint) -> *) (c :: k2 -> k2 -> Constraint) (f :: k2 -> *) (g :: k2 -> *) (xs :: [k2]) (ys :: [k2]). AllZipN (Prod (Mismatch p)) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g ys htrans proxy c p forall (x :: k2) (y :: k2). c x y => f x -> g y t = \case ML p x fx NS f xs gy -> p (Head ys) -> NS g (Tail ys) -> Mismatch p g (Head ys : Tail ys) forall {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) ML (p x -> p (Head ys) forall a b. Coercible a b => a -> b coerce p x fx) (NS g (Tail ys) -> Mismatch p g (Head ys : Tail ys)) -> NS g (Tail ys) -> Mismatch p g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g (Tail ys) forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint) (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> h1 f xs -> h2 g ys forall (c :: k2 -> k2 -> Constraint) (xs :: [k2]) (ys :: [k2]) (proxy :: (k2 -> k2 -> Constraint) -> *) (f :: k2 -> *) (g :: k2 -> *). AllZipN (Prod NS) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g ys htrans proxy c p f x -> g y forall (x :: k2) (y :: k2). c x y => f x -> g y t NS f xs gy MR NS p xs fy f x gx | Dict (AllZip (LiftedCoercible p p) (Tail xs) (Tail ys)) Dict <- Dict (AllZip (LiftedCoercible p p) (Tail xs) (Tail ys)) tailDict -> NS p (Tail ys) -> g (Head ys) -> Mismatch p g (Head ys : Tail ys) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). NS f xs -> g x -> Mismatch f g (x : xs) MR (NS p xs -> NS p (Tail ys) forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (f :: k1 -> *) (g :: k2 -> *) (xs :: l1) (ys :: l2). (HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) => h1 f xs -> h2 g ys forall (f :: k2 -> *) (g :: k2 -> *) (xs :: [k2]) (ys :: [k2]). AllZipN (Prod NS) (LiftedCoercible f g) xs ys => NS f xs -> NS g ys hcoerce NS p xs fy) (g (Head ys) -> Mismatch p g (Head ys : Tail ys)) -> g (Head ys) -> Mismatch p g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ f x -> g (Head ys) forall (x :: k2) (y :: k2). c x y => f x -> g y t f x gx where tailDict :: Dict (AllZip (LiftedCoercible p p) (Tail xs) (Tail ys)) tailDict :: Dict (AllZip (LiftedCoercible p p) (Tail xs) (Tail ys)) tailDict = Proxy c -> Dict (AllZip (LiftedCoercible p p) xs (Tail ys)) forall {a} {b} (c :: a -> b -> Constraint) (c' :: a -> b -> Constraint) (xs :: [a]) (ys :: [b]). (AllZip c xs ys, forall (x :: a) (y :: b). c x y => c' x y) => Proxy c -> Dict (AllZip c' xs ys) impliesAllZip (forall {k} (t :: k). Proxy t forall (t :: k2 -> k2 -> Constraint). Proxy t Proxy @c) MS Mismatch p f xs m -> Mismatch p g (Tail ys) -> Mismatch p g (Head ys : Tail ys) forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). Mismatch f g xs -> Mismatch f g (x : xs) MS (Mismatch p g (Tail ys) -> Mismatch p g (Head ys : Tail ys)) -> Mismatch p g (Tail ys) -> Mismatch p g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g (Tail ys) forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint) (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> h1 f xs -> h2 g ys forall (c :: k2 -> k2 -> Constraint) (xs :: [k2]) (ys :: [k2]) (proxy :: (k2 -> k2 -> Constraint) -> *) (f :: k2 -> *) (g :: k2 -> *). AllZipN (Prod (Mismatch p)) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g ys htrans proxy c p f x -> g y forall (x :: k2) (y :: k2). c x y => f x -> g y t Mismatch p f xs m -- NOTE(jdral): this code could be replaced by 'unsafeCoerce' (see 'trans_NP' -- or 'trans_NS' for examples), but this would technically sacrifice type -- safety. For now, this version should be sufficient. hcoerce :: forall f g xs ys. AllZipN (Prod (Mismatch p)) (LiftedCoercible f g) xs ys => Mismatch p f xs -> Mismatch p g ys hcoerce :: forall (f :: k2 -> *) (g :: k2 -> *) (xs :: [k2]) (ys :: [k2]). AllZipN (Prod (Mismatch p)) (LiftedCoercible f g) xs ys => Mismatch p f xs -> Mismatch p g ys hcoerce = Proxy (LiftedCoercible f g) -> (forall (x :: k2) (y :: k2). LiftedCoercible f g x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g ys forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint) (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> h1 f xs -> h2 g ys forall (c :: k2 -> k2 -> Constraint) (xs :: [k2]) (ys :: [k2]) (proxy :: (k2 -> k2 -> Constraint) -> *) (f :: k2 -> *) (g :: k2 -> *). AllZipN (Prod (Mismatch p)) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Mismatch p f xs -> Mismatch p g ys htrans (forall {k} (t :: k). Proxy t forall (t :: k2 -> k2 -> Constraint). Proxy t Proxy @(LiftedCoercible f g)) f x -> g y forall (x :: k2) (y :: k2). LiftedCoercible f g x y => f x -> g y forall a b. Coercible a b => a -> b coerce impliesAllZip :: forall c c' xs ys. (AllZip c xs ys, forall x y. c x y => c' x y) => Proxy c -> Dict (AllZip c' xs ys) impliesAllZip :: forall {a} {b} (c :: a -> b -> Constraint) (c' :: a -> b -> Constraint) (xs :: [a]) (ys :: [b]). (AllZip c xs ys, forall (x :: a) (y :: b). c x y => c' x y) => Proxy c -> Dict (AllZip c' xs ys) impliesAllZip Proxy c _ = SList xs -> SList ys -> Dict (AllZip c' xs ys) forall (as :: [a]) (bs :: [b]). AllZip c as bs => SList as -> SList bs -> Dict (AllZip c' as bs) go SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList SList ys forall {k} (xs :: [k]). SListI xs => SList xs sList where go :: forall as bs. AllZip c as bs => SList as -> SList bs -> Dict (AllZip c' as bs) go :: forall (as :: [a]) (bs :: [b]). AllZip c as bs => SList as -> SList bs -> Dict (AllZip c' as bs) go SList as SNil SList bs SNil = Dict (AllZip c' as bs) forall (a :: Constraint). a => Dict a Dict go SList as SCons SList bs SCons = case SList xs -> SList (Tail bs) -> Dict (AllZip c' xs (Tail bs)) forall (as :: [a]) (bs :: [b]). AllZip c as bs => SList as -> SList bs -> Dict (AllZip c' as bs) go (forall (xs :: [a]). SListI xs => SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList @(Tail as)) (forall (xs :: [b]). SListI xs => SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList @(Tail bs)) of Dict (AllZip c' xs (Tail bs)) Dict -> Dict (AllZip c' as bs) forall (a :: Constraint). a => Dict a Dict {------------------------------------------------------------------------------- Utilities -------------------------------------------------------------------------------} -- | We cannot give a mismatch if we have only one type variable mismatchOne :: Mismatch f g '[x] -> Void mismatchOne :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k). 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 :: forall {k} (f :: k -> *). 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 :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k) (y :: k). 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 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 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 :: forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (y :: k). 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 {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) ML f x fx (g y -> NS g '[y] forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z g y gy) mkMismatchTwo (Right (f y fy, g x gx)) = NS f '[y] -> g x -> Mismatch f g '[x, y] forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). NS f xs -> g x -> Mismatch f g (x : xs) MR (f y -> NS f '[y] forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]). 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]). 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z f x fx, NS g xs -> NS g (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S NS g xs gy) go (MR NS f xs fy g x gx) = (NS f xs -> NS f (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S NS f xs fy, g x -> NS g (x : xs) forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z g x gx) go (MS Mismatch f g xs m) = (NS f xs -> NS f xs) -> (NS g xs -> NS g xs) -> (NS f xs, NS g xs) -> (NS f xs, NS g xs) forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap NS f xs -> NS f xs NS f xs -> NS f (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S NS g xs -> NS g xs NS g xs -> NS g (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S ((NS f xs, NS g xs) -> (NS f xs, NS g xs)) -> (NS f xs, NS g xs) -> (NS f xs, NS g 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 :: 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 -> (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 :: 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 (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 {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) 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 {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). 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 {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). Mismatch f g xs -> Mismatch f g (x : xs) MS) mismatchNotFirst :: Mismatch f g (x ': xs) -> Either (NS f xs) (NS g xs) mismatchNotFirst :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). 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 :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k) (xs :: [k]). 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' 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' 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 xs') -> (NS g xs' -> NS g xs') -> Either (NS f xs') (NS g xs') -> Either (NS f xs') (NS g xs') forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap NS f xs' -> NS f xs' NS f xs' -> NS f (x : xs') forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S NS g xs' -> NS g xs' NS g xs' -> NS g (x : xs') forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S (Either (NS f xs') (NS g xs') -> Either (NS f xs') (NS g 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') -> 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 :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]). HasCallStack => 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 :: 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 = \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 :: 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 (ML f x fx NS g xs r) ((-.->) f f' x f :* NP (f -.-> f') xs1 _) ((-.->) g g' x _ :* NP (g -.-> g') xs1 gs) = f' x -> NS g' xs -> Mismatch f' g' (x : xs) forall {k} (f :: k -> *) (xs :: k) (g :: k -> *) (x :: [k]). f xs -> NS g x -> Mismatch f g (xs : x) 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 forall (f :: k -> *) (g :: k -> *) (xs :: [k]). Prod NS (f -.-> g) xs -> NS f xs -> NS g xs hap Prod NS (g -.-> g') xs NP (g -.-> g') xs1 gs NS g xs r) go (MR NS f xs l g x gx) ((-.->) f f' x _ :* NP (f -.-> f') xs1 fs) ((-.->) g g' x g :* NP (g -.-> g') xs1 _) = NS f' xs -> g' x -> Mismatch f' g' (x : xs) forall {k} (f :: k -> *) (xs :: [k]) (g :: k -> *) (x :: k). 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 forall (f :: k -> *) (g :: k -> *) (xs :: [k]). Prod NS (f -.-> g) xs -> NS f xs -> NS g xs hap Prod NS (f -.-> f') xs NP (f -.-> f') xs1 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') xs1 fs) ((-.->) g g' x _ :* NP (g -.-> g') xs1 gs) = Mismatch f' g' xs -> Mismatch f' g' (x : xs) forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (x :: k). 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') xs1 fs NP (g -.-> g') xs NP (g -.-> g') xs1 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 {k} (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: k -> *) (g' :: k -> *). SListI xs => (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 (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). 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 :: 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 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 forall (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). AllN NP c xs => proxy c -> (forall (a :: k). c a => f a) -> NP 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 forall (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). AllN NP c xs => proxy c -> (forall (a :: k). c a => f a) -> NP 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