Safe Haskell | None |
---|---|

Language | Haskell2010 |

Intended for qualified import

import Ouroboros.Consensus.HardFork.Combinator.Util.Match (Mismatch(..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Match as Match

## Synopsis

- data Mismatch :: (k -> Type ) -> (k -> Type ) -> [k] -> Type where
- flip :: Mismatch f g xs -> Mismatch g f xs
- matchNS :: NS f xs -> NS g xs -> Either ( Mismatch f g xs) ( NS ( Product f g) xs)
- matchTelescope :: NS h xs -> Telescope g f xs -> Either ( Mismatch h f xs) ( Telescope g ( Product h f) xs)
- mismatchNotEmpty :: Mismatch f g xs -> ( forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a
- mismatchNotFirst :: Mismatch f g (x ': xs) -> Either ( NS f xs) ( NS g xs)
- mismatchOne :: Mismatch f g '[x] -> Void
- mismatchToNS :: Mismatch f g xs -> ( NS f xs, NS g xs)
- mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x)
- mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y]
- mustMatchNS :: forall f g xs. HasCallStack => String -> NS f xs -> NS g xs -> NS ( Product f g) xs
- bihap :: NP (f -.-> f') xs -> NP (g -.-> g') xs -> Mismatch f g xs -> Mismatch f' g' xs
- 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
- bihmap :: SListI xs => ( forall x. f x -> f' x) -> ( forall x. g x -> g' x) -> Mismatch f g xs -> Mismatch f' g' xs

# Documentation

data Mismatch :: (k -> Type ) -> (k -> Type ) -> [k] -> Type where Source #

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

#### Instances

matchTelescope :: NS h xs -> Telescope g f xs -> Either ( Mismatch h f xs) ( Telescope g ( Product h f) xs) Source #

# Utilities

mismatchNotEmpty :: Mismatch f g xs -> ( forall x xs'. xs ~ (x ': xs') => Mismatch f g (x ': xs') -> a) -> a Source #

mismatchOne :: Mismatch f g '[x] -> Void Source #

We cannot give a mismatch if we have only one type variable

mismatchTwo :: Mismatch f g '[x, y] -> Either (f x, g y) (f y, g x) Source #

If we only have two eras, only two possibilities for a mismatch

mkMismatchTwo :: Either (f x, g y) (f y, g x) -> Mismatch f g '[x, y] Source #

mustMatchNS :: forall f g xs. HasCallStack => String -> NS f xs -> NS g xs -> NS ( Product f g) xs Source #