Validate the logic for merging "any" vs. "all" guesses in param inference.

Specifically:

"All" merges attempt to target the most-general guess. Each "all" guess for a param must be satisfied because all of the conversions they came from are required to happen.
"Any" merges attempt to target the least-general guess. In theory, we could take any one of them as "the" guess, since all guesses came from successful conversions. But, the existence of multiple guesses causes ambiguity, so it makes sense to try to merge them.

Is that's actually what happens? I think that those semantics originally had some relationship to variance, so I also need to look into how "any" and "all" conversions relate to covariant and contravariant conversions. (mergeInferredTypes might need more patterns in anyCheck and allCheck to ensure that variance is handled consistently.)

Another consideration is that mergeAllM Nothing is the default return when conversion succeeds and there are no guesses. What happens when we process something like mergeAny [mergeAll Nothing,someGuess]? The result should always be someGuess, even though mergeAll Nothing isn't an identity for mergeAny.

It's possible that "any" and "all" guess merges don't need to be treated differently, due to the way conversion checks deal with covariance and contravariance.

Looking just at variance for now:

Reader<A>→Reader<#x>: #x can be any B s.t. A→B. (Covariant)
Writer<A>→Writer<#x>: #x can be any B s.t. B→A. (Contravariant)
When checking two covariant guesses B and C, if B→C then C must be kept.
When checking two contravariant guesses B and C, if B←C then C must be kept.
If either guess is invariant then the invariant one must be kept.
When checking covariant B and contravariant C, #x must fall between B and C. First of all, this is only possible if B→C. Which of the two should be preferred, though?

Merging covariant and contravariant too early could cause other merges to fail; therefore, it's probably better to keep both and then have a "final" merge stage that prefers the contravariant, i.e., the more constrained end of the range.

This still leaves a possible scenario where we have covariant B and C and contravariant D. This can only happen if B and C cannot be converted in either direction. Rather than trying to replace both with D, it would be better to keep both, thus giving the user an error due to the ambiguity.

The above makes sense for "all" aggregation, but it's unclear how to deal with "any".

It would make sense to keep "all" as a merge operation and treat "any" as an operation on alternatives, e.g., All{ a, Any{ b, c } } becomes Try{ Merge{ a, b }, Merge{ a, c } }, where Try selects any alternative that has a single result. The rationale here is that if #x can be b or c but doesn't need to be both, then the failure to merge one should eliminate it as a possibility.

On the other hand, another way to look at it is using duality: "all" (intersection) and "any" (union) are duals, just as covariant and contravariant are duals. So, if "all" preferred covariant guesses over contravariant and "any" preferred the reverse, then the merge operation would (probably?) be self-dual.

The main issue with that approach is "all" loses upper bounds and "any" loses lower bounds before moving onto the next level. This will only be problematic if "all" and "any" are nested with each other, e.g., there are multiple function args and one of them is a type union with both a covariant guess and a contravariant guess. In such cases, a type error after inference would be possible.

So, for now I'm going to accept that type-inference could result in a bad type guess, i.e., it's not going to be a dichotomy between "valid inference" vs. "failed inference".

It's worth noting that a union with covariant guess A and contravariant guess B has a "range" of valid guesses (all,B] ∪ [A,any), i.e., anything not strictly in (B,A). If A→B then literally any type on a chain passing through A will do. So, I don't think there's any point preserving A in this situation.

Similar logic can be applied to the intersection case.

Therefore, it should be fine to drop covariant guesses for "any" and contravariant guesses for "all" where possible, as mentioned in the previous comment.

In the case of "all", invariant guesses must be preserved. On the other hand, they don't need to be preserved in "any"; even if they can't be merged. For consistency, however, it's appropriate to only eliminate invariant guesses in "any" if they can be merged.

So, I think the actual end result of all of this is that the original behavior was appropriate.

If this approach becomes problematic, it would be reasonable to infer a meta type when things can't be merged. For example, if A and B can't be merged then go with [A&B] or [A|B], for "all" and "any", respectively.

It turns out it isn't quite that simple, but unions and intersections can still be helpful. (Note that, since unions and intersections are defined as limits and colimits, they are the "best" way to combine two types.)

"All" Semantics

If A→#x and B→#x then A,B→[A|B]→#x. Further, if A→B then [A|B]=B.
If A←#x and B←#x then A,B←[A&B]←#x. Further, if A←B then [A&B]=B.

