Currently, both Github_core.Pull.get and Gitub_core.Pull.for_repo both return values of type pull.
My understanding is that, type pull represents what the GitHub API (in the response schema for the repos/OWNER/REPO/pulls endpoint) calls a "Pull Request Simple".
However, the repos/OWNER/REPO/pulls/PULL_NUMBER endpoint (for fetching a single pull request) returns what GitHub calls in the response schema a "Pull Request".
Critically for my purposes, the "Pull Request" object includes many properties that are omitted from the "Pull Request Simple" object, including properties that indicate whether a PR is mergable or whether it has auto_merge enabled.
If we wanted to support inspecting these extended attributes, I think we'd need to introduce a new ATD type that inherited from and extended type pull, and then adapt Github_core.Pull.get to deserialize into the corresponding record.
Perhaps this new type could be something like the following?
type pull_full = {
mergeable: bool;
(* etc... *)
inherit pull
}
If maintaining backwards compatibility where not paramount, you might instead rename the current type pull as type pull_simple to more closely reflect the GitHub API.
On the other hand, to avoid breaking backwards compatibility, we might introduce a new function Github_core.Pull.get_full.
What do you all think of pursuing some such change?