re #5448: check that clause target type is usable at modality

src/full/Agda/Interaction/BasicOps.hs

@@ -491,7 +491,7 @@ instance Reify Constraint where
       t <- jMetaType . mvJudgement <$> lookupLocalMeta m
       OfType <$> reify (MetaV m []) <*> reify t
     reify (CheckType t) = JustType <$> reify t
-    reify (UsableAtModality _ mod t) = UsableAtMod mod <$> reify t
+    reify (UsableAtModality _ _ mod t) = UsableAtMod mod <$> reify t
 
 instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
   prettyTCM (OutputForm r pids unblock c) =
@@ -664,7 +664,7 @@ getConstraintsMentioning norm m = getConstrs instantiateBlockingFull (mentionsMe
         CheckMetaInst{}            -> Nothing
         CheckType t                -> isMeta (unEl t)
         CheckLockedVars t _ _ _    -> isMeta t
-        UsableAtModality ms _ t    -> caseMaybe ms (isMeta t) $ \ s -> isMetaS s `mplus` isMeta t
+        UsableAtModality _ ms _ t  -> caseMaybe ms (isMeta t) $ \ s -> isMetaS s `mplus` isMeta t
 
     isMeta (MetaV m' es_m)
       | m == m' = Just es_m

src/full/Agda/Syntax/Common.hs

@@ -1244,7 +1244,6 @@ nonStrictToIrr :: Relevance -> Relevance
 nonStrictToIrr NonStrict = Irrelevant
 nonStrictToIrr rel       = rel
 
-
 ---------------------------------------------------------------------------
 -- * Annotations
 ---------------------------------------------------------------------------

src/full/Agda/TypeChecking/Constraints.hs

@@ -294,7 +294,7 @@ solveConstraint_ (HasPTSRule a b)       = hasPTSRule a b
 solveConstraint_ (CheckDataSort q s)    = checkDataSort q s
 solveConstraint_ (CheckMetaInst m)      = checkMetaInst m
 solveConstraint_ (CheckType t)          = checkType t
-solveConstraint_ (UsableAtModality ms mod t) = usableAtModality' ms mod t
+solveConstraint_ (UsableAtModality cc ms mod t) = usableAtModality' ms cc mod t
 
 checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
 checkTypeCheckingProblem = \case

src/full/Agda/TypeChecking/Coverage/Cubical.hs

@@ -901,7 +901,7 @@ createMissingTrXConClause q_trX f n x old_sc c (UE gamma gamma' xTel u v rho tau
   applyModalityToContext mod $ do
     unlessM (asksTC hasQuantity0) $ do
     reportSDoc "tc.cover.trxcon" 20 $ text "testing usable at mod: " <+> pretty mod
-    addContext cTel $ usableAtModality mod rhs
+    addContext cTel $ usableAtModality IndexedClause mod rhs
 
   return cl
 

src/full/Agda/TypeChecking/Irrelevance.hs

@@ -93,6 +93,7 @@ import Agda.Utils.Function
 import Agda.Utils.Lens
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
+import qualified Agda.Utils.Null as Null
 
 -- | data 'Relevance'
 --   see "Agda.Syntax.Common".
@@ -480,18 +481,44 @@ instance UsableModality a => UsableModality (Arg a) where
 instance UsableModality a => UsableModality (Dom a) where
   usableMod mod Dom{unDom = u} = usableMod mod u
 
-usableAtModality' :: MonadConstraint TCM => Maybe Sort -> Modality -> Term -> TCM ()
-usableAtModality' ms mod t = catchConstraint (UsableAtModality ms mod t) $ do
-  whenM (maybe (pure True) isFibrant ms) $ do
-    res <- runExceptT $ usableMod mod t
-    case res of
-      Right b -> do
-        unless b $
-          typeError . GenericDocError =<< (prettyTCM t <+> "is not usable at the required modality" <+> prettyTCM mod)
-      Left blocker -> patternViolation blocker
-
-
-usableAtModality :: MonadConstraint TCM => Modality -> Term -> TCM ()
+usableAtModality'
+  :: MonadConstraint TCM
+  -- Note: This weird-looking constraint is to trick GHC into accepting
+  -- that an instance of MonadConstraint TCM will exist, even if we
+  -- can't import the module in which it is defined.
+  => Maybe Sort -> WhyCheckModality -> Modality -> Term -> TCM ()
+usableAtModality' ms why mod t =
+  catchConstraint (UsableAtModality why ms mod t) $ do
+    whenM (maybe (pure True) isFibrant ms) $ do
+      res <- runExceptT $ usableMod mod t
+      case res of
+        Right b -> unless b $
+          typeError . GenericDocError =<< formatWhy
+        Left blocker -> patternViolation blocker
+  where
+    formatWhy = do
+      cubes <- isJust . optCubical <$> pragmaOptions
+      let
+        justification = if cubes then "in Cubical Agda," else "when --without-K is enabled,"
+      case why of
+        IndexedClause ->
+          vcat
+            [ fsep ( pwords "This clause has target type"
+                  ++ [prettyTCM t]
+                  ++ pwords "which is not usable at the required modality"
+                  ++ [prettyTCM mod])
+            , ""
+            , fsep ( "Note:":pwords justification
+                  ++ pwords "the target type must be usable at the modality"
+                  ++ pwords "in which the function was defined, since it is"
+                  ++ pwords (if cubes then "used for computing transports." else "used in substitutions.")
+                   )
+            , ""
+            ]
+        _ -> prettyTCM t <+> "is not usable at the required modality" <+> prettyTCM mod
+
+
+usableAtModality :: MonadConstraint TCM => WhyCheckModality -> Modality -> Term -> TCM ()
 usableAtModality = usableAtModality' Nothing
 
 

src/full/Agda/TypeChecking/MetaVars/Mention.hs

@@ -123,7 +123,7 @@ instance MentionsMeta Constraint where
     CheckMetaInst m     -> True   -- TODO
     CheckType t         -> mm t
     CheckLockedVars a b c d -> mm ((a, b), (c, d))
-    UsableAtModality ms mod t -> mm (ms, t)
+    UsableAtModality _ ms mod t -> mm (ms, t)
     where
       mm :: forall t. MentionsMeta t => t -> Bool
       mm = mentionsMetas xs

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

@@ -1092,6 +1092,16 @@ data ProblemConstraint = PConstr
 instance HasRange ProblemConstraint where
   getRange = getRange . theConstraint
 
+-- | Why are we performing a modality check?
+data WhyCheckModality
+  = ConstructorType
+  -- ^ Because --without-K is enabled, so the types of data constructors
+  -- must be usable at the context's modality.
+  | IndexedClause
+  -- ^ Because --without-K is enabled, so the result type of clauses
+  -- must be usable at the context's modality.
+  deriving (Show, Generic)
+
 data Constraint
   = ValueCmp Comparison CompareAs Term Term
   | ValueCmpOnFace Comparison Term Type Term Term
@@ -1123,7 +1133,7 @@ data Constraint
     -- ^ Last argument is the error causing us to postpone.
   | UnquoteTactic Term Term Type   -- ^ First argument is computation and the others are hole and goal type
   | CheckLockedVars Term Type (Arg Term) Type     -- ^ @CheckLockedVars t ty lk lk_ty@ with @t : ty@, @lk : lk_ty@ and @t lk@ well-typed.
-  | UsableAtModality (Maybe Sort) Modality Term
+  | UsableAtModality WhyCheckModality (Maybe Sort) Modality Term
     -- ^ Is the term usable at the given modality?
     -- This check should run if the @Sort@ is @Nothing@ or @isFibrant@.
   deriving (Show, Generic)
@@ -1161,7 +1171,7 @@ instance Free Constraint where
       CheckDataSort _ s     -> freeVars' s
       CheckMetaInst m       -> mempty
       CheckType t           -> freeVars' t
-      UsableAtModality ms mod t -> freeVars' (ms, t)
+      UsableAtModality _ ms mod t -> freeVars' (ms, t)
 
 instance TermLike Constraint where
   foldTerm f = \case
@@ -1182,7 +1192,7 @@ instance TermLike Constraint where
       CheckDataSort _ s      -> foldTerm f s
       CheckMetaInst m        -> mempty
       CheckType t            -> foldTerm f t
-      UsableAtModality ms m t   -> foldTerm f (Sort <$> ms, t)
+      UsableAtModality _ ms m t   -> foldTerm f (Sort <$> ms, t)
 
   traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented
 
@@ -5307,6 +5317,7 @@ instance NFData ForeignCode
 instance NFData Interface
 instance NFData a => NFData (Closure a)
 instance NFData ProblemConstraint
+instance NFData WhyCheckModality
 instance NFData Constraint
 instance NFData Signature
 instance NFData Comparison

src/full/Agda/TypeChecking/Pretty/Constraint.hs

@@ -157,7 +157,7 @@ instance PrettyTCM Constraint where
           prettyTCM t <+> "is a well-formed type"
         CheckLockedVars t ty lk lk_ty -> do
           "Lock" <+> prettyTCM lk <+> "|-" <+> prettyTCMCtx TopCtx t <+> ":" <+> prettyTCM ty
-        UsableAtModality ms mod t -> "Is usable at" <+> text (verbalize mod) <+> "modality:" <+> prettyTCM t
+        UsableAtModality _ ms mod t -> "Is usable at" <+> text (verbalize mod) <+> "modality:" <+> prettyTCM t
           -- TODO: print @ms : Maybe Sort@ as well?
 
       where

src/full/Agda/TypeChecking/Reduce.hs

@@ -301,7 +301,7 @@ instance Instantiate Constraint where
   instantiate' (CheckDataSort q s)  = CheckDataSort q <$> instantiate' s
   instantiate' c@CheckMetaInst{}    = return c
   instantiate' (CheckType t)        = CheckType <$> instantiate' t
-  instantiate' (UsableAtModality ms mod t) = flip UsableAtModality mod <$> instantiate' ms <*> instantiate' t
+  instantiate' (UsableAtModality cc ms mod t) = flip (UsableAtModality cc) mod <$> instantiate' ms <*> instantiate' t
 
 instance Instantiate CompareAs where
   instantiate' (AsTermsOf a) = AsTermsOf <$> instantiate' a
@@ -938,7 +938,7 @@ instance Reduce Constraint where
   reduce' (CheckDataSort q s)   = CheckDataSort q <$> reduce' s
   reduce' c@CheckMetaInst{}     = return c
   reduce' (CheckType t)         = CheckType <$> reduce' t
-  reduce' (UsableAtModality ms mod t) = flip UsableAtModality mod <$> reduce' ms <*> reduce' t
+  reduce' (UsableAtModality cc ms mod t) = flip (UsableAtModality cc) mod <$> reduce' ms <*> reduce' t
 
 instance Reduce CompareAs where
   reduce' (AsTermsOf a) = AsTermsOf <$> reduce' a
@@ -1105,7 +1105,7 @@ instance Simplify Constraint where
   simplify' (CheckDataSort q s)   = CheckDataSort q <$> simplify' s
   simplify' c@CheckMetaInst{}     = return c
   simplify' (CheckType t)         = CheckType <$> simplify' t
-  simplify' (UsableAtModality ms mod t) = flip UsableAtModality mod <$> simplify' ms <*> simplify' t
+  simplify' (UsableAtModality cc ms mod t) = flip (UsableAtModality cc) mod <$> simplify' ms <*> simplify' t
 
 instance Simplify CompareAs where
   simplify' (AsTermsOf a) = AsTermsOf <$> simplify' a
@@ -1287,7 +1287,7 @@ instance Normalise Constraint where
   normalise' (CheckDataSort q s)   = CheckDataSort q <$> normalise' s
   normalise' c@CheckMetaInst{}     = return c
   normalise' (CheckType t)         = CheckType <$> normalise' t
-  normalise' (UsableAtModality ms mod t) = flip UsableAtModality mod <$> normalise' ms <*> normalise' t
+  normalise' (UsableAtModality cc ms mod t) = flip (UsableAtModality cc) mod <$> normalise' ms <*> normalise' t
 
 instance Normalise CompareAs where
   normalise' (AsTermsOf a) = AsTermsOf <$> normalise' a
@@ -1522,7 +1522,7 @@ instance InstantiateFull Constraint where
     CheckDataSort q s   -> CheckDataSort q <$> instantiateFull' s
     c@CheckMetaInst{}   -> return c
     CheckType t         -> CheckType <$> instantiateFull' t
-    UsableAtModality ms mod t -> flip UsableAtModality mod <$> instantiateFull' ms <*> instantiateFull' t
+    UsableAtModality cc ms mod t -> flip (UsableAtModality cc) mod <$> instantiateFull' ms <*> instantiateFull' t
 
 instance InstantiateFull CompareAs where
   instantiateFull' (AsTermsOf a) = AsTermsOf <$> instantiateFull' a

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

@@ -1734,7 +1734,7 @@ fitsIn uc forceds t s = do
   withoutK <- withoutKOption
   when withoutK $ do
     q <- viewTC eQuantity
-    usableAtModality' (Just s) (setQuantity q defaultModality) (unEl t)
+    usableAtModality' (Just s) ConstructorType (setQuantity q defaultModality) (unEl t)
 
   fitsIn' withoutK forceds t s
   where

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

@@ -73,6 +73,7 @@ import Agda.Utils.Size
 import qualified Agda.Utils.SmallSet as SmallSet
 
 import Agda.Utils.Impossible
+import Agda.Utils.WithDefault
 
 ---------------------------------------------------------------------------
 -- * Definitions by pattern matching
@@ -680,7 +681,7 @@ checkClause
 
 checkClause t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
   cxtNames <- reverse . map (fst . unDom) <$> getContext
-  checkClauseLHS t withSub c $ \ lhsResult@(LHSResult npars delta ps absurdPat trhs patSubst asb psplit) -> do
+  checkClauseLHS t withSub c $ \ lhsResult@(LHSResult npars delta ps absurdPat trhs patSubst asb psplit ixsplit) -> do
         -- Note that we might now be in irrelevant context,
         -- in case checkLeftHandSide walked over an irrelevant projection pattern.
 
@@ -800,7 +801,7 @@ checkRHS
   -> A.RHS                   -- ^ Rhs to check.
   -> TCM (Maybe Term, WithFunctionProblem)
                                               -- Note: the as-bindings are already bound (in checkClause)
-checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb _) rhs0 =
+checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb _ _) rhs0 =
   handleRHS rhs0 where
 
   handleRHS :: A.RHS -> TCM (Maybe Term, WithFunctionProblem)
@@ -1016,7 +1017,7 @@ checkWithRHS
   -> [A.Clause]                        -- ^ With-clauses to check.
   -> TCM (Maybe Term, WithFunctionProblem)
                                 -- Note: as-bindings already bound (in checkClause)
-checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb _) vtys0 cs =
+checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb _ _) vtys0 cs =
   verboseBracket "tc.with.top" 25 "checkWithRHS" $ do
     Bench.billTo [Bench.Typing, Bench.With] $ do
         withArgs <- withArguments vtys0

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

