Instance resolution kicks in too late when populating record

[omelkonian]

Instance resolution kicks in too late when populating record

[jespercockx]

The problem is that with λ where you don't necessarily get a simple list of all the fields: there can be other patterns or copatterns, and this can be different for each clause. To solve this properly, what we'd need to do is to first construct the case tree (inserting missing cases in the process) and only then check all of the right-hand sides. But this is not what we do currently: we start by typechecking each clause in isolation and only build the case tree after the fact. It's also not clear how we should deal with overlapping clauses if that strategy would be implemented.

See also #2124 and #3054.

[UlfNorell]

It's the same reason this also fails:

-- ✖ fails
_ : X
_ = λ where
  .p → refl
  .x → it

To type check the p clause you need the x clause to evaluate. Missing clauses are inserted after type checking the given clauses, so leaving it out behaves the same as writing it at the end.

I would be a little hesitant to say that we should postpone checking the p clause until we know the value of the x clause. You have to be very careful if doing that to not introduce cyclic dependencies between the clauses.

[omelkonian]

OK, that makes some sense, it just didn't occur to me that the order of fields matters.
However, this still doesn't explain why the same thing using record is not order-dependent; this seems somewhat inconsistent.

Also, shouldn't the type checker perform checks according to the dependency order of the fields (i.e. perform a topological sort first, then start type-checking individual fields) and whenever an instance field is encountered either search for a term given by the user, or otherwise appeal to instance resolution. Something like that..