[ fix #5805 ] Catch pattern violations in checkType

src/full/Agda/TypeChecking/CheckInternal.hs

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

test/Fail/Issue5805.agda

@@ -0,0 +1,31 @@
+open import Agda.Builtin.Equality
+
+cong : ∀{a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
+cong f refl = refl
+
+record Category : Set₂ where
+  field
+    Ob  : Set₁
+    _⇒_ : Ob → Ob → Set
+    _∘_ : ∀ {O P Q} → P ⇒ Q → O ⇒ P → O ⇒ Q
+
+  -- Moving this out of the record fixes the problem.
+  idem : {X : Ob} → X ⇒ X → Set₁
+  idem {X} f = f ∘ f ≡ f → Set
+
+Sets : Category
+Sets = record
+    { Ob = Set
+    ; _⇒_ = {!!}
+    ; _∘_ = λ f g x → f (g x)
+    }
+open Category Sets
+
+postulate
+  Y : Ob
+  f : Y ⇒ Y
+
+idem-f : idem {X = _} f  -- Solving the _ fixes the problem
+idem-f ff≡f
+  with ffx≡fx ← cong {!!} ff≡f
+  = Y

test/Fail/Issue5805.err

@@ -0,0 +1,8 @@
+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