Closed
Description
The following code is accepted by Agda:
{-# OPTIONS --erasure #-}
postulate
f : (P : Set → Set₁) → (A : Set) → P A
works : (A : Set) → @0 A → Set
works = f _However, Agda fails to infer the value of the final underscore in the following variant of the code:
{-# OPTIONS --erasure #-}
postulate
f : (P : @0 Set → Set₁) → (A : Set) → P A
fails : (A : Set) → @0 A → Set
fails = f __P_2 : @0 Set → Set₁ [ at […]:7,11-12 ]
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
_P_2 A =< @0 A → Set (blocked on _P_2)
The problem can be fixed by replacing the underscore by (λ _ → @0 _ → _):
{-# OPTIONS --erasure #-}
postulate
f : (P : @0 Set → Set₁) → (A : Set) → P A
works : (A : Set) → @0 A → Set
works = f (λ _ → @0 _ → _)For some reason Agda fails to solve the constraint _P_2 A =< @0 A → Set.
I could seemingly fix the problem by tweaking the following code:
agda/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
Lines 718 to 720 in c0d263e
New code:
occurs (Dom info n f t x) =
Dom info n f t <$> underQuantity info (occurs x)I don't think a similar change should be performed for irrelevance, because the following code is rejected:
F : .(A : Set) → Set₁
F A = .A → SetI also left the cohesion component of the modality unchanged, because I know too little about cohesion.