type
type Context (n :: Nat) s t a b = (GenericN s, GenericN t, Defined (Rep s) (NoGeneric s '['Text "arising from a generic traversal of the type parameter at position "
':<>: QuoteType n, (('Text "of type "
':<>: QuoteType a) ':<>: 'Text " in "
) ':<>: QuoteType s]) (), s ~ Infer t (P n b 'PTag) a, t ~ Infer s (P n a 'PTag) b, Error (ArgCount s <=? n) n (ArgCount s) s, a ~ ArgAt s n, b ~ ArgAt t n, GHasTypes ChGeneric (RepN s) (RepN t) (Param n a) (Param n b))