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

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