Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Intended for qualified import
import Data.SOP.Match (Mismatch(..)) import qualified Data.SOP.Match as Match
Synopsis
- data Mismatch f g xs where
- flipMatch ∷ 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 → (∀ 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 ∷ ∀ 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 → (∀ x. c x ⇒ f x → f' x) → (∀ x. c x ⇒ g x → g' x) → Mismatch f g xs → Mismatch f' g' xs
- bihmap ∷ SListI xs ⇒ (∀ x. f x → f' x) → (∀ x. g x → g' x) → Mismatch f g xs → Mismatch f' g' xs
Documentation
data Mismatch f g xs where Source #
We have a mismatch in the index between two NS
ML ∷ f x → NS g xs → Mismatch f g (x ': xs) | The left is at the current |
MR ∷ NS f xs → g x → Mismatch f g (x ': xs) | The right is at the current |
MS ∷ Mismatch f g xs → Mismatch f g (x ': xs) | There is a mismatch later on in the |
Instances
(∀ (x ∷ k2) (y ∷ k2). LiftedCoercible p p x y) ⇒ HTrans (Mismatch p ∷ (k2 → Type) → [k2] → Type) (Mismatch p ∷ (k2 → Type) → [k2] → Type) Source # | |
Defined in Data.SOP.Match htrans ∷ ∀ c (xs ∷ l1) (ys ∷ l2) proxy f g. AllZipN (Prod (Mismatch p)) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k20). c x y ⇒ f x → g y) → Mismatch p f xs → Mismatch p g ys Source # hcoerce ∷ ∀ (f ∷ k1 → Type) (g ∷ k20 → Type) (xs ∷ l1) (ys ∷ l2). AllZipN (Prod (Mismatch p)) (LiftedCoercible f g) xs ys ⇒ Mismatch p f xs → Mismatch p g ys Source # | |
HAp (Mismatch f ∷ (k → Type) → [k] → Type) Source # | |
(All (Compose Show f) xs, All (Compose Show g) xs) ⇒ Show (Mismatch f g xs) Source # | |
(All (Compose Eq f) xs, All (Compose Eq g) xs) ⇒ Eq (Mismatch f g xs) Source # | |
(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) Source # | |
Defined in Data.SOP.Match compare ∷ Mismatch f g xs → Mismatch f g xs → Ordering # (<) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (<=) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (>) ∷ Mismatch f g xs → Mismatch f g xs → Bool # (>=) ∷ Mismatch f g xs → Mismatch f g xs → Bool # | |
(All (Compose NoThunks f) xs, All (Compose NoThunks g) xs) ⇒ NoThunks (Mismatch f g xs) Source # | |
type Same (Mismatch f ∷ (k2 → Type) → [k2] → Type) Source # | |
type Prod (Mismatch f ∷ (k → Type) → [k] → Type) Source # | |
type SListIN (Mismatch f ∷ (k → Type) → [k] → Type) Source # | |
Defined in Data.SOP.Match | |
type AllN (Mismatch f ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source # | |
Defined in Data.SOP.Match |
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 → (∀ 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 ∷ ∀ f g xs. HasCallStack ⇒ String → NS f xs → NS g xs → NS (Product f g) xs Source #