Ema.Route.Generic.Verification

Documentation

type family VerifyModels model (subModels :: [Type]) (lookups :: [Type]) :: Constraint where ...

VerifyModels model routeModels lookups verifies the given model to ensure that there exists a valid HasSubModels instance for the given combination of (model, routeModels, lookups).

Equations

VerifyModels m '[] '[] = ()

VerifyModels m '[] t = TypeError (('Text "'WithSubModels' has extra unnecessary types: " :$$: 'Text "") :$$: ('Text "\t" :<>: 'ShowType t))

VerifyModels m f '[] = TypeError (('Text "'WithSubModels' is missing submodel types: " :$$: 'Text "") :$$: ('Text "\t" :<>: 'ShowType f))

VerifyModels model (model ': fs) (model ': ss) = VerifyModels model fs ss

VerifyModels model (subModel ': subModels) (sel ': sels) = (HasAny sel model model subModel subModel, VerifyModels model subModels sels)

type family VerifyRoutes (rcode :: [Type]) (subRoutes :: [Type]) :: Constraint where ...

VerifyRoutes route rep subroutes verifies the given route to ensure that there exists a valid HasSubRoutes instance for route given its rep and the subroutes it is generic-deriving from.

Invariant: code ~ Code route

Equations

VerifyRoutes '[] '[] = ()

VerifyRoutes '[] t = TypeError (('Text "'WithSubRoutes' has extra unnecessary types: " :$$: 'Text "") :$$: ('Text "\t" :<>: 'ShowType t))

VerifyRoutes t '[] = TypeError (('Text "'WithSubRoutes' is missing subroutes for:" :$$: 'Text "") :$$: ('Text "\t" :<>: 'ShowType t))

VerifyRoutes (() ': rs) (() ': rs') = VerifyRoutes rs rs'

VerifyRoutes (r' ': rs) (() ': rs') = TypeError ('Text "A 'WithSubRoutes' entry is '()' instead of the expected: " :$$: 'ShowType r')

VerifyRoutes (r1 ': rs) (r2 ': rs') = (Coercible r1 r2, VerifyRoutes rs rs')