-The data type for this list of witnesses is \haskelllhstexinline{Record}.
-The \haskelllhstexinline{Record} \gls{GADT} is parametrised by two type variables, the first type variable (\haskelllhstexinline{dt}) is the data type on which the constraints can be applied.
-The second type variable (\haskelllhstexinline{clist}) is the list of constraints itself.
-It is not just a list of \haskelllhstexinline{Constraint} but it is a list containing constraint constructors that will, when given a type of the polymorphic kind \haskelllhstexinline{k}, produce a constraint.
-This means that when \haskelllhstexinline{Cons} is pattern matched, the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
-\GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of the data type is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL}s using type classes but also type constructor classes (e.g.\ when using \glspl{GADT})..
+The data type for this list of witnesses is \haskelllhstexinline{Record} as shown in \cref{lst_cbde:record_type}.
+This \gls{GADT} is parametrised by two type variables.
+The first type variable (\haskelllhstexinline{dt}) is the type or type constructor on which the constraints can be applied and the second type variable (\haskelllhstexinline{clist}) is the list of constraints constructors itself.
+This means that when \haskelllhstexinline{Cons} is pattern matched, the overloading of the type class constraint for \haskelllhstexinline{c dt} can be solved by the compiler.
+\GHCmod{KindSignatures} is used to force the kinds of the type parameters and the kind of \haskelllhstexinline{dt} is polymorphic (\GHCmod{PolyKinds}) so that the \haskelllhstexinline{Record} data type can be used for \glspl{DSL} using type classes but also type constructor classes (e.g.\ when using \glspl{GADT}).