"Any" Semantics

If A→#x or B→#x then [A&B]→A,B→#x. Further, if B→A then [A&B]=B.
If A←#x or B←#x then [A|B]←A,B←#x. Further, if B←A then [A|B]=B.

Invariance

A guess of A=#x can't be included in any union or intersection because invariance doesn't allow conversion. We could in theory discard those guesses in "any", but we must keep them in "all". Therefore, it's probably better to just pass them along untouched.
Each "any" and "all" merge operation can therefore result in a single guess of each variance type. At the final "all" stage in mergeInferredTypes, we can then try to merge them into a single guess, preferring invariant, covariant, and lastly contravariant.

Actually, the reasoning for "any" is invalid above because the merged result needs to be between the original guesses and #x.

If A→#x or B→#x then A,B→[A|B]→#x. Further, if A→B then we can choose A as a more relaxed guess. (We can still get back to B if needed in "all".)
If A←#x or B←#x then A,B←[A&B]←#x. Further, if A←B then we can choose A as a more relaxed guess. (We can still get back to B if needed in "all".)
We can also attempt to merge invariant guesses with either covariant or contravariant, so that their optionality isn't lost when moving to the next level.

Another thing I hadn't thought about before: Conversion checks for Invariant (in TypeInstance.hs) perform a mergeAllM on the results of separate Covariant and Contravariant checks. because of this, there will generally not be invariant guesses; instead, it will likely be a pair of covariant and contravariant guesses with the same type.

So, the merging logic needs to treat invariant guesses as if they were both lower and upper bounds.

If an "any" or "all" merge operation yields multiple guesses, all of those constraints must be met.
Saying #x∈[A,B] and #x=C is the same as saying #x∈[[A|C],[B&C]], whether or not simplifications can be made. This means that "all" handles the two representations consistently.
A failure of [A|C]→[B&C] in the final merge would mean that the range is actually empty.
"Any" operations will remove invariant C if A→C or B←C.
- If A→C→B then both C→ and C← are removed, which is consistent with removing invariant C.
- If A→C and C←B then the range becomes [A,C]. This allows for possible guesses that fall between B and C, whereas if C was invariant then it would have just been removed.

I think these issues can be summarized as a failure to properly distribute an "or" operation over "and" operations, i.e., (a&b)|(c&d) ≠ (a|c)&(b|d). Put another way, "any" fails to turn an "or" operation into an "and" operation to pass on to the next merging stage. Or, multiple guesses from "any" should be treated as an "or".

A more set-theoretic approach using ranges:

There is no way to turn [A,B]∪[C,D] into a single range if they don't already intersect, which is a problem when "all" concatenates guesses before merging them.
An invariant guess C should be converted to [C,C].
If not A→B then [A,B]=∅; therefore, such ranges should be dropped.
For "all" operations, if [A,B]∩[C,D]=∅ then they should be dropped; otherwise, they should be intersected.
For "any" operations, if [A,B]∩[C,D]≠∅ then they should be unioned; otherwise, they should be kept separate.
We can distribute "all" over "any" with (a|b)&(c|d) → (a&c)|(a&d)|(b&c)|(b&d). This will allow the result of each "all" to be the union of ranges. This can be done in the "all" stages.

It's probably better to transform the guesses from a MergeTree into something that treats "all" and "any" differently.

For example:

data GuessRange a =
  GuessRange {
    grLower :: a,
    grUpper :: a
  }

data GuessUnion a =
  GuessUnion {
    guGuesses :: [GuessRange a]
  }

The operations for reduceMergeTree would then be:

leafOp: Turn A→ into [A,any], A← into [all,A], and A= into [A,A].
anyOp: Concatenate guGuesses.
allOp: Fold the list of guess lists. (foldr probably won't work, due to CompileErrorM.)

To combine list X and list Y:
- For each pairing of ranges x∈X and y∈Y, add x∩y to a new list if the intersection isn't empty.
- Combine ranges in the resulting list where possible.

The final result will be a set of possible ranges for the inferred param; the final choice is arbitrary.

If there is only one range remaining, it would make sense to take either end of it, e.g., the lower bound if it isn't all, and the upper bound otherwise. (Note that function params are invariant, so there's no real reason to prefer one end over the other.)
If there are multiple ranges, the user is likely to also be confused; therefore, it's probably better to treat other-than one remaining range as an error.

ta0kira / zeolite