Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data MatchPrim p k a where
- matchPrim :: Prim p k a -> MatchPrim p k a
- data MatchPrimD a where
- MatchPrimD :: MatchPrim p k a -> Prim p k a -> MatchPrimD (PrimS a)
- matchPrimD :: D a -> Maybe (MatchPrimD a)
- data MakePrim p k where
- makePrim :: Sing p -> Sing k -> Maybe (MakePrim p k)
- eqSymbol :: forall n1 n2. SSymbol n1 -> SSymbol n2 -> Maybe (n1 :~: n2)
- eqPrim :: Prim p1 k1 a -> Prim p2 k2 b -> Maybe ('(p1, k1, a) :~: '(p2, k2, b))
- eqField :: (forall x y. f x -> g y -> Maybe (x :~: y)) -> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2)
- eqRec :: (forall a b. t a -> t b -> Maybe (a :~: b)) -> Rec (Field t) fs -> Rec (Field t) gs -> Maybe (fs :~: gs)
- eqArrValue :: ArrValue a -> ArrValue b -> Maybe (a :~: b)
- eqD :: D a -> D b -> Maybe (a :~: b)
- dcast :: D a -> D b -> f a -> Maybe (f b)
Documentation
data MatchPrimD a where Source #
MatchPrimD :: MatchPrim p k a -> Prim p k a -> MatchPrimD (PrimS a) |
matchPrimD :: D a -> Maybe (MatchPrimD a) Source #
Checks if the given type is primitive, and if so returns a proof of that fact.
makePrim :: Sing p -> Sing k -> Maybe (MakePrim p k) Source #
Tries to make a primitive type with the given precision and kind. Fails if there is no primitive with the given combination.
eqField :: (forall x y. f x -> g y -> Maybe (x :~: y)) -> Field f p1 -> Field g p2 -> Maybe (p1 :~: p2) Source #