[ #5341 ] Context variables are no longer made non-erased.

By inverseApplyModality, which was renamed to
inverseApplyModalityButNotQuantity.

src/full/Agda/Syntax/Common.hs

@@ -459,8 +459,13 @@ inverseComposeModality (Modality r q c) (Modality r' q' c') =
 
 -- | Left division by a 'Modality'.
 --   Used e.g. to modify context when going into a @m@ argument.
-inverseApplyModality :: LensModality a => Modality -> a -> a
-inverseApplyModality m = mapModality (m `inverseComposeModality`)
+--
+-- Note that this function does not change quantities.
+inverseApplyModalityButNotQuantity :: LensModality a => Modality -> a -> a
+inverseApplyModalityButNotQuantity m =
+  mapModality (m' `inverseComposeModality`)
+  where
+  m' = setQuantity (Quantity1 Q1Inferred) m
 
 -- | 'Modality' forms a pointwise additive monoid.
 addModality :: Modality -> Modality -> Modality

src/full/Agda/TypeChecking/Irrelevance.hs

@@ -228,10 +228,9 @@ applyModalityToContext thing =
 --   Precondition: @Modality /= Relevant@
 applyModalityToContextOnly :: (MonadTCEnv tcm) => Modality -> tcm a -> tcm a
 applyModalityToContextOnly m = localTC
-  $ over eContext     (map $ inverseApplyModality m')
-  . over eLetBindings (Map.map . fmap . second $ inverseApplyModality m')
-  where
-  m' = setQuantity (Quantity1 Q1Inferred) m
+  $ over eContext (map $ inverseApplyModalityButNotQuantity m)
+  . over eLetBindings
+      (Map.map . fmap . second $ inverseApplyModalityButNotQuantity m)
 
 -- | Apply modality @m@ the the modality annotation of the (typing/equality)
 --   judgement.  This is part of the work done when going into a @m@-context.

src/full/Agda/TypeChecking/MetaVars.hs

@@ -322,8 +322,10 @@ newArgsMetaCtx' frozen condition (El s tm) tel perm ctx = do
       let mod  = getModality info
           -- Issue #3031: It's not enough to applyModalityToContext, since most (all?)
           -- of the context lives in tel. Don't forget the arguments in ctx.
-          tel' = telFromList . map (mod `inverseApplyModality`) . telToList $ tel
-          ctx' = (map . mapModality) (mod `inverseComposeModality`) ctx
+          tel' = telFromList $
+                 map (mod `inverseApplyModalityButNotQuantity`) $
+                 telToList tel
+          ctx' = map (mod `inverseApplyModalityButNotQuantity`) ctx
       (m, u) <- applyModalityToContext info $
                  newValueMetaCtx frozen RunMetaOccursCheck CmpLeq a tel' perm ctx'
       -- Jesper, 2021-05-05: When creating a metavariable from a

src/full/Agda/TypeChecking/Monad/Context.hs

@@ -189,10 +189,8 @@ class MonadTCEnv m => MonadAddContext m where
 
 -- | Default implementation of addCtx in terms of updateContext
 defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
-defaultAddCtx x a ret = do
-  q <- viewTC eQuantity
-  let ce = (x,) <$> inverseApplyQuantity q a
-  updateContext (raiseS 1) (ce :) ret
+defaultAddCtx x a ret =
+  updateContext (raiseS 1) (((x,) <$> a) :) ret
 
 withFreshName_ :: (MonadAddContext m) => ArgName -> (Name -> m a) -> m a
 withFreshName_ = withFreshName noRange

src/full/Agda/TypeChecking/Rules/LHS.hs

@@ -862,7 +862,8 @@ checkLHS mf = updateModality checkLHS_ where
  updateModality cont st@(LHSState tel ip problem target psplit) = do
       let m = getModality target
       applyModalityToContext m $ do
-        cont $ over (lhsTel . listTel) (map $ inverseApplyModality m) st
+        cont $ over (lhsTel . listTel)
+                 (map $ inverseApplyModalityButNotQuantity m) st
         -- Andreas, 2018-10-23, issue #3309
         -- the modalities in the clause telescope also need updating.
 

test/Fail/Issue5341.agda

@@ -0,0 +1,3 @@
+postulate
+  F : Set → Set
+  _ : {@0 A : Set} → F λ { → A }

test/Fail/Issue5341.out

@@ -0,0 +1,3 @@
+Issue5341.agda:3,30-31
+Variable A is declared erased, so it cannot be used here
+when checking that the expression A has type Set