[ fix agda#5681 ] Add postponed fibrancy check to UsableAtModality co…

…nstraint

src/full/Agda/Interaction/BasicOps.hs

@@ -48,7 +48,7 @@ import Agda.Syntax.Parser
 import Agda.TheTypeChecker
 import Agda.TypeChecking.Constraints
 import Agda.TypeChecking.Conversion
-import Agda.TypeChecking.Errors ( getAllWarnings, stringTCErr )
+import Agda.TypeChecking.Errors ( getAllWarnings, stringTCErr, Verbalize(..) )
 import Agda.TypeChecking.Monad as M hiding (MetaInfo)
 import Agda.TypeChecking.MetaVars
 import Agda.TypeChecking.MetaVars.Mention
@@ -485,7 +485,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) =
@@ -540,7 +540,7 @@ instance (Pretty a, Pretty b) => Pretty (OutputConstraint a b) where
              -- , nest 2 "stuck because" <?> pretty err ] -- We don't have Pretty for TCErr
       DataSort q s         -> "Sort" <+> pretty s <+> "allows data/record definitions"
       CheckLock t lk       -> "Check lock" <+> pretty lk <+> "allows" <+> pretty t
-      UsableAtMod mod t    -> "Is usable at" <+> pretty mod <+> pretty t
+      UsableAtMod mod t    -> "Is usable at" <+> text (verbalize mod) <+> "modality:" <+> pretty t
     where
       bin a op b = sep [a, nest 2 $ op <+> b]
       pcmp cmp a b = bin (pretty a) (pretty cmp) (pretty b)
@@ -658,7 +658,7 @@ getConstraintsMentioning norm m = getConstrs instantiateBlockingFull (mentionsMe
         CheckMetaInst{}            -> Nothing
         CheckType t                -> isMeta (unEl t)
         CheckLockedVars t _ _ _    -> isMeta t
-        UsableAtModality _ t       -> isMeta t
+        UsableAtModality _ _ t     -> isMeta t
 
     isMeta (MetaV m' es_m)
       | m == m' = Just es_m

src/full/Agda/TypeChecking/Constraints.hs

@@ -301,7 +301,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 mod t) = usableAtModality mod t
+solveConstraint_ (UsableAtModality c mod t) = usableAtModality' c mod t
 
 checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term
 checkTypeCheckingProblem = \case

src/full/Agda/TypeChecking/Errors.hs

@@ -17,6 +17,7 @@ module Agda.TypeChecking.Errors
   , dropTopLevelModule
   , topLevelModuleDropper
   , stringTCErr
+  , Verbalize(verbalize)
   ) where
 
 import Prelude hiding ( null, foldl )
@@ -1412,6 +1413,13 @@ instance Verbalize Cohesion where
       Continuous -> "continuous"
       Squash     -> "squashed"
 
+instance Verbalize Modality where
+  verbalize mod | mod == defaultModality = "default"
+  verbalize (Modality rel qnt coh) = intercalate "," $
+    [ verbalize rel | rel /= defaultRelevance ] ++
+    [ verbalize qnt | qnt /= defaultQuantity ] ++
+    [ verbalize coh | coh /= defaultCohesion ]
+
 -- | Indefinite article.
 data Indefinite a = Indefinite a
 

src/full/Agda/TypeChecking/Irrelevance.hs

@@ -480,14 +480,19 @@ 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 => TCM Bool -> Modality -> Term -> TCM ()
+usableAtModality' c mod t = catchConstraint (UsableAtModality c mod t) $ do
+  whenM c $ 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 mod t = catchConstraint (UsableAtModality mod t) $ 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 = usableAtModality' $ pure True
 
 
 -- * Propositions

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

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

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

@@ -1137,7 +1137,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 Modality Term   -- ^ is the term usable at the given modality?
+  | UsableAtModality (TCM Bool) Modality Term   -- ^ is the term usable at the given modality? (Only runs this check if the given computation returns @True@)
   deriving (Show, Generic)
 
 instance HasRange Constraint where
@@ -1173,7 +1173,7 @@ instance Free Constraint where
       CheckDataSort _ s     -> freeVars' s
       CheckMetaInst m       -> mempty
       CheckType t           -> freeVars' t
-      UsableAtModality mod t -> freeVars' t
+      UsableAtModality c mod t -> freeVars' t
 
 instance TermLike Constraint where
   foldTerm f = \case
