Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/6976 below:

Unexpected failure of instance resolution · Issue #6976 · agda/agda · GitHub

The changelog for 2.6.4 mentions:

[Breaking] The algorithm for resolution of instance arguments has been simplified. It will now only rely on the type of instances to determine which candidate it should use, and no longer on their values.

Alas the following example shows a regression w.r.t. Agda-2.6.3; maybe the algorithm has been over-simplified?

module FILE1 where

_∋_ : (A : Set) → A → A
A ∋ x = x

it : {A : Set} → ⦃ A ⦄ → A
it ⦃ x ⦄ = x

postulate DecidableEquality : Set → Set

record DecEq (A : Set) : Set where
  field _≟_ : DecidableEquality A

module M where
  postulate A : Set; _≟_ : DecidableEquality A

instance
  -- DecEq-A : DecEq _
  DecEq-A = DecEq _ ∋ record {M}
    where putAnythingHere!! = Set

-- _ = DecEq A ∋ it where open M

-- FILE2
open import FILE1

_ = DecEq A ∋ it where open M

<MY_PATH>.agda:3,18-20
No instance of type DecEq A was found in scope.
when checking that the expression it has type DecEq A

Here are a couple of ways to make the error go away:

1. Include the (commented) DecEq : _ type signature, surely related to the changelog.
2. Include (an identical copy of) the unit test in FILE1. Somehow, triggering instance resolution in the initial module "assigns" the type to DecEq-A and afterwards the same example succeeds in FILE2! Very weird indeed.
   EDIT: In fact, putting any piece of code (e.g. _ = Set) at the end of FILE1 works :S
3. Removing the anything-goes where clause surprisingly works!

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