Some initial comments:

check-of: "Returns the most exact check matching the value, as a
procedure that this value must satisfy."

I think this procedure is a bit too open-ended to be portably useful:
`(λ (x) (eq? obj x))` would be a valid return value for any object,
although it is not very useful.

I would suggest fixing a set of portable return values that this
procedure will return for standard objects:

1. list? if the object is a (finite) list
2. pair? null? vector? string? boolean? char? bytevector? if the object
is one of those types
3. The most precise combination of exact?/inexact? and
number?/complex?/real?/rational?/integer? for number types
4. The record predicate for an inspectable record type (R6RS/SRFI
99/CLOS-like/whatever)

_______________

procedure-type-of: "Returns an implementation-specific number of
implementation-specific values"

This seems pretty unwieldy to use, because it is very difficult to bind
values to it. The only portable way to use it would be

     (let-values ((v (procedure-type-of proc)))
       ...)

It should return a fixed number of implementation-specific values.

As-is, the type operations are too unspecific to be of portable value.
Some reasonable things to specify are what it means for two types to be
eqv?, and to specify a type->check procedure to derive a check from a
type object. Maybe also procedures to do meta-introspection on type objects.

__________________

procedure-check-of: "This in particular might mean that procedures
defined with case-lambda(-checked) only get checks for the required
arguments. But this glaring under-design of this SRFI is offset by the
fact that multiple-arity procedures are problematic in many ways when it
comes to checks."

I was playing around with the idea of adding introspection to procedures
and thought that the easiest thing to do with case-lambda forms is to
store argument information as multiple lists, one list for each branch
of the case-lambda form. Here is a quick-and-dirty SRFI 259 example:

     (define-procedure-tag %make-introspectable
introspectable-procedure? procedure-info)

     (define-syntax my-case-lambda
       (syntax-rules ()
         ((_ (formal body ...) ...)
          (%make-introspectable
           '#(formal ...)
           (case-lambda (formal body) ...)))))

     (define f
       (my-case-lambda
         ((x) 1)
         ((x y) y)))

     (introspectable-procedure? f) => #t
     (procedure-info f) => #((x) (x y))

With more macro sugar this could be bolted onto an SRFI 259 procedure
for run-time introspection of checks.

-- Peter McGoron