If attempting instance search while checking an instance definition with an as yet unknown type, we throw a hard error instead of postponing the search:
open import Agda.Builtin.Nat
record Countable (A : Set) : Set₁ where
field
count : A → Nat
open Countable ⦃ ... ⦄
mkCountable : (A : Set) → (A → Nat) → Countable A
mkCountable A c .count = c
T : (A : Set) → ⦃ Countable A ⦄ → Set
T A = A
instance
iN = mkCountable Nat λ n → n
works = mkCountable (T Nat) λ n → n
instance
fails = mkCountable (T Nat) λ n → n
-- There are instances whose type is still unsolved
-- when checking that Nat is a valid argument to a function of type
-- (A : Set) ⦃ _ : Countable A ⦄ → Set
The error is thrown here:
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