Typer failure on ambiguous type argument

[jiribenes]

Error: Cannot fully infer type for addError: [T, E](Result[T, E], E) => Result[T, E]

type Result[T, E] {
  Success(value: T)
  Failure(errors: List[E])
}

def addError[T, E](result: Result[T, E], e: E) =
  result match {
    case Success(value)  => Failure([e])             // also error: Cannot infer type argument T, maybe consider annotating it?
    case Failure(errors) => Failure(Cons(e, errors)) // also error: Cannot infer type argument T, maybe consider annotating it?
  }

Reproducible both on the website and on v0.25.

[jiribenes]

Doing eta [?] of the match, i.e.

def addError[T, E](result: Result[T, E], e: E) =
  Failure(Cons(e, result match {
    case Success(value) => Nil()
    case Failure(errors) => errors
  }))

produces two errors:

Cannot fully infer type for addError: [T, E](Result[T, E], E) => Result[T, E]
Cannot infer type argument T, maybe consider annotating it?

But if you annotate the Failure as Failure[T, E], then everything seems to work!

So I think the actual error is just Cannot infer type argument T, maybe consider annotating it? for the Failure cases happening twice -- my hypothesis is that:

1. first case has type Failure[?T1, E]
2. second case has type Failure[?T2, E]

The result type is a merge of 1. and 2., but our types are invariant, so we can't even compare ?T1 and ?T2, therefore we just give up and report the Cannot infer type argument T, maybe consider annotating it? heuristic for each one.

Can we do better here somehow?

[jiribenes]

What would definitely help is to name the type for which we're reporting: Cannot infer type argument T, maybe consider annotating it?
Something like:

Cannot infer type argument T *of Failure[T, E]*,  ...

would help, provided we have the info?

effekt/effekt/shared/src/main/scala/effekt/typer/Constraints.scala

Lines 206 to 213 in a7d1a1f

	def leave(types: List[UnificationVar], capts: List[CaptUnificationVar]): Unit =
	// Check that we could infer all types of type variable instantiations.
	types.foreach {
	case x @ UnificationVar(underlying, callTree) =>
	if (!typeSubstitution.isDefinedAt(getNode(x))) C.at(callTree) {
	C.error(s"Cannot infer type argument ${underlying}, maybe consider annotating it?")
	}
	}

[jiribenes]

#932 has a part of the solution, but I never finished it -- we need to thread the implicit Context through in order to resolve a symbol.