The description of crate-item-ok-goal for function declarations specifies that

For a fn declaration declared in the crate C, like the following:

fn foo<'a, T>(t: &'a T) -> u32 where T: Ord { ... }

We generate the following goal, which specifies that -- assuming the generics
are well formed and the where-clauses hold -- the field types are well-formed:

(∀ ((lifetime A) (type T))
    (implies ((well-formed (lifetime A))
              (well-formed (type T))
              (well-formed (type (rigid-ty (ref ()) (A (rigid-ty T ()))))))
      (well-formed-goal-for-biformula (T : Trait_Ord ()))))

but the implementation does not create well-formed clauses for the function's argument or return types.
https://github.com/nikomatsakis/a-mir-formality/blob/038b0e1ccfb2a3f591688d5855a42c129d577e85/racket-src/decl/decl-ok/crate-item.rkt#L56:L61