Type-checking optional arguments

I wanted to make some sort functions with an optional key argument (like I remember from Lisp in the old days), but the type checker doesn’t seem to like Fun.id as the default value. I guess because ‘a → ‘a is more specific than a’ → b’?

But even a specified key will lock in a more specific type for that particular call, and the default argument isn’t any more relevant to the function’s type when it’s not used than any other possible argument is. ‘a = ‘b is consistent with a’ → b’ as long as it’s not an absolute requirement.

So wouldn’t it be possible for a type checker to accept that sort of situation? Is there currently a way to make it work? Just wondering.

EDIT: Oh, I see this was discussed in Begginer looking to provide a default parameter without changing the signature of a function.