Generic contexts

[omelkonian]

Currently, we require the user to provide an associated type of contexts for the given type of expressions.

Conor McBride has shown that these correspond to just the type derivatives of the original type (http://strictlypositive.org/diff.pdf), so a good idea would be to generically derive these automatically. Alas, computing generic type derivatives can be very hard and impractical in the general case (mutually recursive types, etc...).

A more lightweight approach would be to use a Generic Zipper,
hence needing only one context type for all user-defined types, i.e.

data Context = Up | Down | Right

where up/down navigates the parent/children of a recursive datatype and right moves to the next sibling.