[ re agda#5805 ] Create constraint instead of hard error in checkType

This fixes the issue when I load Issue5805.agda in Emacs, but
when I run `make test` it somehow throws a pattern violation again.

src/full/Agda/Interaction/BasicOps.hs

@@ -482,6 +482,7 @@ instance Reify Constraint where
     reify (CheckMetaInst m) = do
       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
 
 instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
@@ -650,6 +651,7 @@ getConstraintsMentioning norm m = getConstrs instantiateBlockingFull (mentionsMe
         HasPTSRule a b             -> Nothing
         UnquoteTactic{}            -> Nothing
         CheckMetaInst{}            -> Nothing
+        CheckType t                -> isMeta (unEl t)
         CheckLockedVars t _ _ _    -> isMeta t
         UsableAtModality _ t       -> isMeta t
 

src/full/Agda/TypeChecking/CheckInternal.hs

@@ -57,9 +57,8 @@ type MonadCheckInternal m = MonadConversion m
 
 -- | Entry point for e.g. checking WithFunctionType.
 checkType :: (MonadCheckInternal m) => Type -> m ()
-checkType t = do
-  let err = typeError $ InvalidType $ unEl t
-  inferred <- catchPatternErr (\_ -> err) $ checkType' t
+checkType t = catchConstraint (CheckType t) $ do
+  inferred <- checkType' t
   equalSort (getSort t) inferred
 
 -- | Check a type and infer its sort.

src/full/Agda/TypeChecking/Constraints.hs

@@ -32,6 +32,7 @@ import {-# SOURCE #-} Agda.TypeChecking.Conversion
 import {-# SOURCE #-} Agda.TypeChecking.MetaVars
 import {-# SOURCE #-} Agda.TypeChecking.Empty
 import {-# SOURCE #-} Agda.TypeChecking.Lock
+import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType )
 
 import Agda.Utils.CallStack ( withCurrentCallStack )
 import Agda.Utils.Functor
@@ -297,6 +298,7 @@ solveConstraint_ (CheckLockedVars a b c d)   = checkLockedVars a b c d
 solveConstraint_ (HasBiggerSort a)      = hasBiggerSort a
 solveConstraint_ (HasPTSRule a b)       = hasPTSRule a b
 solveConstraint_ (CheckMetaInst m)      = checkMetaInst m
+solveConstraint_ (CheckType t)          = checkType t
 solveConstraint_ (UsableAtModality mod t) = usableAtModality mod t
 
 checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term

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

@@ -119,6 +119,7 @@ instance MentionsMeta Constraint where
     HasPTSRule a b      -> mm (a, b)
     UnquoteTactic tac hole goal -> False
     CheckMetaInst m     -> True   -- TODO
+    CheckType t         -> mm t
     CheckLockedVars a b c d -> mm ((a, b), (c, d))
     UsableAtModality mod t -> mm t
     where

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

@@ -1111,6 +1111,7 @@ data Constraint
   | HasBiggerSort Sort
   | HasPTSRule (Dom Type) (Abs Sort)
   | CheckMetaInst MetaId
+  | CheckType Type
   | UnBlock MetaId
     -- ^ Meta created for a term blocked by a postponed type checking problem or unsolved
     --   constraints. The 'MetaInstantiation' for the meta (when unsolved) is either 'BlockedConst'
@@ -1160,6 +1161,7 @@ instance Free Constraint where
       CheckLockedVars a b c d -> freeVars' ((a,b),(c,d))
       UnquoteTactic t h g   -> freeVars' (t, (h, g))
       CheckMetaInst m       -> mempty
+      CheckType t           -> freeVars' t
       UsableAtModality mod t -> freeVars' t
 
 instance TermLike Constraint where
@@ -1179,6 +1181,7 @@ instance TermLike Constraint where
       HasBiggerSort s        -> foldTerm f s
       HasPTSRule a s         -> foldTerm f (a, Sort <$> s)
       CheckMetaInst m        -> mempty
+      CheckType t            -> foldTerm f t
       UsableAtModality m t   -> foldTerm f t
 
   traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented

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

@@ -210,6 +210,7 @@ addConstraintTo bucket unblock c = do
       CheckFunDef{}    -> True
       UnquoteTactic{}  -> True
       CheckMetaInst{}  -> True
+      CheckType{}      -> True
       CheckLockedVars{} -> True
       UsableAtModality{} -> True
 

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

@@ -406,6 +406,7 @@ constraintMetas = \case
       HasBiggerSort{}          -> return mempty
       HasPTSRule{}             -> return mempty
       CheckMetaInst x          -> return mempty
+      CheckType t              -> return $ allMetas Set.singleton t
       CheckLockedVars a b c d  -> return $ allMetas Set.singleton (a, b, c, d)
       UsableAtModality{}       -> return mempty
   where

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

@@ -151,6 +151,8 @@ instance PrettyTCM Constraint where
           case mvJudgement m of
             HasType{ jMetaType = t } -> prettyTCM x <+> ":" <+> prettyTCM t
             IsSort{} -> prettyTCM x <+> "is a sort"
+        CheckType t ->
+          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

src/full/Agda/TypeChecking/Reduce.hs

@@ -274,6 +274,7 @@ instance Instantiate Constraint where
     CheckLockedVars <$> instantiate' a <*> instantiate' b <*> instantiate' c <*> instantiate' d
   instantiate' (UnquoteTactic t h g) = UnquoteTactic <$> instantiate' t <*> instantiate' h <*> instantiate' g
   instantiate' c@CheckMetaInst{}    = return c
+  instantiate' (CheckType t)        = CheckType <$> instantiate' t
   instantiate' (UsableAtModality mod t) = UsableAtModality mod <$> instantiate' t
 
 instance Instantiate CompareAs where
@@ -883,6 +884,7 @@ instance Reduce Constraint where
   reduce' (CheckLockedVars a b c d) =
     CheckLockedVars <$> reduce' a <*> reduce' b <*> reduce' c <*> reduce' d
   reduce' c@CheckMetaInst{}     = return c
+  reduce' (CheckType t)         = CheckType <$> reduce' t
   reduce' (UsableAtModality mod t) = UsableAtModality mod <$> reduce' t
 
 instance Reduce CompareAs where
@@ -1048,6 +1050,7 @@ instance Simplify Constraint where
   simplify' (CheckLockedVars a b c d) =
     CheckLockedVars <$> simplify' a <*> simplify' b <*> simplify' c <*> simplify' d
   simplify' c@CheckMetaInst{}     = return c
+  simplify' (CheckType t)         = CheckType <$> simplify' t
   simplify' (UsableAtModality mod t) = UsableAtModality mod <$> simplify' t
 
 instance Simplify CompareAs where
@@ -1228,6 +1231,7 @@ instance Normalise Constraint where
   normalise' (CheckLockedVars a b c d) =
     CheckLockedVars <$> normalise' a <*> normalise' b <*> normalise' c <*> normalise' d
   normalise' c@CheckMetaInst{}     = return c
+  normalise' (CheckType t)         = CheckType <$> normalise' t
   normalise' (UsableAtModality mod t) = UsableAtModality mod <$> normalise' t
 
 instance Normalise CompareAs where
@@ -1461,6 +1465,7 @@ instance InstantiateFull Constraint where
     CheckLockedVars a b c d ->
       CheckLockedVars <$> instantiateFull' a <*> instantiateFull' b <*> instantiateFull' c <*> instantiateFull' d
     c@CheckMetaInst{}   -> return c
+    CheckType t         -> CheckType <$> instantiateFull' t
     UsableAtModality mod t -> UsableAtModality mod <$> instantiateFull' t
 
 instance InstantiateFull CompareAs where

src/full/Agda/TypeChecking/Substitute.hs

@@ -995,6 +995,7 @@ instance Subst Constraint where
     CheckLockedVars a b c d  -> CheckLockedVars (rf a) (rf b) (rf c) (rf d)
     UnquoteTactic t h g      -> UnquoteTactic (rf t) (rf h) (rf g)
     CheckMetaInst m          -> CheckMetaInst m
+    CheckType t              -> CheckType (rf t)
     UsableAtModality mod m   -> UsableAtModality mod (rf m)
     where
       rf :: forall a. TermSubst a => a -> a

test/Fail/Issue5805.err

@@ -1,8 +1 @@
-Issue5805.agda:29,1-31,6
-(ff≡f : (_65 ∘ _65) ≡ _65) →
-?1 (ff≡f = ff≡f) (λ x → _65 (_65 x)) ≡ ?1 (ff≡f = ff≡f) _65 → Set
-is not a valid type
-when checking that the type
-(ff≡f : (_65 ∘ _65) ≡ _65) →
-?1 (ff≡f = ff≡f) (λ x → _65 (_65 x)) ≡ ?1 (ff≡f = ff≡f) _65 → Set
-of the generated with function is well-formed
+Panic: uncaught pattern violation