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

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

Possible regression in 2.8.0-rc1 using reflection (maybe related to instance resolution) · Issue #7883 · agda/agda · GitHub

Using:

Agda version 2.7.20250510
Built with flags (cabal -f)
 - enable-cluster-counting: unicode cluster counting in LaTeX backend using the ICU library
 - optimise-heavily: extra optimisations

the following code:

module Example where

open import Agda.Builtin.Nat
  renaming (Nat to ℕ)
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Sigma

infixr 4 _×_
_×_ : Set → Set → Set 
A × B =  Σ A λ _ → B

record HasCast (A : Set) (B : Set) : Set where
  field
    cast : A → B

open HasCast ⦃...⦄ public

record Nat : Set where
  constructor mkNat
  field
    theNat : ℕ

instance
  HasCast-Nat : HasCast (ℕ × ℕ) Nat
  HasCast-Nat .HasCast.cast x = mkNat (fst x)

  HasCast-id : ∀ {A : Set} → HasCast A A
  HasCast-id .cast x = x

variable
  n : Nat

data D : Nat → Set where
  DC : let open Nat n in D (cast (1 , theNat ))

def-Z : (n : Name) → TC ⊤
def-Z n =
  quoteTC 0 >>= λ zero →
  getType (quote DC) >>= λ ty →
  normalise ty >>= λ _ →
  defineFun n
    ( clause
      []
      []
      zero
    ∷ [])
  where _>>=_ = bindTC

Z : ℕ
unquoteDef Z = def-Z Z

fails to typecheck with the following error:

Checking Example (/tmp/Example.agda).
/tmp/Example.agda:53.1-23: error: [CannotApply]
Expression used as function but does not have function type:
  expr: Example.GeneralizeTel.constructor
  type: Example.GeneralizeTel
when checking that n is a valid argument to a function of type
{n = n₁ : Nat} → Example.GeneralizeTel

Using Agda 2.7.0.1 it typechecks just fine.

I found some alternative ways of changing the code to avoid getting the error:

1. Comment out the call to normalise in def-Z
2. Remove the instance HasCast-id from scope
3. Remove let open Nat n in and make theNat an implicit argument in the body of DC
4. Remove the use of theNat from the body of DC
5. Change the order of arguments to cast in the body of DC, that is, to cast (theNat , 1)

This issue might be related to #7847 and #7882.

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