Annotating every node of a free foil term.

A node can be annotated with anything: a source position, a type, a memoised normal form. AnnSig turns a signature into an annotated one, and AnnAST is the annotated syntax it generates.

The annotation is a functor of the term, and that is what lets it depend on the node's scope. In AST binder sig n the signature's term parameter is the AST at the node's own scope, so an annotation built from it holds terms in that scope — which is what a type annotation in a dependent language needs. An annotation that ignores the term (a source position, say) is Const a.

Whether two annotations must agree for their nodes to match is a property of ann, not of AnnSig. Two examples, and they are the two you will want:

An annotation that ignores the term (a source position) and is compared:

instance Eq a => ZipMatchK (Const (a :: Type)) where
  zipMatchWithK _ (Const l) (Const r)
    | l == r    = Just (Const l)
    | otherwise = Nothing

An annotation that holds terms (a type, say) and is ignored, so that two terms differing only in their types are α-equivalent. Make the held term optional, so that pairing can fail without failing the match:

newtype TypeOf term = TypeOf (Maybe term)

instance ZipMatchK TypeOf where
  zipMatchWithK (f :^: M0) (TypeOf l) (TypeOf r) =
    Just (TypeOf (do { a <- l; b <- r; f a b }))

The instance must return Just unconditionally, and lazily. Matching is annotation-blind, so it must succeed whatever the annotations are; the paired annotation is a thunk the (annotation-skipping) Bifoldable never forces. A strict shape — TypeOf <$> f l r, or anything that yields Nothing when f fails — is a footgun twice over: it breaks blindness (two nodes with different types would fail to match), and it diverges for a finite or lazily-bottomed annotation (a universe tower ending in error, say), because forcing the annotation runs off the end. This is why the held term is a Maybe: a plain term field would have no value to pair when f fails, forcing a bottom into the result.

Do not reach for the generic instance here. It compares the annotation's shape, so a node carrying a memoised normal form would fail to match the same node without one. (Nor is zipMatchViaChooseLeft available: an annotation holding terms must construct a value at the result index, and cannot simply pick a side.)

Note the asymmetry in the instances below: Bifunctor and Bitraversable traverse the annotation, but Bifoldable does not. This is deliberate — see AnnSig.