@@ -92,6 +92,7 @@ import Agda.Utils.Size
 import Agda.Utils.Tuple
 
 import Agda.Utils.Impossible
+import Agda.Utils.WithDefault
 
 --UNUSED Liang-Ting Chen 2019-07-16
 ---- | Compute the set of flexible patterns in a list of patterns. The result is
@@ -639,17 +640,20 @@ data LHSResult = LHSResult
     -- (Issue 2303).
   , lhsPartialSplit :: IntSet
     -- ^ have we done a partial split?
+  , lhsIndexedSplit :: Bool
+    -- ^ have we split on an indexed type?
   }
 
 instance InstantiateFull LHSResult where
-  instantiateFull' (LHSResult n tel ps abs t sub as psplit) = LHSResult n
+  instantiateFull' (LHSResult n tel ps abs t sub as psplit ixsplit) = LHSResult n
     <$> instantiateFull' tel
     <*> instantiateFull' ps
     <*> instantiateFull' abs
     <*> instantiateFull' t
     <*> instantiateFull' sub
     <*> instantiateFull' as
     <*> pure psplit
+    <*> pure ixsplit
 
 -- | Check a LHS. Main function.
 --
@@ -688,7 +692,7 @@ checkLeftHandSide call f ps a withSub' strippedPats =
       eqs0 = zipWith3 ProblemEq (map namedArg cps) (map var $ downFrom $ size tel) (flattenTel tel)
 
   let finalChecks :: LHSState a -> TCM a
