Support macros and/or polymorphism to simplify proofs

[fizruk]

In rzk-lang/sHoTT#138, @TashiWalde suggests to support some form of metaprogramming to simplify proofs:

Side remark for @fizruk : For these sort of constructions it would be very convenient if rzk would support some rudimentary meta-programming features. For example, it would be nice if I could define a macro (syntax just as an example)

#macro @isomorphism-shape-inclusions (repg ; repf)
  :=
    ( \ A →
      ( repg
      , ( ( repf , \ _ → refl)
        , ( repf , \ _ → refl)))
    , \ A _ →
      ( \ repg
      , ( ( repf , \ _ → refl)
        , ( repf , \ _ → refl))))

and then define

#def isomorphism-0-Δ¹-1-right-leg-of-Λ
  : isomorphism-shape-inclusions
    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 0₂)
  := @isomorphism-shape-inclusion
     ( \ τ (t,s) → τ s
     ; \ υ s → υ (1₂ , s))

and have the compiler automatically do a syntactic-expansion of the macro @isomorphism-shape-> inclusion before type-checking.

In the specific example above it is not too bad, since the formula defining the map of shapes is so short. But it one defines isomorphisms or maps on more complicated shapes, the formulas may involve case distinctions and become long; in that case repeating them multiple times can quickly make the code explode.

Note that there is no way to make this macro into an actual function (without some polymorphism) because different instances of \ τ (t,s) → τ s have different types.

I see the following options (that have to be thought through):

1. Add a (good) macro system (e.g. à la Lean).
2. Support necessary type system features (polymorphism/implicit arguments/instance arguments) to make it possible for @isomorphism-shape-inclusion to become an actual function.
3. Support type coercions, e.g. A → B could be coerced to Σ (f : A → B), P f whenever P f can be figured out from context (especially, if it's a proposition).

I am generally hesitant to add a macro system, since macros tend to get out of hand fairly easily, unless implemented with extra care. Also, implementing a good (hygienic macro) system is not trivial and will take time. That said, I am open to suggestions.

At the moment, I think type inference and implicit arguments should be the priority, since we want them anyway. Once that is implemented, we can see what inconveniences are left and decide for an appropriate solution.