-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)@
-