Issues

• Testsuite latex/html: do not allow to overwrite golden value when Agda run fails

  infra: test suite
  agda/agda#8909 · Filter by author andreasabel opened on Nov 11, 2026

• Cmd_infer_toplevel forgets module parameters after loading from .agdai

  checkpointsux: interaction
  Bug

  agda/agda#8905 · Filter by author banacorn opened on Nov 10, 2026 · 2.10.0

• What is DoubleDot notation

  irrelevancemodalitiesshape-irrelevanceuser-manual
  agda/agda#8903 · Filter by author L-TChen opened on Nov 10, 2026
  5

• primShowChar / primShowString give different strings in the type checker, the GHC backend and the JS backend

  backend: jsbug or feature?builtinliteralstype: bug
  agda/agda#8902 · Filter by author Ode-to-a-Nightingale opened on Nov 10, 2026
  1

• Deprecate Floats

  floattype: discussionwarning-on-usage
  agda/agda#8901 · Filter by author lawcho opened on Nov 9, 2026
  5

• Record fields with shared type declaration and interation metas trigger __IMPOSSIBLE__, called at MetaVars.hs:482:11

  agda/agda#8900 · Filter by author shhyou opened on Nov 9, 2026
  2

• JS backend: primFloatToRatio is approximate and primFloatToWord64 throws, unlike the type checker and the GHC backend

  backend: ghcbackend: jsbackendsfloattype: bug
  agda/agda#8899 · Filter by author Ode-to-a-Nightingale opened on Nov 8, 2026
  2

• Builtin imports fail with "COMPILE pragma not allowed in safe mode" when the data directory's lib or lib/prim is a symlink

  agda/agda#8897 · Filter by author scks1 opened on Nov 7, 2026

• opaque unfolding and REWRITE rules breaks subject reduction

  confluenceopaquesubject reduction
  agda/agda#8893 · Filter by author TOTBWF opened on Nov 5, 2026
  4

• Warning that has been turned off is reported

  PR welcometype: bugux: warnings
  agda/agda#8886 · Filter by author nad opened on Nov 1, 2026 · later
  2

• 2.8.0: slow "undefined" report

  status: MWE needed
  agda/agda#8885 · Filter by author mechvel opened on Oct 31, 2026
  3

• Bulk hidden arguments

  hidden argumentstype: enhancement
  agda/agda#8872 · Filter by author andreasabel opened on Oct 22, 2026 · 2.10.0
  1

• Opaque control from reflection API

  opaquereflectiontype: enhancement
  agda/agda#8861 · Filter by author jespercockx opened on Oct 21, 2026

• Control over reduction during elaboration

  performancetype: discussiontype: enhancement
  agda/agda#8860 · Filter by author jespercockx opened on Oct 21, 2026
  4

• macOS deploy broken (macos-26-arm64, image version 20261013.0424.1)

  infra: github workflowsupstream
  agda/agda#8845 · Filter by author andreasabel opened on Oct 16, 2026 · 2.10.0
  5

• Macro defined in a module does not respect parameter binding

  parametersreflection
  agda/agda#8844 · Filter by author ashinkarov opened on Oct 15, 2026
  1

• Incorrect warning location detection

  agda-modetype: bugux: emacs
  agda/agda#8839 · Filter by author nad opened on Oct 14, 2026 · 2.10.0
  5

  

• Add std-lib-meta to ecosystem tests

  ecoysteminfra: test suitetype: enhancement
  agda/agda#8836 · Filter by author jespercockx opened on Oct 14, 2026 · 2.10.0
  1

  

• Sized types (successor style): semi-continuity check not implemented

  falsesized typessized-types-suc
  agda/agda#8829 · Filter by author andreasabel opened on Oct 11, 2026
  

• When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?

  injectivitytype: enhancementux: error reporting
  agda/agda#8814 · Filter by author andreasabel opened on Oct 6, 2026

• Improve "refine" interactive command: currently fails with more than 10 arguments

  type: enhancementux: interaction
  agda/agda#8813 · Filter by author andreasabel opened on Oct 6, 2026

• Better error reporting for failed meta instantiations

  metaux: error reporting
  agda/agda#8796 · Filter by author jespercockx opened on Oct 1, 2026 · 2.10.0
  

• ClashesViaRenaming too strict

  difficulty: easyimportux: warnings
  agda/agda#8786 · Filter by author andreasabel opened on Sep 27, 2026

• Positivity checker loses information through module applications

  polaritypositivitytype: enhancement
  agda/agda#8773 · Filter by author andreasabel opened on Sep 24, 2026 · 2.10.0
  1

  

• The strict GHC backend generates code that segfaults

  backend: ghcghc issueupstream
  agda/agda#8764 · Filter by author nad opened on Sep 20, 2026 · 2.10.0
  6