Fix false nonexhaustive record patterns warning

[erszcz]

This stems from the research in #418 and supersedes any experiments done there. By dropping argument-wise exhaustiveness checking we get rid of the false positive warning and therefore go from:

$ make gradualize | wc -l
make: *** [gradualize] Error 1
     361

to

$ make gradualize | wc -l
make: *** [gradualize] Error 1
     307

[erszcz]

Some comments need fixing, so I'm converting this to a draft for now.

[berbiche]

Neat, this seems better than #411

I will try the PR in the upcoming days 👍

edit: see #414 (comment)

[zuiderkwast]

Looks OK, but the one below worked before and now it's move to known problems (should fail). Do you think it is less important than the added test case? Can you think of a way to solve both?

-type t() :: ala | ola.

-spec f(t(), any()) -> ok.
f(ala, _) -> ok.

[erszcz]

Do you think it is less important than the added test case?

Yes, I think it's less important. We get rid of a very annoying and very common false positive warning that way.

Can you think of a way to solve both?

I don't know how to do that and I'm unsure if it's possible at all without really significant changes to the typechecker. The long explanation is in #418, together with some approaches I tried, but to no success :/

[zuiderkwast]

Then I think we can document that we do exhaustiveness if and only if all of the parameters are typed, not any(). Does it make sense? It's good to have a clear rule to follow.

[zuiderkwast]

OK, feel free to merge when ready.

The edoc comments are mainly for internal use. The user documentation (as far as we have any) is on the wiki so we can consider updating that too.