+type CoTyConKindChecker = forall m. Monad m => CoTyConKindCheckerFun m
+
+type CoTyConKindCheckerFun m
+ = (Type -> m Kind) -- Kind checker for types
+ -> (Type -> m (Type,Type)) -- and for coercions
+ -> Bool -- True => apply consistency checks
+ -> [Type] -- Exactly right number of args
+ -> m (Type, Type) -- Kind of this application
+
+ -- ^ Function that when given a list of the type arguments to the 'TyCon'
+ -- constructs the types that the resulting coercion relates.
+ -- Returns Nothing if ill-kinded.
+ --
+ -- INVARIANT: 'coKindFun' is always applied to exactly 'tyConArity' args
+ -- E.g. for @trans (c1 :: ta=tb) (c2 :: tb=tc)@, the 'coKindFun' returns
+ -- the kind as a pair of types: @(ta, tc)@
+