Allow patterns in function params and add hints on shape coercion

[fizruk]

• Allow patterns in function types, e.g. ((x, y) : I * J) -> C x y
• Use shape types with parentheses (instead of braces)
  • in function types, e.g. ((t, s) : I * J | psi t /\ phi s) -> X t s
  • in parameters and lambda arguments
• Deprecate braces

  • in function types, e.g. {a : A} -> B a

  • in functions from shapes:

    [DEPRECATED]: at line 187 column 9
    the following notation is deprecated and will be removed from future version of rzk:
      { (t : I) | ϕ t \/ ψ t } → U
    instead consider using the following notation:
      (t : I | ϕ t \/ ψ t) → U
    

  • in parameters and lambda arguments

• Hints for shape coercions

  • in function types, e.g.

    [HINT]: consider replacing
      (s : J | ζ s) → X t s [χ s |-> f (t, s)]
    with the following
      (s : ζ) → X t s [χ s |-> f (t, s)]
    

  • in params and lambdas, e.g.

    [HINT]: at line 34 column 6 consider replacing
      \ (t : 2 | Δ¹ t) → t === 0_2 \/ t === 1_2
    with the following
      \ (t : Δ¹) → t === 0_2 \/ t === 1_2
    

The fix allows arbitrary terms in function types, and converts terms to patterns.

Note that parameters are desugared before hints/deprecations are checked, so messages do not correspond well to input (yet).