T :: forall k -> (k ~ k) => forall j -> k -> j -> *