@@ -1194,10 +1194,16 @@ instance TermLike Constraint where
       CheckDataSort _ s      -> foldTerm f s
       CheckMetaInst m        -> mempty
       CheckType t            -> foldTerm f t
-      UsableAtModality m t   -> foldTerm f t
+      UsableAtModality c m t -> foldTerm f t
 
   traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented
 
+instance NFData (TCM a) where
+  rnf _ = ()
+
+instance Show (TCM a) where
+  show _ = ""
+
 instance AllMetas Constraint
 
 data Comparison = CmpEq | CmpLeq

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 mod t -> "Is usable at" <+> prettyTCM mod <+> ":" <+> prettyTCM t
+        UsableAtModality _ mod t -> "Is usable at" <+> text (verbalize mod) <+> "modality:" <+> prettyTCM t
 
       where
         prettyCmp

src/full/Agda/TypeChecking/Reduce.hs

@@ -276,7 +276,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 mod t) = UsableAtModality mod <$> instantiate' t
+  instantiate' (UsableAtModality c mod t) = UsableAtModality c mod <$> instantiate' t
 
 instance Instantiate CompareAs where
   instantiate' (AsTermsOf a) = AsTermsOf <$> instantiate' a
@@ -887,7 +887,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 mod t) = UsableAtModality mod <$> reduce' t
+  reduce' (UsableAtModality c mod t) = UsableAtModality c mod <$> reduce' t
 
 instance Reduce CompareAs where
   reduce' (AsTermsOf a) = AsTermsOf <$> reduce' a
@@ -1054,7 +1054,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 mod t) = UsableAtModality mod <$> simplify' t
+  simplify' (UsableAtModality c mod t) = UsableAtModality c mod <$> simplify' t
 
 instance Simplify CompareAs where
   simplify' (AsTermsOf a) = AsTermsOf <$> simplify' a
@@ -1236,7 +1236,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 mod t) = UsableAtModality mod <$> normalise' t
+  normalise' (UsableAtModality c mod t) = UsableAtModality c mod <$> normalise' t
 
 instance Normalise CompareAs where
   normalise' (AsTermsOf a) = AsTermsOf <$> normalise' a
@@ -1471,7 +1471,7 @@ instance InstantiateFull Constraint where
     CheckDataSort q s   -> CheckDataSort q <$> instantiateFull' s
     c@CheckMetaInst{}   -> return c
     CheckType t         -> CheckType <$> instantiateFull' t
-    UsableAtModality mod t -> UsableAtModality mod <$> instantiateFull' t
+    UsableAtModality c mod t -> UsableAtModality c mod <$> instantiateFull' t
 
 instance InstantiateFull CompareAs where
   instantiateFull' (AsTermsOf a) = AsTermsOf <$> instantiateFull' a

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

@@ -1732,9 +1732,9 @@ fitsIn uc forceds t s = do
   -- noConstraints $ s' `leqSort` s
 
   withoutK <- withoutKOption
-  when withoutK $ whenM (isFibrant s) $ do
+  when withoutK $ do
     q <- viewTC eQuantity
-    usableAtModality (setQuantity q defaultModality) (unEl t)
+    usableAtModality' (isFibrant s) (setQuantity q defaultModality) (unEl t)
 
   fitsIn' withoutK forceds t s
   where

src/full/Agda/TypeChecking/Substitute.hs

@@ -1008,7 +1008,7 @@ instance Subst Constraint where
     CheckDataSort q s        -> CheckDataSort q (rf s)
     CheckMetaInst m          -> CheckMetaInst m
     CheckType t              -> CheckType (rf t)
-    UsableAtModality mod m   -> UsableAtModality mod (rf m)
+    UsableAtModality c mod m   -> UsableAtModality c mod (rf m)
     where
       rf :: forall a. TermSubst a => a -> a
       rf x = applySubst rho x

test/Fail/Issue5681.agda

@@ -0,0 +1,3 @@
+{-# OPTIONS --without-K #-}
+
+record foo : {!!} where

test/Fail/Issue5681.err

@@ -0,0 +1,7 @@
+Failed to solve the following constraints:
+  Sort _2 of foo admits data/record definitions. (blocked on _2)
+  Is usable at default modality: foo (blocked on _2)
+Unsolved metas at the following locations:
+  Issue5681.agda:3,8-11
+Unsolved interaction metas at the following locations:
+  Issue5681.agda:3,14-18