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