Make it possible to leave out implicit fields for copattern matches

[jashug]

Minor feature request. This was considered in #2288 and postponed.

I have a use case for leaving out implicit fields even if metas for the implicit right-hand sides are added late. Define InstanceField as

record InstanceField (Field : Set) : Set where
  field
    {{box}} : Field

When the type Field is a strict singleton like unit, an implicit variable of type InstanceField Field can be solved even if the implicit is otherwise unconstrained. This allows introducing an instance field which is always automatically solved without defining any top-level instances, as long as the instance type is a strict singleton.

When overloading notation, the following is a useful named strict singleton.

record Define-+ (X : Set) (_+_ : X → X → X) : Set where
-- zero fields

I would like to use this as

_+_ : {X : Set} {_+_ : X → X → X} → {{Define-+ X _+_}} → X → X → X
_+_ {_+_ = _+_} = _+_

open import Agda.Builtin.Equality using (_≡_ ; refl)

record AbelianGroup : Set₁ where
  field
    Carrier : Set
    operation : Carrier → Carrier → Carrier
    {overload-plus} : InstanceField (Define-+ Carrier operation)
    commutative : ∀ {x y : Carrier} → x + y ≡ y + x
open AbelianGroup hiding (overload-plus)

module _ (G : AbelianGroup) where
  -- This works great: the instance field gets picked up, giving
  -- a definition for + on G .Carrier when G is a local variable
  test : ∀ {x y : G .Carrier} → x + y ≡ x + y
  test = refl

record Unit : Set where
-- Error: incomplete pattern matching ... missing overload-plus
Unit-Ab : AbelianGroup
Unit-Ab .Carrier = Unit
Unit-Ab .operation _ _ = _
Unit-Ab .commutative = refl

Allowing the implicit field to be left out if it can still be solved would mean that I don't have to include a clause

Unit-Ab .overload-plus = _

which would be nice.

---

If this is added with the implicit metas being added late (which from the linked issue sounds easy to implement), there is a question about user messages. If the implicit metas can't be solved, or if checking explicit fields which depend on a missing implicit field fails, a the fact that there was a missing field would be a helpful addition to the error message which might otherwise be full of unsolved metas.

Note that if later fields do depend on an instance field which is omitted, we can get similar errors in the status quo:

open import Agda.Builtin.Equality using (_≡_ ; refl)

record One : Set where
  no-eta-equality
  instance constructor tt
record Two : Set where
  field
    {{one}} : One
    two : one ≡ tt
test2 : Two
test2 .Two.two = refl
-- test2.Two.one != tt of type One
-- when checking that the expression refl has type test2 .Two.one ≡ tt

As the linked issue says, this is probably more common with implicit rather than instance fields, but we can still hit most or all of the edge cases caused by omitting implicit fields in the current implementation by replacing them with instance fields. So implementing the late addition of implicit metas for missing implicit fields should not create many new problems.