Instances cannot be resolved if the type contains holes

[lukaszcz]

For example, type-checking

main : Nat :=
  for (acc := 0) ((x, _) in [1, 1; 2, 2; 3, 3]) {
    acc + x
  };

gives the error:

No trait instance found for: Foldable (List (Pair Nat Nat)) (Pair Nat _)

This is a more fundamental problem with not being able to backtrack on unification in the type checker.

[paulcadman]

We should tackle this after #3209

[lukaszcz]

I think I can solve this by replacing holes with instance metavariables during instance search, and then only unifying them at the end when the instance is found.