Release notes for Agda version 2.5.3

Installation and infrastructure

Added support for GHC 8.0.2 and 8.2.1.
Removed support for GHC 7.6.3.
Markdown support for literate Agda [PR #2357].

Files ending in .lagda.md will be parsed as literate Markdown files.

Code blocks start with ``` or ```agda in its own line, and end with ```, also in its own line.
Code blocks which should be type-checked by Agda but should not be visible when the Markdown is rendered may be enclosed in HTML comment delimiters ().
Code blocks which should be ignored by Agda, but rendered in the final document may be indented by four spaces.
Note that inline code fragments are not supported due to the difficulty of interpreting their indentation level with respect to the rest of the file.

Language

Pattern matching

Dot patterns.

The dot in front of an inaccessible pattern can now be skipped if the pattern consists entirely of constructors or literals. For example:

    open import Agda.Builtin.Bool

    data D : Bool → Set where
      c : D true

    f : (x : Bool) → D x → Bool
    f true c = true

Before this change, you had to write f .true c = true.

With-clause patterns can be replaced by _ [Issue #2363]. Example: agda test : Nat → Set test zero with zero test _ | _ = Nat test (suc x) with zero test _ | _ = Nat We do not have to spell out the pattern of the parent clause (zero / suc x) in the with-clause if we do not need the pattern variables. Note that x is not in scope in the with-clause!

A more elaborate example, which cannot be reduced to an ellipsis ...:

    record R : Set where
      coinductive -- disallow matching
      field f : Bool
            n : Nat

    data P (r : R) : Nat → Set where
      fTrue  : R.f r ≡ true → P r zero
      nSuc   : P r (suc (R.n r))

    data Q : (b : Bool) (n : Nat) →  Set where
      true! : Q true zero
      suc!  : ∀{b n} → Q b (suc n)

    test : (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
    test r nSuc       = suc!
    test r (fTrue p)  with R.f r
    test _ (fTrue ()) | false
    test _ _          | true = true!  -- underscore instead of (isTrue _)

Pattern matching lambdas (also known as extended lambdas) can now be nullary, mirroring the behaviour for ordinary function definitions. [Issue #2671]

This is useful for case splitting on the result inside an expression: given

  record _×_ (A B : Set) : Set where
    field
      π₁ : A
      π₂ : B
  open _×_

one may case split on the result (C-c C-c RET) in a hole

    λ { → {!!}}

of type A × B to produce

    λ { .π₁ → {!!} ; .π₂ → {!!}}

Records with a field of an empty type are now recognized as empty by Agda. In particular, they can be matched against with an absurd pattern (). For example:
```
data ⊥ : Set where

record Empty : Set where
  field absurdity : ⊥

magic : Empty → ⊥
magic ()
```
Injective pragmas.

Injective pragmas can be used to mark a definition as injective for the pattern matching unifier. This can be used as a version of --injective-type-constructors that only applies to specific datatypes. For example:

    open import Agda.Builtin.Equality
    data Fin : Nat → Set where
      zero : {n : Nat} → Fin (suc n)
      suc  : {n : Nat} → Fin n → Fin (suc n)

    {-# INJECTIVE Fin #-}

    Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
    Fin-injective refl = refl

Aside from datatypes, this pragma can also be used to mark other definitions as being injective (for example postulates).

Metavariables can no longer be instantiated during case splitting. This means Agda will refuse to split instead of taking the first constructor it finds. For example:
```
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  nil : Vec A 0
  cons : {n : Nat} → A → Vec A n → Vec A (suc n)

foo : Vec Nat _ → Nat
foo x = {!x!}
```
In Agda 2.5.2, case splitting on x produced the single clause foo nil = {!!}, but now Agda refuses to split.

Reflection

New TC primitive: debugPrint.

    debugPrint : String → Nat → List ErrorPart → TC ⊤

This maps to the internal function reportSDoc. Debug output is enabled with the -v flag at the command line, or in an OPTIONS pragma. For instance, giving -v a.b.c:10 enables printing from debugPrint "a.b.c.d" 10 msg. In the Emacs mode, debug output ends up in the *Agda debug* buffer.

Built-ins

BUILTIN REFL is now superfluous, subsumed by BUILTIN EQUALITY [Issue #2389].
BUILTIN EQUALITY is now more liberal [Issue #2386]. It accepts, among others, the following new definitions of equality: ```agda -- Non-universe polymorphic: data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

-- ... with explicit argument to refl; data ≡ {A : Set} : (x y : A) → Set where refl : {x : A} → x ≡ x

-- ... even visible data ≡ {A : Set} : (x y : A) → Set where refl : (x : A) → x ≡ x

-- Equality in a different universe than domain: -- (also with explicit argument to refl) data ≡ {a} {A : Set a} (x : A) : A → Set where refl : x ≡ x

  The standard definition is still:
  ```agda
    -- Equality in same universe as domain:
    data _≡_ {a} {A : Set a} (x : A) : A → Set a where
      refl : x ≡ x

Miscellaneous

Rule change for omitted top-level module headers. [Issue #1077]

If your file is named Bla.agda, then the following content is rejected.

    foo = Set
    module Bla where
      bar = Set

Before the fix of this issue, Agda would add the missing module header module Bla where at the top of the file. However, in this particular case it is more likely the user put the declaration foo = Set before the module start in error. Now you get the error

    Illegal declaration(s) before top-level module

if the following conditions are met:

1. There is at least one non-import declaration or non-toplevel pragma
   before the start of the first module.

2. The module has the same name as the file.

3. The module is the only module at this level
   (may have submodules, of course).

If you should see this error, insert a top-level module before the illegal declarations, or move them inside the existing module.

Emacs mode

New warnings:
- Unreachable clauses give rise to a simple warning. They are highlighted in gray.
- Incomplete patterns are non-fatal warnings: it is possible to keep interacting with the file (the reduction will simply be stuck on arguments not matching any pattern). The definition with incomplete patterns are highlighted in wheat.
Clauses which do not hold definitionally are now highlighted in white smoke.
Fewer commands have the side effect that the buffer is saved.
Aborting commands.

Now one can (try to) abort an Agda command by using C-c C-x C-a or a menu entry. The effect is similar to that of restarting Agda (C-c C-x C-r), but some state is preserved, which could mean that it takes less time to reload the module.

Warning: If a command is aborted while it is writing data to disk (for instance .agdai files or Haskell files generated by the GHC backend), then the resulting files may be corrupted. Note also that external commands (like GHC) are not aborted, and their output may continue to be sent to the Emacs mode.

New bindings for the Agda input method:
- All the bold digits are now available. The naming scheme is \Bx for digit x.
- Typing \: you can now get a whole slew of colons.
(The Agda input method originally only bound the standard unicode colon, which looks deceptively like the normal colon.)

Case splitting now preserves underscores. [Issue #819]

data ⊥ : Set where

test : {A B : Set} → A → ⊥ → B
test _ x = {! x !}

Splitting on x yields

test _ ()

Interactively expanding ellipsis. [Issue #2589] An ellipsis in a with-clause can be expanded by splitting on "variable" "." (dot).
```
test0 : Nat → Nat
test0 x with zero
... | q = {! . !}  -- C-c C-c
```
Splitting on dot here yields:
```
test0 x | q = ?
```
New command to check an expression against the type of the hole it is in and see what it elaborates to. [Issue #2700] This is useful to determine e.g. what solution typeclass resolution yields. The command is bound to C-c C-; and respects the C-u modifier.

    record Pointed (A : Set) : Set where
      field point : A

    it : ∀ {A : Set} {{x : A}} → A
    it {{x}} = x

    instance _ = record { point = 3 - 4 }

    _ : Pointed Nat
    _ = {! it !} -- C-u C-u C-c C-;

yields

    Goal: Pointed Nat
    Elaborates to: record { point = 0 }

If agda2-give is called with a prefix, then giving is forced, i.e., the safety checks are skipped, including positivity, termination, and double type-checking. [Issue #2730]

Invoke forced giving with key sequence C-u C-c C-SPC.

Library management

The name field in an .agda-lib file is now optional. [Issue #2708]

This feature is convenient if you just want to specify the dependencies and include pathes for your local project in an .agda-lib file.

Naturally, libraries without names cannot be depended on.

Compiler backends

Unified compiler pragmas

The compiler pragmas (COMPILED, COMPILED_DATA, etc.) have been unified across backends into two new pragmas:

    {-# COMPILE <Backend> <Name> <Text> #-}
    {-# FOREIGN <Backend> <Text> #-}

The old pragmas still work, but will emit a warning if used. They will be removed completely in Agda 2.6.

The translation of old pragmas into new ones is as follows:

Old	New
`{-# COMPILED f e #-}`	`{-# COMPILE GHC f = e #-}`
`{-# COMPILED_TYPE A T #-}`	`{-# COMPILE GHC A = type T #-}`
`{-# COMPILED_DATA A D C1 .. CN #-}`	`{-# COMPILE GHC A = data D (C1 \\| .. \\| CN) #-}`
`{-# COMPILED_DECLARE_DATA #-}`	obsolete, removed
`{-# COMPILED_EXPORT f g #-}`	`{-# COMPILE GHC f as g #-}`
`{-# IMPORT M #-}`	`{-# FOREIGN GHC import qualified M #-}`
`{-# HASKELL code #-}`	`{-# FOREIGN GHC code #-}`
`{-# COMPILED_UHC f e #-}`	`{-# COMPILE UHC f = e #-}`
`{-# COMPILED_DATA_UHC A D C1 .. CN #-}`	`{-# COMPILE UHC A = data D (C1 \\| .. \\| CN) #-}`
`{-# IMPORT_UHC M #-}`	`{-# FOREIGN UHC __IMPORT__ M #-}`
`{-# COMPILED_JS f e #-}`	`{-# COMPILE JS f = e #-}`

GHC Haskell backend

The COMPILED pragma (and the corresponding COMPILE GHC pragma) is now also allowed for functions. This makes it possible to have both an Agda implementation and a native Haskell runtime implementation.

The GHC file header pragmas LANGUAGE, OPTIONS_GHC, and INCLUDE inside a FOREIGN GHC pragma are recognized and printed correctly at the top of the generated Haskell file. [Issue #2712]

UHC compiler backend

The UHC backend has been moved to its own repository [https://github.com/agda/agda-uhc] and is no longer part of the Agda distribution.

Haskell imports are no longer transitively inherited from imported modules.

The (now deprecated) IMPORT and IMPORT_UHC pragmas no longer cause import statements in modules importing the module containing the pragma.

The same is true for the corresponding FOREIGN pragmas.

Support for stand-alone backends.

There is a new API in Agda.Compiler.Backend for creating stand-alone backends using Agda as a library. This allows prospective backend writers to experiment with new backends without having to change the Agda code base.

HTML backend

Anchors for identifiers (excluding bound variables) are now the identifiers themselves rather than just the file position [Issue #2604].

Symbolic anchors look like

  <a id="test1">
  <a id="M.bla">

while other anchors just give the character position in the file:

  <a id="42">

Top-level module names do not get a symbolic anchor, since the position of a top-level module is defined to be the beginning of the file.

Example:

  module Issue2604 where   -- Character position anchor

  test1 : Set₁             -- Issue2604.html#test1
  test1 = bla
    where
    bla = Set              -- Character position anchor

  test2 : Set₁             -- Issue2604.html#test2
  test2 = bla
    where
    bla = Set              -- Character position anchor

  test3 : Set₁             -- Issue2604.html#test3
  test3 = bla
    module M where         -- Issue2604.html#M
    bla = Set              -- Issue2604.html#M.bla

  module NamedModule where -- Issue2604.html#NamedModule
    test4 : Set₁           -- Issue2604.html#NamedModule.test4
    test4 = M.bla

  module _ where           -- Character position anchor
    test5 : Set₁           -- Character position anchor
    test5 = M.bla

Some generated HTML files now have different file names [Issue #2725].

Agda now uses an encoding that amounts to first converting the module names to UTF-8, and then percent-encoding the resulting bytes. For instance, HTML for the module Σ is placed in %CE%A3.html.

LaTeX backend

The LaTeX backend now handles indentation in a different way [Issue #1832].

A constraint on the indentation of the first token t on a line is determined as follows:

Let T be the set containing every previous token (in any code block) that is either the initial token on its line or preceded by at least one whitespace character.
Let S be the set containing all tokens in T that are not shadowed by other tokens in T. A token t₁ is shadowed by t₂ if t₂ is further down than t₁ and does not start to the right of t₁.
Let L be the set containing all tokens in S that start to the left of t, and E be the set containing all tokens in S that start in the same column as t.
The constraint is that t must be indented further than every token in L, and aligned with every token in E.

Note that if any token in L or E belongs to a previous code block, then the constraint may not be satisfied unless (say) the AgdaAlign environment is used in an appropriate way.

If custom settings are used, for instance if \AgdaIndent is redefined, then the constraint discussed above may not be satisfied. (Note that the meaning of the \AgdaIndent command's argument has changed, and that the command is now used in a different way in the generated LaTeX files.)

Examples:

Here C is indented further than B:
```
postulate
  A  B
      C : Set
```
Here C is not (necessarily) indented further than B, because X shadows B:
```
postulate
  A  B  : Set
  X
      C : Set
```

The new rule is inspired by, but not identical to, the one used by lhs2TeX's poly mode (see Section 8.4 of the manual for lhs2TeX version 1.17).

Some spacing issues [#2353, #2441, #2733, #2740] have been fixed.
The user can now control the typesetting of (certain) individual tokens by redefining the \AgdaFormat command. Example: ```latex \usepackage{ifthen}

% Insert extra space before some tokens. \DeclareRobustCommand{\AgdaFormat}[2]{%

\ifthenelse{
  \equal{#1}{≡⟨} \OR
  \equal{#1}{≡⟨⟩} \OR
  \equal{#1}{∎}
}{\ }{}#2}

  Note the use of `\DeclareRobustCommand`. The first argument to
  `\AgdaFormat` is the token, and the second argument the thing to
  be typeset.

* One can now instruct the agda package not to select any fonts.

  If the `nofontsetup` option is used, then some font packages are
  loaded, but specific fonts are not selected:
  ```latex
  \usepackage[nofontsetup]{agda}

The height of empty lines is now configurable [#2734].

The height is controlled by the length \AgdaEmptySkip, which by default is \baselineskip.

The alignment feature regards the string +̲, containing + and a combining character, as having length two. However, it seems more reasonable to treat it as having length one, as it occupies a single column, if displayed "properly" using a monospace font. The new flag --count-clusters is an attempt at fixing this. When this flag is enabled the backend counts "extended grapheme clusters" rather than code points.

Note that this fix is not perfect: a single extended grapheme cluster might be displayed in different ways by different programs, and might, in some cases, occupy more than one column. Here are some examples of extended grapheme clusters, all of which are treated as a single character by the alignment algorithm:

  │ │
  │+̲│
  │Ö̂│
  │நி│
  │ᄀힰᇹ│
  │ᄀᄀᄀᄀᄀᄀힰᇹᇹᇹᇹᇹᇹ│
  │ │

Note also that the layout machinery does not count extended grapheme clusters, but code points. The following code is syntactically correct, but if --count-clusters is used, then the LaTeX backend does not align the two field keywords:

    record +̲ : Set₁ where  field A : Set
                            field B : Set

The --count-clusters flag is not enabled in all builds of Agda, because the implementation depends on the ICU library, the installation of which could cause extra trouble for some users. The presence of this flag is controlled by the Cabal flag enable-cluster-counting.

A faster variant of the LaTeX backend: QuickLaTeX.

When this variant of the backend is used the top-level module is not type-checked, only scope-checked. This implies that some highlighting information is not available. For instance, overloaded constructors are not resolved.

QuickLaTeX can be invoked from the Emacs mode, or using agda --latex --only-scope-checking. If the module has already been type-checked successfully, then this information is reused; in this case QuickLaTeX behaves like the regular LaTeX backend.

The --only-scope-checking flag can also be used independently, but it is perhaps unclear what purpose that would serve. (The flag can currently not be combined with --html, --dependency-graph or --vim.) The flag is not allowed in safe mode.

Pragmas and options

The --safe option is now a valid pragma.

This makes it possible to declare a module as being part of the safe subset of the language by stating {-# OPTIONS --safe #-} at the top of the corresponding file. Incompatibilities between the --safe option and other options or language constructs are non-fatal errors.

The --no-main option is now a valid pragma.

One can now suppress the compiler warning about a missing main function by putting

    {-# OPTIONS --no-main #-}

on top of the file.

New command-line option and pragma --warning=MODE (or -W MODE) for setting the warning mode. Current options are
- warn for displaying warnings (default)
- error for turning warnings into errors
- ignore for not displaying warnings

List of fixed issues

For 2.5.3, the following issues have been fixed (see bug tracker):

#142: Inherited dot patterns in with functions are not checked
#623: Error message points to importing module rather than imported module
#657: Yet another display form problem
#668: Ability to stop, or restart, typechecking somehow
#705: confusing error message for ambiguous datatype module name
#719: Error message for duplicate module definition points to external module instead of internal module
#776: Unsolvable constraints should give error
#819: Case-splitting doesn't preserve underscores
#883: Rewrite loses type information
#899: Instance search fails if there are several definitionally equal values in scope
#1077: problem with module syntax, with parametric module import
#1126: Port optimizations from the Epic backend
#1175: Internal Error in Auto
#1544: Positivity polymorphism needed for compositional positivity analysis
#1611: Interactive splitting instantiates meta
#1664: Add Reflection primitives to expose precedence and fixity
#1817: Solvable size constraints reported as unsolvable
#1832: Insufficient indentation in LaTeX-rendered Agda code
#1834: Copattern matching: order of clauses should not matter here
#1886: Second copies of telescopes not checked?
#1899: Positivity checker does not treat datatypes and record types in the same way
#1975: Type-incorrect instantiated overloaded constructor accepted in pattern
#1976: Type-incorrect instantiated projection accepted in pattern
#2035: Matching on string causes solver to fail with internal error
#2146: Unicode syntax for instance arguments
#2217: Abort Agda without losing state
#2229: Absence or presence of top-level module header affects scope
#2253: Wrong scope error for abstract constructors
#2261: Internal error in Auto/CaseSplit.hs:284
#2270: Printer does not use sections.
#2329: Size solver does not use type Size< i to gain the necessary information
#2354: Interaction between instance search, size solver, and ordinary constraint solver.
#2355: Literate Agda parser does not recognize TeX comments
#2360: With clause stripping chokes on ambiguous projection
#2362: Printing of parent patterns when with-clause does not match
#2363: Allow underscore in with-clause patterns
#2366: With-clause patterns renamed in error message
#2368: Internal error after refining a tactic @ MetaVars.hs:267
#2371: Shadowed module parameter crashes interaction
#2372: problems when instances are declared with inferred types
#2374: Ambiguous projection pattern could be disambiguated by visibility
#2376: Termination checking interacts badly with eta-contraction
#2377: open public is useless before module header
#2381: Search (C-c C-z) panics on pattern synonyms
#2386: Relax requirements of BUILTIN EQUALITY
#2389: BUILTIN REFL not needed
#2400: LaTeX backend error on LaTeX comments
#2402: Parameters not dropped when reporting incomplete patterns
#2403: Termination checker should reduce arguments in structural order check
#2405: instance search failing in parameterized module
#2408: DLub sorts are not serialized
#2412: Problem with checking with sized types
#2413: Agda crashes on x@y pattern
#2415: Size solver reports "inconsistent upper bound" even though there is a solution
#2416: Cannot give size as computed by solver
#2422: Overloaded inherited projections don't resolve
#2423: Inherited projection on lhs
#2426: On just warning about missing cases
#2429: Irrelevant lambda should be accepted when relevant lambda is expected
#2430: Another regression related to parameter refinement?
#2433: rebindLocalRewriteRules re-adds global rewrite rules
#2434: Exact split analysis is too strict when matching on eta record constructor
#2441: Incorrect alignement in latex using the new ACM format
#2444: Generalising compiler pragmas
#2445: The LaTeX backend is slow
#2447: Cache loaded interfaces even if a type error is encountered
#2449: Agda depends on additional C library icu
#2451: Agda panics when attempting to rewrite a typeclass Eq
#2456: Internal error when postulating instance
#2458: Regression: Agda-2.5.3 loops where Agda-2.5.2 passes
#2462: Overloaded postfix projection does not resolve
#2464: Eta contraction for irrelevant functions breaks subject reduction
#2466: Case split to make hidden variable visible does not work
#2467: REWRITE without BUILTIN REWRITE crashes
#2469: "Partial" pattern match causes segfault at runtime
#2472: Regression related to the auto command
#2477: Sized data type analysis brittle, does not reduce size
#2478: Multiply defined labels on the user manual (pdf)
#2479: "Occurs check" error in generated Haskell code
#2480: Agda accepts incorrect (?) code, subject reduction broken
#2482: Wrong counting of data parameters with new-style mutual blocks
#2483: Files are sometimes truncated to a size of 201 bytes
#2486: Imports via FOREIGN are not transitively inherited anymore
#2488: Instance search inhibits holes for instance fields
#2493: Regression: Agda seems to loop when expression is given
#2494: Instance fields sometimes have incorrect goal types
#2495: Regression: termination checker of Agda-2.5.3 seemingly loops where Agda-2.5.2 passes
#2500: Adding fields to a record can cause Agda to reject previous definitions
#2510: Wrong error with --no-pattern-matching
#2517: "Not a variable error"
#2518: CopatternReductions in TreeLess
#2523: The documentation of --without-K is outdated
#2529: Unable to install Agda on Windows.
#2537: case splitting with 'with' creates {_} instead of replicating the arguments it found.
#2538: Internal error when parsing as-pattern
#2543: Case splitting with ellipsis produces spurious parentheses
#2545: Race condition in api tests
#2549: Rewrite rule for higher path constructor does not fire
#2550: Internal error in Agda.TypeChecking.Substitute
#2552: Let bindings in module telescopes crash Agda.Interaction.BasicOps
#2553: Internal error in Agda.TypeChecking.CheckInternal
#2554: More flexible size-assignment in successor style
#2555: Why does the positivity checker care about non-recursive occurrences?
#2558: Internal error in Warshall Solver
#2560: Internal Error in Reduce.Fast
#2564: Non-exact-split highlighting makes other highlighting disappear
#2568: agda2-infer-type-maybe-toplevel (in hole) does not respect "single-solution" requirement of instance resolution
#2571: Record pattern translation does not eta contract
#2573: Rewrite rules fail depending on unrelated changes
#2574: No link attached to module without toplevel name
#2575: Internal error, related to caching
#2577: deBruijn fail for higher order instance problem
#2578: Catch-all clause face used incorrectly for parent with pattern
#2579: Import statements with module instantiation should not trigger an error message
#2580: Implicit absurd match is NonVariant, explicit not
#2583: Wrong de Bruijn index introduced by absurd pattern
#2584: Duplicate warning printing
#2585: Definition by copatterns not modulo eta
#2586: "λ where" with single absurd clause not parsed
#2588: agda --latex produces invalid LaTeX when there are block comments
#2592: Internal Error in Agda/TypeChecking/Serialise/Instances/Common.hs
#2597: Inline record definitions confuse the reflection API
#2602: Debug output messes up AgdaInfo buffer
#2603: Internal error in MetaVars.hs
#2604: Use QNames as anchors in generated HTML
#2605: HTML backend generates anchors for whitespace
#2606: Check that LHS of a rewrite rule doesn't reduce is too strict
#2612: exact-split documentation is outdated and incomplete
#2613: Parametrised modules, with-abstraction and termination
#2620: Internal error in auto.
#2621: Case splitting instantiates meta
#2626: triggered internal error with sized types in MetaVars module
#2629: Exact splitting should not complain about absurd clauses
#2631: docs for auto aren't clear on how to use flags/options
#2632: some flags to auto dont seem to work in current agda 2.5.2
#2637: Internal error in Agda.TypeChecking.Pretty, possibly related to sized types
#2639: Performance regression, possibly related to the size solver
#2641: Required instance of FromNat when compiling imported files
#2642: Records with duplicate fields
#2644: Wrong substitution in expandRecordVar
#2645: Agda accepts postulated fields in a record
#2646: Only warn if fixities for undefined symbols are given
#2649: Empty list of "previous definition" in duplicate definition error
#2652: Added a new variant of the colon to the Agda input method
#2653: agda-mode: "cannot refine" inside instance argument even though term to be refined typechecks there
#2654: Internal error on result splitting without --postfix-projections
#2664: Segmentation fault with compiled programs using mutual record
#2665: Documentation: Record update syntax in wrong location
#2666: Internal error at Agda/Syntax/Abstract/Name.hs:113
#2667: Panic error on unbound variable.
#2669: Interaction: incorrect field variable name generation
#2671: Feature request: nullary pattern matching lambdas
#2679: Internal error at "Typechecking/Abstract.hs:133" and "TypeChecking/Telescope.hs:68"
#2682: What are the rules for projections of abstract records?
#2684: Bad error message for abstract constructor
#2686: Abstract constructors should be ignored when resolving overloading
#2690: [regression?] Agda engages in deep search instead of immediately failing
#2700: Add a command to check against goal type (and normalise)
#2703: Regression: Internal error for underapplied indexed constructor
#2705: The GHC backend might diverge in infinite file creation
#2708: Why is the name field in .agda-lib files mandatory?
#2710: Type checker hangs
#2712: Compiler Pragma for headers
#2714: Option --no-main should be allowed as file-local option
#2717: internal error at DisplayForm.hs:197
#2718: Interactive 'give' doesn't insert enough parenthesis
#2721: Without-K doesn't prevent heterogeneous conflict between literals
#2723: Unreachable clauses in definition by copattern matching trip clause compiler
#2725: File names for generated HTML files
#2726: Old regression related to with
#2727: Internal errors related to rewrite
#2729: Regression: case splitting uses variable name variants instead of the unused original names
#2730: Command to give in spite of termination errors
#2731: Agda fails to build with happy 1.19.6
#2733: Avoid some uses of \AgdaIndent?
#2734: Make height of empty lines configurable
#2736: Segfault using Alex 3.2.2 and cpphs
#2740: Indenting every line of code should be a no-op

2.5.3.md 39 KB 永久連結 文件歷史 原始文件