Do not make context variables non-erased

[nad]

This issue has been broken out of issue #4525.

Agda accepts the following code:

postulate
  F : @0 Set → Set

G : @0 Set → Set
G A = F (λ { → A })

The reason why this code is accepted is that when an erased argument is checked, then Agda makes all variables in the context non-erased:

agda/src/full/Agda/TypeChecking/Rules/Application.hs

Lines 694 to 699 in b63b0ad

	case unEl t0' of
	Pi (Dom{domInfo = info', domName = dname, unDom = a}) b
	| let name = bareNameWithDefault "_" dname,
	sameHiding info info'
	&& (visible info || maybe True (name ==) mx) -> do
	u <- lift $ applyModalityToContext info' $ do

Thus, when the pattern-matching lambda is checked, the variable A is treated as non-erased.

The following code is rejected, because Agda does not make the variables in the context non-erased:

@0 F : @0 Set → Set
F A = λ { → A }

I suggest that we stop changing the context, and instead keep track of whether a term is in an erased context or not. (The TCEnv's envModality field is already supposed to keep track of this.)

[nad]

I found a related problem, and I hope I have a fix for it.