-      finalChecks (LHSState delta qs0 (Problem eqs rps _) b psplit) = do
+      finalChecks (LHSState delta qs0 (Problem eqs rps _) b psplit ixsplit) = do
 
         reportSDoc "tc.lhs.top" 20 $ vcat
           [ "lhs: final checks with remaining equations"
@@ -701,6 +705,12 @@ checkLeftHandSide call f ps a withSub' strippedPats =
         addContext delta $ do
           mapM_ noShadowingOfConstructors eqs
 
+          -- If we're working --without-K, then we have to check the
+          withoutK <- collapseDefault . optWithoutK <$> pragmaOptions
+          mod <- asksTC getModality
+          when (withoutK && ixsplit) $
+            usableAtModality IndexedClause mod (unEl (unArg b))
+
         arity_a <- arityPiPath a
         -- Compute substitution from the out patterns @qs0@
         let notProj ProjP{} = False
@@ -768,7 +778,7 @@ checkLeftHandSide call f ps a withSub' strippedPats =
 
         let hasAbsurd = not . null $ absurds
 
-        let lhsResult = LHSResult (length cxt) delta qs hasAbsurd b patSub asb (IntSet.fromList $ catMaybes psplit)
+        let lhsResult = LHSResult (length cxt) delta qs hasAbsurd b patSub asb (IntSet.fromList $ catMaybes psplit) ixsplit
 
         -- Debug output
         reportSDoc "tc.lhs.top" 10 $
@@ -861,15 +871,15 @@ checkLHS
 checkLHS mf = updateModality checkLHS_ where
     -- If the target type is irrelevant or in Prop,
     -- we need to check the lhs in irr. cxt. (see Issue 939).
- updateModality cont st@(LHSState tel ip problem target psplit) = do
+ updateModality cont st@(LHSState tel ip problem target psplit _) = do
       let m = getModality target
       applyModalityToContext m $ do
         cont $ over (lhsTel . listTel)
                  (map $ inverseApplyModalityButNotQuantity m) st
         -- Andreas, 2018-10-23, issue #3309
         -- the modalities in the clause telescope also need updating.
 
- checkLHS_ st@(LHSState tel ip problem target psplit) = do
+ checkLHS_ st@(LHSState tel ip problem target psplit ixsplit) = do
   reportSDoc "tc.lhs" 40 $ "tel is" <+> prettyTCM tel
   reportSDoc "tc.lhs" 40 $ "ip is" <+> pretty ip
   reportSDoc "tc.lhs" 40 $ "target is" <+> addContext tel (prettyTCM target)
@@ -984,7 +994,7 @@ checkLHS mf = updateModality checkLHS_ where
           ip'      = ip ++ [projP]
           -- drop the projection pattern (already splitted)
           problem' = over problemRestPats tail problem
-      liftTCM $ updateLHSState (LHSState tel ip' problem' target' psplit)
+      liftTCM $ updateLHSState (LHSState tel ip' problem' target' psplit ixsplit)
 
 
     -- Split a Partial.
@@ -1144,7 +1154,7 @@ checkLHS mf = updateModality checkLHS_ where
       -- Compute the new state
       let problem' = set problemEqs eqs' problem
       reportSDoc "tc.lhs.split.partial" 60 $ text (show problem')
-      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' (psplit ++ [Just o_n]))
+      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' (psplit ++ [Just o_n]) ixsplit)
 
 
     splitLit :: Telescope      -- The types of arguments before the one we split on
@@ -1183,7 +1193,7 @@ checkLHS mf = updateModality checkLHS_ where
 
       -- Compute the new state
       let problem' = set problemEqs eqs' problem
-      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' psplit)
+      liftTCM $ updateLHSState (LHSState delta' ip' problem' target' psplit ixsplit)
 
 
     splitCon :: Telescope      -- The types of arguments before the one we split on
@@ -1438,7 +1448,7 @@ checkLHS mf = updateModality checkLHS_ where
 
           -- if rest type reduces,
           -- extend the split problem by previously not considered patterns
-          st' <- liftTCM $ updateLHSState $ LHSState delta' ip' problem' target'' psplit
+          st' <- liftTCM $ updateLHSState $ LHSState delta' ip' problem' target'' psplit (ixsplit || not (null ixs))
 
           reportSDoc "tc.lhs.top" 12 $ sep
             [ "new problem from rest"