A few questions about BuiltInSynFamily/CoAxiomRules

[Jan van Brügge]

Hi lovely people,

sorry if my recent emails are getting annoying.

In the last few days I refactored my code to use `BuiltInSynFamily` and
`CoAxiomRule` to replace what was very ad-hoc code. So far so easy. But
I have a few questions due to sparse documentation.

First, about `BuiltInSynFamily`. It is a record of three functions. From
what I can tell by looking at `TcTypeNats`, the two `interact` functions
are used to solve the argument parts of builtin families based on known
results. `interactTop` seems to simply constraints on their own,
`interactInert` seems to simplify based on being given two similar
contraints.

By big questions is what exactly `matchFam` does. The argument seems to
be the arguments to the type family, but the tuple in the result is less
clear. The axiom rule is the proof witness, the second argument I guess
is the type arguments you actually care about? What is this used for?
The last one should be the result type.

Attached to that, what are the garantuees about the list of types that
you get? I assumed at first they were all flattened, but my other type
family is not. I am talking about this piece of code here:

```
matchFamRnil :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamRnil [] = Just (axRnilDef, [], mkRowTy k v [])
    where binders = mkTemplateKindTyConBinders [liftedTypeKind,
liftedTypeKind]
          [k, v] = map (mkTyVarTy . binderVar) binders
matchFamRnil _ = Nothing


matchFamRowExt :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
matchFamRowExt [_k, _v, x, y, row@(RowTy (MkRowTy k v flds))] = Just
(axRowExtDef, [x, y, row], RowTy (MkRowTy k v $ (x, y):flds))
matchFamRowExt [k, v, x, y, _rnil] = Just (axRowExtRNilDef, [k, v],
RowTy (MkRowTy k v [(x, y)]))
matchFamRowExt _ = Nothing

```

I needed an extra `_rnil` case  in `matchFamRowExt` because `RowExt
"foo" Int RNil` did not match the first pattern match (the dumped list I
got was `[Symbol, Type, "foo", Int, RNil]`). Also, is there a better way
to conjure up polykinded variables out of the blue or is this fine? I
thought about leaving off that info from the type, but then I would have
the same question when trying to implement `typeKind` or `tcTypeKind`
(for a non-empty row I can use the kinds of the head of the list, for an
empty one I would need polykinded variables)

My last question is about CoAxiomRules. The note says that they
represent "forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2", but it is not
clear for me in what relation the constraints on the left are with the
right. From the typeNats it looks like `t1` is the type family applied
to the `_1` arguments and `t2` is the calculated result using the `_2`
arguments. Why are we not getting just a list of types as inputs? Is the
`_1` always a unification/type variable and not really a type you can
use to calculate stuff? Also, if I extrapolate my observations to type
families without arguments, I would assume that I do not have
constraints on the left hand side as `t1` would be the family appied to
the arguments (none) and `t2` would be the calculated result from the
`_2` args (I do not need anything to return an empty row). Is this
correct or am I horribly wrong?


Thanks for your time listening to my questions, maybe I can open a PR
with a bit of documentation with eventual answers.

Cheers,
Jan