Allow to omit the signature of functions defined in instances

[valis]

Currently, the type of parameters and the result type of functions defined in instances can be inferred only when it does not mention other fields of the class. It should be possible to infer them anyway by substituting the implementation of fields.

Example:

\class C
  | z : Nat
  | f (x : Nat) (p : x = z) : z = 0

\instance inst : C
  | z => 0
  | f x p \elim x {
    | 0 => idp
    | suc _ => idp
  }