Reflection: Use Telescope for getContext, inContext, and extendContext

[L-TChen]

Currently, getContext and inContext only returns and takes a list of Arg Type without a name, and internally all variables are named x:

agda/src/full/Agda/TypeChecking/Unquote.hs

Lines 780 to 783 in 9428b1d

	extendCxt :: Arg R.Type -> UnquoteM a -> UnquoteM a
	extendCxt a m = do
	a <- locallyReduceAllDefs $ liftTCM $ traverse (isType_ <=< toAbstract_) a
	liftU1 (addContext ("x" :: String, domFromArg a :: Dom Type)) m

In order to print terms nicely, e.g. using debugPrint or typeError with termErr, I propose that they all should use Telescope (i.e. List (Σ String λ _ → Arg Type)) instead. For the same reason, extendContext should take an extra argument of type String in order to give a name to the variable introduced to the context.

It would be a breaking change but this change allows programmers to easily print not only understandable but also more precise type information during macro expansion.

[andreasabel]

Note: this breaks master of cubical:

• Reflection API changing in Agda 2.6.3 cubical#743

[asr]

I removed a trailing whitespace in the title.