Skip to content

Issues: agda/agda

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
28 Open 162 Closed
28 Open 162 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Hole/postulate asymmetry in @++ checker meta Metavariables, insertion of implicit arguments, etc modalities polarity positivity Positivity checking for data-type definitions postulate Concerning postulates.
#7205 opened Mar 27, 2024 by lawcho
Unsolved metas when inferring type signatures in mutual block meta Metavariables, insertion of implicit arguments, etc mutual type: bug Issues and pull requests about actual bugs
#7028 opened Dec 13, 2023 by omelkonian
1
Regression related to instance resolution meta Metavariables, insertion of implicit arguments, etc occurs check Problems with checking that metavariable solutions aren't loopy regression on master Unreleased regression in development version (Change to "regression in ..." should it be released!)
#6700 opened Jun 24, 2023 by nad 2.7.0
@jespercockx
7
Occurs check does not properly handle singleton type eta η-expansion of metavariables and unification modulo η meta Metavariables, insertion of implicit arguments, etc occurs check Problems with checking that metavariable solutions aren't loopy singleton-types Issues related to conversion modulo eta-equality for singleton types type: bug Issues and pull requests about actual bugs
#5837 opened Mar 18, 2022 by jespercockx 2.8.0
2
@jespercockx
22
Document the different uses of _ help wanted meta Metavariables, insertion of implicit arguments, etc ux: documentation Issues relating to Agda's documentation
#5704 opened Dec 22, 2021 by jespercockx later
5
Report warnings right away, not at the end of the file meta Metavariables, insertion of implicit arguments, etc type: enhancement Issues and pull requests about possible improvements ux: warnings Issues relating to the reporting of warnings
#5306 opened Apr 7, 2021 by nad icebox
7
Agda infers types that are not unique hidden arguments Insertion of hidden arguments and implicit lambdas meta Metavariables, insertion of implicit arguments, etc type: bug Issues and pull requests about actual bugs
#5304 opened Apr 6, 2021 by nad later
2
Allow let-aliasing of unambiguous data constructors? constructors Inductive constructors let Issues relating to let expressions meta Metavariables, insertion of implicit arguments, etc type: enhancement Issues and pull requests about possible improvements
#5274 opened Mar 12, 2021 by berndlosert icebox
5
Cyclic metavariable should raise error, not unsolved constraints meta Metavariables, insertion of implicit arguments, etc occurs check Problems with checking that metavariable solutions aren't loopy type: enhancement Issues and pull requests about possible improvements
#4153 opened Oct 22, 2019 by jespercockx icebox
Functions with beta-equal types lead in one case only to unsolved meta-variables ambiguous-constructors Issues to do with constructor disambiguation meta Metavariables, insertion of implicit arguments, etc overloading Overloaded projections; Projection disambiguation type: bug Issues and pull requests about actual bugs
#3562 opened Feb 13, 2019 by gallais later
3
Loading a file with --allow-unsolved-metas should create an interface file allow-unsolved-metas Issues relating to allow-unsolved-metas import Issues to do with importing modules meta Metavariables, insertion of implicit arguments, etc type: bug Issues and pull requests about actual bugs ux: warnings Issues relating to the reporting of warnings
#3393 opened Nov 14, 2018 by guillaumebrunerie icebox
@andreasabel
5
Preserve sharing in meta variable solutions by instantiating less aggressively meta Metavariables, insertion of implicit arguments, etc performance Slow type checking, interaction, compilation or execution of Agda programs sharing type: enhancement Issues and pull requests about possible improvements
#3094 opened May 28, 2018 by UlfNorell 2.7.0
@jul1u5
19
Overzealous pruning (reprise) eta η-expansion of metavariables and unification modulo η meta Metavariables, insertion of implicit arguments, etc pruning singleton-types Issues related to conversion modulo eta-equality for singleton types type: bug Issues and pull requests about actual bugs
#2876 opened Dec 19, 2017 by vlopezj later
6
Agda does not prune terms of singleton type constraints Constraints (postponed type checking problems, postponed unification problems, instance constraints) eta η-expansion of metavariables and unification modulo η meta Metavariables, insertion of implicit arguments, etc singleton-types Issues related to conversion modulo eta-equality for singleton types type: enhancement Issues and pull requests about possible improvements
#2625 opened Jul 3, 2017 by andreasabel icebox
In record declarations, meta variables are messed up meta Metavariables, insertion of implicit arguments, etc records Record declarations, literals, constructors and updates type: bug Issues and pull requests about actual bugs
#2561 opened May 1, 2017 by andreasabel icebox
2
Load does not turn placeholders into holes in emacs allow-unsolved-metas Issues relating to allow-unsolved-metas meta Metavariables, insertion of implicit arguments, etc type: bug Issues and pull requests about actual bugs ux: emacs Issues relating to the Emacs agda2-mode ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#2475 opened Feb 23, 2017 by andreasabel icebox
3
“Module cannot be imported since it has open interaction points” should always point to module import Issues to do with importing modules meta Metavariables, insertion of implicit arguments, etc modules Issues relating to the module system status: info-needed More information is needed from the bug reporter to confirm the issue. ux: error reporting Issues to do with how Agda reports errors
#2369 opened Dec 30, 2016 by mietek icebox
@andreasabel
13
The handling of implicit arguments should be improved give Problems with the "give" command hidden arguments Insertion of hidden arguments and implicit lambdas meta Metavariables, insertion of implicit arguments, etc type: bug Issues and pull requests about actual bugs type-checking ux: interaction Issues to do with interactive development (holes, case splitting, etc)
#2099 opened Jul 15, 2016 by mietek icebox
13
Better error messages when metavariable cannot be solved meta Metavariables, insertion of implicit arguments, etc pruning type: enhancement Issues and pull requests about possible improvements ux: error reporting Issues to do with how Agda reports errors
#2073 opened Jun 30, 2016 by jespercockx icebox
1
Agda allows "very dependent" types induction-induction Data declarations mutually recursive with data declarations insanely dependent types Declarations which appear in their own types (don't think about it too hard) meta Metavariables, insertion of implicit arguments, etc termination Issues relating to the termination checker type: bug Issues and pull requests about actual bugs
#1556 opened Aug 8, 2015 by GoogleCodeExporter icebox
20
Task: refactor metas in contextual type theory style. Proper sort metas. meta Metavariables, insertion of implicit arguments, etc sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy type: task Concerning the development of Agda (not in changelog)
#1432 opened Aug 8, 2015 by GoogleCodeExporter icebox
6
Pruning does not curry metas conversion Conversion checking for terms, types; Subtyping; Size solving eta η-expansion of metavariables and unification modulo η meta Metavariables, insertion of implicit arguments, etc pruning type: bug Issues and pull requests about actual bugs
#1330 opened Aug 8, 2015 by GoogleCodeExporter icebox
4
Termination checker run too late in mutual block meta Metavariables, insertion of implicit arguments, etc records Record declarations, literals, constructors and updates termination Issues relating to the termination checker type: bug Issues and pull requests about actual bugs
#1270 opened Aug 8, 2015 by GoogleCodeExporter icebox
6
Implicit-lambda insertion fails on reload hidden arguments Insertion of hidden arguments and implicit lambdas meta Metavariables, insertion of implicit arguments, etc type: bug Issues and pull requests about actual bugs
#1079 opened Aug 8, 2015 by GoogleCodeExporter later
8
Size constraint solver too eager in the presence of meta variables meta Metavariables, insertion of implicit arguments, etc sized types Sized types, termination checking with sized types, size inference type: bug Issues and pull requests about actual bugs
#992 opened Aug 8, 2015 by GoogleCodeExporter later
4
ProTip! Exclude everything labeled bug with -label:bug.