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