The following code is accepted by Agda 2.7.0.1, but not by Agda 2.8.0-50c9f1f:
{-# OPTIONS --hidden-argument-puns #-}
open import Agda.Builtin.Equality
record R₁ (F : Set → Set) : Set₁ where
field
f : {A : Set} → F A → A
record R₂ (A : Set) : Set where
field
x : A
record R₃ (A : Set) : Set where
field
x : A
r : R₂ A
r = record { x = x }
instance
r₂ : R₁ R₂
r₂ = record { f = R₂.x }
r₃ : R₁ R₃
r₃ = record { f = R₃.x }
P :
{A : Set} {F₁ F₂ : Set → Set} ⦃ r₁ : R₁ F₁ ⦄ ⦃ r₂ : R₁ F₂ ⦄ →
F₁ A → F₂ A → Set
P ⦃ r₁ ⦄ ⦃ r₂ ⦄ x y = R₁.f r₁ x ≡ R₁.f r₂ y
Q :
{F₁ F₂ : Set → Set} ⦃ r₁ : R₁ F₁ ⦄ ⦃ r₂ : R₁ F₂ ⦄
(A : Set) → (F₁ A → F₂ A) → Set
Q {F₁} A f = (x : F₁ A) → P (f x) x
opaque
_ : (A : Set) → Q A R₃.r
_ = λ _ _ → refl
_F₁_36 : Set → Set [ at […]:40.19-20 ]
_F₂_37 : Set → Set [ at […]:40.19-20 ]
_r₁_38 : R₁ _F₁_36 [ at […]:40.19-20 ]
_r₂_39 : R₁ _F₂_37 [ at […]:40.19-20 ]
_A_40 : Set [ at […]:40.23-27 ]
———— Error —————————————————————————————————————————————————
error: [UnsolvedConstraints]
Failed to solve the following constraints:
Resolve instance argument _r₂_39 : R₁ _F₂_37
Candidates
r₂ : R₁ R₂
r₃ : R₁ R₃
(stuck)
Resolve instance argument _r₁_38 : R₁ _F₁_36
Candidates
r₂ : R₁ R₂
r₃ : R₁ R₃
(stuck)
R₁.f (_r₂_39 (A = A)) (R₃.r x) = R₁.f (_r₁_38 (A = A)) x : A
(blocked on any(_r₁_38, _r₂_39))
_F₁_36 A =< R₃ _A_40 (blocked on _F₁_36)
R₂ _A_40 =< _F₂_37 A (blocked on _F₂_37)
@plt-amy, is this change intended?
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4