Release notes for Agda version 2.6.0

Highlights

Added support for Cubical Agda which adds new features such as univalence and higher inductive types to Agda.
Added support for ML-style automatic generalization of variables.
Added a new sort Prop of definitionally proof-irrelevant propositions.
The implementation of instance search got a major overhaul and no longer supports overlapping instances (unless enabled by a flag).

Installation and infrastructure

Added support for GHC 8.6.4.
Interface files for all builtin and primitive files are now re-generated each time Agda is installed.

Syntax

Agda now supports implicit generalization of declared variables. Variables to be generalized can declared with the new keyword variable. For example:

    postulate
      Con : Set

    variable
      Γ Δ θ : Con

Declared variables are automatically generalized in type signatures, module telescopes and data type and record parameters and indices:

    postulate
      Sub : Con → Con → Set

      id  : Sub Γ Γ
   -- -- equivalent to
   -- id  : {Γ : Con} → Sub Γ Γ

      _∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
   -- -- equivalent to
   -- _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ

See the user manual for more details.

Data type and record definitions separated from their type signatures can no longer repeat the types of the parameters, but can bind implicit parameters by name [Issue #1886].

This is now allowed

    data D {a b} (A : Set a) (B : Set b) : Set (a ⊔ lsuc b)
    data D {b = b} A B where
      mkD : (A → Set b) → D A B

but this is not

    data I (A : Set) : Set
    data I (A : Set) where

The label used for named implicit arguments can now be different from the name of the bound variable [Issue #952].

Example,

    id₁ : {A = X : Set} → X → X
    id₁ x = x

    id₂ : ∀ {B = X} → X → X
    id₂ {B = X} x = id₁ {A = X} x

    test : Nat
    test = id₁ {A = Nat} 5 + id₂ {B = Nat} 6

Only implicit and instance arguments can have a label and either or both of the label and bound variable can be _. Labeled bindings with a type signature can only bind a single variable. For instance, the type Set has to be repeated here:

    const : {A = X : Set} {B = Y : Set} → X → Y → X
    const x _ = x

The rules for parsing of patterns have changed slightly [Issue #3400].

Now projections are treated similarly to constructors: In a pattern name parts coming from projections can only be used as part of projections, constructors or pattern synonyms. They cannot be used as variables, or as part of the name of the defined value.

Examples:

The following code used to be syntactically ambiguous, but is now parsed, because A can no longer be used as a variable:
```
record R : Set₂ where
  field
    _A : Set₁

open R

r : R
r A = Set
```
On the other hand the following code is no longer parsed: ```agda record R : Set₁ where field
```
⟨_+_⟩ : Set
```
open R
- : Set → Set
- A = A ```

Type checking

Agda now supports a cubical mode which adds new features from Cubical Type Theory, including univalence and higher inductive types. Option --cubical enables the cubical mode, and cubical primitives are defined in the module Agda.Primitive.Cubical. See the user manual for more info.
Agda now supports the new sort Prop of definitionally proof-irrelevant propositions. Option --prop enables the Prop universe but is off by default. Option --no-prop disables the Prop universe. See the user manual for more details.

In the absense of Prop, the sort Set is the lowest sort, thus, the sort annotation : Set can be ommitted if the sort is constrained to be weakly below Set. For instance:

  {-# OPTIONS --no-prop #-}

  data Wrap A : Set where
    wrap : A → Wrap A

In contrast, when --prop is enabled the sort of A could be either Set or Prop so this code no longer typechecks.

Agda now allows omitting absurd clauses in case one of the pattern variable inhabits an obviously empty type [Issue #1086]. For example: agda f : Fin 1 → Nat f zero = 0 -- f (suc ()) -- this clause is no longer required Absurd clauses are still required in case deep pattern matching is needed to expose the absurd variable, or if there are no non-absurd clauses.

Due to the changes to the coverage checker required for this new feature, Agda will now sometimes construct a different case tree when there are multiple valid splitting orders. In some cases this may impact the constraints that Agda is able to solve (for example, see #673 on the standard library).

Since Agda 2.5.3, the hiding is considered part of the name in the insertion of implicit arguments. Until Agda 2.5.2, the following code was rejected:
```
test : {{X : Set}} {X : Set} → Set
test {X = X} = X
```
The rationale was that named argument X is given with the wrong hiding. The new rationale is that the hiding is considered part of the name, distinguishing {{X}} from {X}. This language change was accidential and has not been documented in the 2.5.3 release notes.
Agda no longer allows case splitting on irrelevant arguments of record types (see Issue #3056).
Metavariables in module telescopes are now sometimes frozen later [Issue #1063].

Metavariables created in the types of module parameters used to be frozen right after the module's first mutual block had been type-checked (unless, perhaps, if the module itself was contained in a mutual block). Now they are instead frozen at the end of the module (with a similar caveat regarding an outer mutual block).

When --without-K is enabled, Agda no longer allows datatypes with large indices. For example, the following definition of equality is now forbidden when --without-K is enabled:
```
data _≡₀_ {ℓ} {A : Set ℓ} (x : A) : A → Set where
  refl : x ≡₀ x
```
The termination checker now also looks for recursive calls in the type of definitions. This fixes an issue where Agda allowed very dependent types [Issue #1556].

This change affects induction-induction, e.g.

    mutual
      data Cxt : Set where
        ε    :  Cxt
        _,_  :  (Γ : Cxt) (A : Ty Γ) → Cxt

      data Ty : (Γ : Cxt) → Set where
        u  :  ∀ Γ → Ty Γ
        Π  :  ∀ Γ (A : Ty Γ) (B : Ty (Γ , A)) → Ty Γ

    mutual
      f : Cxt → Cxt
      f ε        =  ε
      f (Γ , T)  =  (f Γ , g Γ T)

      g : ∀ Γ → Ty Γ → Ty (f Γ)
      g Γ (u .Γ)      =  u (f Γ)
      g Γ (Π .Γ A B)  =  Π (f Γ) (g Γ A) (g (Γ , A) B)

The type of g contains a call g Γ _ --> f Γ which is now taken into account during termination checking.

Instance search

Instance argument resolution now also applies when there are unconstrained metavariables in the type of the argument. For example, if there is a single instance eqBool : Eq Bool in scope, then an instance argument {{eq : Eq _}} will be solved to eqBool, setting the value of the metavariable _ to Bool in the process.
By default, Agda no longer allows overlapping instances. Two instances are defined to overlap if they could both solve the instance goal when given appropriate solutions for their recursive (instance) arguments. Agda used to choose between undecidable instances based on the result of recursive instance search, but this lead to an exponential slowdown in instance resolution. Overlapping instances can be enabled with the flag --overlapping-instances.
Explicit arguments are no longer automatically turned into instance arguments for the purpose of recursive instance search. Instead, explicit arguments are left unresolved and will thus never be used for instance search.

If an instance is declared which has explicit arguments, Agda will raise a warning that this instance will never be considered by instance search.

Instance arguments that are already solved by conversion checking are no longer ignored by instance search. Thus the constructor of the unit type must now be explicitly be declared as an instance in order to be considered by instance search:
```
record ⊤ : Set where
  instance constructor tt
```
Instances are now (correctly) required to be in scope to be eligible (see Issue #1913 and Issue #2489 ). This means that you can no longer import instances from parameterised modules by
```
import Some.Module Arg₁ Arg2
```
without opening or naming the module.

Reflection

New TC primitive noConstraints [Issue #2351]:

    noConstraints : ∀ {a} {A : Set a} → TC A → TC A

The computation noConstraints m fails if m gives rise to new, unsolved "blocking" constraints.

New TC primitive runSpeculative [Issue #3346]:

    runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A

The computation runSpeculative m runs m and either keeps the new TC state (if the second component is true) or resets to the old TC state (if it is false).

Interaction and error reporting

A new command agda2-elaborate-give (C-c C-m) normalizes a goal input (it respects the C-u prefixes), type checks, and inserts the normalized term into the goal.
'Solve constraints' (C-c C-s) now turns unsolved metavariables into new interaction holes (see Issue #2273).
Out-of-scope identifiers are no longer prefixed by a '.' dot [Issue #3127]. This notation could be confused with dot patterns, postfix projections, and irrelevance. Now Agda will do its best to make up fresh names for out-of-scope identifiers that do not conflict with any existing names. In addition, these names are marked as "(out of scope)" when printing the context.

The change affects the printing of terms, e.g. in error messages and interaction, and the parsing of out-of-scope variables for case splitting (C-c C-c in emacs).

Shadowed local variables are now assigned fresh names in error messages and interactive goals [Issue #572]. For example, consider the following piece of code:

postulate P : Set -> Set

test : (B : Set) -> P B -> P B
test = λ p p -> {!!}

When asking for the goal type, Agda will now print the following:

Goal: P p₁
————————————————————————————————————————————————————————————
p      : P p₁
p = p₁ : Set  (not in scope)

Shadowed top-level identifiers are printed using the qualified name, for example in

module M where

  postulate A : Set

  test : Set → A
  test A = {!!}

Agda will now show the goal type as

Goal: M.A
————————————————————————————————————————————————————————————
A : Set

When case splitting (C-c C-c in emacs), Agda will now filter out impossible cases (i.e. ones where at least one of the variables could be replaced by an absurd pattern ()). If all the clauses produced by a case split are impossible, Agda will not filter out any of them.

Pragmas and options

Consistency checking of options used.

Agda now checks that options used in imported modules are consistent with each other, e.g. a module using --safe, --without-K, --no-universe-polymorphism or --no-sized-types may only import modules with the same option, and modules using --cubical or --prop must in turn use the same option. If an interface file has been generated using different options compared to the current ones, Agda will now re-typecheck the file. [Issue #2487].

New option --cubical to enable Cubical Agda.
New option --prop to enable the Prop sort, and --no-prop to disable it (default).
New options --guardedness and --no-guardedness [Issue #1209].

Constructor-based guarded corecursion is now only (meant to be) allowed if the --guardedness option is active. This option is active by default. The combination of constructor-based guarded corecursion and sized types is not allowed if --safe is used, and activating --safe turns off both --guardedness and --sized-types (because this combination is known to be inconsistent in the current implementation). If you want to use either constructor-based guarded corecursion or sized types in safe mode, then you can use --safe --guardedness or --safe --sized-types respectively (in this order).

The option --no-guardedness turns off constructor-based guarded corecursion.

Option --irrelevant-projections is now off by default and not considered --safe any longer. Reason: There are consistency issues that may be systemic [Issue #2170].
New option --no-syntactic-equality disables the syntactic equality shortcut used by the conversion checker. This will slow down typechecking in most cases, but makes the performance more predictable and stable under minor changes.
New option --overlapping-instances enables overlapping instances by performing recursive instance search during pruning of instance candidates (this used to be the default behaviour). Overlapping instances can be disabled with --no-overlapping-instances (default).
Option (and experimental feature) --guardedness-preserving-type-constructors has been removed. [Issue #3180].
Deprecated options --sharing and --no-sharing now raise an error.
New primitive primErase. It takes a proof of equality and returns a proof of the same equality. primErase eq reduces to refl on the diagonal. trustMe is not a primitive anymore, it is implemented using primErase.

The primitive is declared in Agda.Builtin.Equality.Erase.

The REWRITE builtin is now bound to the builtin equality type from Agda.Builtin.Equality in Agda.Builtin.Equality.Rewrite [Issue #3318].
New primitives primCharToNatInjective and primStringToListInjective internalising the fact that primCharToNat and primStringtoList are injective functions. They are respectively bound in Agda.Builtin.Char.Properties and Agda.Builtin.String.Properties.
The option --only-scope-checking is now allowed together with --safe.
The option --ignore-interfaces no longer ignores the interfaces of builtin and primitive modules. For experts, there is the option --ignore-all-interfaces which also rechecks builtin and primitive files.
The following deprecated compiler pragmas have been removed:

    {-# COMPILED f e #-}
    {-# COMPILED_TYPE A T #-}
    {-# COMPILED_DATA A D C1 .. CN #-}
    {-# COMPILED_DECLARE_DATA #-}
    {-# COMPILED_EXPORT f g #-}
    {-# IMPORT M #-}
    {-# HASKELL code #-}
    {-# COMPILED_UHC f e #-}
    {-# COMPILED_DATA_UHC A D C1 .. CN #-}
    {-# IMPORT_UHC M #-}
    {-# COMPILED_JS f e #-}

See the user manual for how to use the COMPILE and FOREIGN pragmas that replaced these in Agda 2.5.

New warnings

A declaration of the form f : A without an accompanying definition is no longer an error, but instead raises a warning.
A clause that has both an absurd pattern and a right-hand side is no longer an error, but instead raises a warning.
An import statement for M that mentions names not exported by M (in either using, hiding, or renaming) is no longer an error. Instead, Agda will raise a warning and ignore the names.
Pragma, primitive, module or import statements in a mutual block are no longer errors. Instead, Agda will raise a warning and ignore these statements.

Pragmas and options concerning universes

New pragma {-# NO_UNIVERSE_CHECK #-}.

The pragma {-# NO_UNIVERSE_CHECK #-} can be put in front of a data or record type to disable universe consistency checking locally. Example:

    {-# NO_UNIVERSE_CHECK #-}
    data U : Set where
      el : Set → U

Like the similar pragmas for disabling termination and positivity checking, {-# NO_UNIVERSE_CHECK #-} cannot be used with --safe.

New builtin SETOMEGA.

Agda's top sort Setω is now defined as a builtin in Agda.Primitive and can be renamed when importing that module.

New option --omega-in-omega.

The option --omega-in-omega enables the typing rule Setω : Setω. Example:

  {-# OPTIONS --omega-in-omega #-}
  open import Agda.Primitive

  data Type : Setω where
    el : ∀ {ℓ} → Set ℓ → Type

Like --type-in-type, this makes Agda inconsistent. However, code written using --omega-in-omega is still compatible with normal universe-polymorphic code and can be used in such files.

Emacs mode

Jump-to-definition now works for record field names in record expressions and patterns. [Issue #3120]
```
record R : Set₂ where
  field f : Set₁

exp : R
exp = record { f = Set }

pat : R → R
pat r@record { f = X } = record r { f = X }
```
Jump-to-definition (M-. or middle-click) on any of these fs now jumps to the field declaration.
Commas "ʻ،⸲⸴⹁⹉、︐︑﹐﹑，､" and semi-colons "؛⁏፤꛶；︔﹔⍮⸵;" added to the input mode.
It is now possible to customise the highlighting of more text in pragmas [Issue #2452].

Some text was already highlighted. Now there is a specific face for the remaining text (agda2-highlight-pragma-face).

LaTeX backend

The code environment has two new options, inline and inline*.

These options are for typesetting inline code. The implementation of these options is a bit of a hack. Only use these options for typesetting a single line of code without multiple consecutive whitespace characters (except at the beginning of the line).

When the option inline* is used space (\AgdaSpace{}) is added at the end of the code, and when inline is used space is not added.

Now highlighting commands for things like "this is an unsolved meta-variable" are applied on the outside of highlighting commands for things like "this is a postulate" [Issue #2474].

Example: Instead of generating \AgdaPostulate{\AgdaUnsolvedMeta{F}} Agda now generates \AgdaUnsolvedMeta{\AgdaPostulate{F}}.

The package agda.sty no longer selects any fonts, and no longer changes the input or font encodings [Issue #3224].

The new behaviour is the same as the old behaviour with the options nofontsetup and noinputencodingsetup. These options have been removed.

One reason for this change is that several persons have received complaints from reviewers because they have unwittingly used non-standard fonts in submitted papers. Another is that the utf8x option to inputenc is now deprecated.

Note that Agda code is now less likely to typeset properly out of the box. See the documentation for some hints about what to do if this affects you.

Some text was by default typeset in math mode when LuaLaTeX or XeLaTeX were used, and in text mode when pdfLaTeX was used. Now text mode is the default for all of these engines.
Typesetting of pragmas should now work better [Issue #2452].

The \AgdaOption command and AgdaOption colour have been replaced by \AgdaPragma and AgdaPragma. The \AgdaPragma command is used where \AgdaOption used to be used (for certain options), but also in other cases (for other options and certain other text in pragmas).

There is no longer any special treatment of the character - [Issue #2452].

This might, depending on things like what font your are using, mean that the token -- is typeset like an en dash (–). However, this is not the case for at least one common monospace font (in at least one setting).

The default value of \AgdaEmptySkip has been changed from \baselineskip to \abovedisplayskip. This could mean that less vertical space is used to render empty lines in code blocks.

HTML backend

New option --html-highlight=[code,all,auto].

The option --html-highlight=code makes the HTML-backend generate files with:

No HTML footer/header
Agda codes highlighted
Non-Agda code parts as-is
Output file extension as-is (i.e. .lagda.md becomes .md)
For ReStructuredText, a .. raw:: html\n will be inserted before every code blocks

This makes it possible to use an ordinary Markdown/ReStructuredText processor to render the generated HTML.

This will affect all the files involved in one compilation, making pure Agda code files rendered without HTML footer/header as well. To use code with literate Agda files and all with pure Agda files, use --html-highlight=auto, which means auto-detection.

The old and default behaviour is still --html-highlight=all.

List of all closed issues

For 2.6.0, the following issues have been closed (see bug tracker):

#572: Shadowed identifiers should be preceded by a dot when printed
#723: Instance search needs to know whether a meta must be a function type
#758: No highlighting for syntax declarations
#887: Case-split causes problems for coverage checker
#952: Parse named implicit pi {x = y : A} -> B
#1003: No highlighting for ambiguous instance argument
#1063: Freeze metas in module telescope after checking the module?
#1086: Make absurd patterns not needed at toplevel
#1209: Guardedness checker inconsistency with copatterns
#1581: Fields of opened records sometimes highlighted, sometimes not
#1602: NonStrict arguments should be allowed to occur relevantly in the type
#1706: Feature request: ML-style forall-generalization
#1764: Type in type and universe polymorphism
#1886: Second copies of telescopes not checked?
#1909: parameters are not dropped from reflected pattern lambda
#1913: Names that are not in scope can sometimes be candidates for instance resolution
#1995: Correct names in goal types after multiple renaming imports.
#2044: Better diagnosis for failed instance search
#2089: ''No such module'' is a rude error message for private modules
#2153: PDF version of Language Documentation on readthedocs lacks most Unicode characters
#2273: C-c C-s should put new goals instead of underscores for unknown subterms
#2351: expose noConstraints to reflection framework
#2452: The LaTeX backend does not handle options very well
#2473: Don't reread the source code without checking that it is unchanged
#2487: Options used for different modules must be consistent with each other, and options used when loading an interface must be consistent with those used when the interface was created
#2489: Where clauses in functions leak instances to global instance search
#2490: possible non-terminating inference of instance arguments?
#2513: Extensible syntax for function space annotations
#2548: Move the "Old Reference Manual" to the current documentation
#2563: Improve documentation and error reporting related to instance resolution (especially unconstrained metavariables)
#2579: Import statements with module instantiation should not trigger an error message
#2618: Reflection and pattern-matching lambdas
#2670: Instance arguments and multi-sorted algebras
#2757: Proposal: split non-strict relevance into shape-irrelevance, parametricity, and runtime-irrelevance
#2760: Relax instance search restriction on unconstrained metas
#2774: Internal error with sized types
#2783: Make more primitive/builtin modules safe?
#2789: Narrow and broad options
#2791: More illtyped meta solutions
#2797: Relevance check missed for overloaded projection
#2833: Coverage checker splits on result too eagerly
#2837: The Emacs mode only handles LaTeX-based literate Agda
#2872: Case splitting adds a dot in front of pattern matches on Chars
#2880: Disallow FFI binding for defined functions when --safe is used
#2892: 'With' should also abstract over the type of stripped dot patterns
#2893: Display warnings also when an error is encountered
#2899: Add a warning for infix notations without corresponding fixity declaration
#2929: Turn "missing definition" into a warning
#2936: Sort warning flags alphabetically in user manual
#2939: make install-bin on a Mac can fail to install text-icu
#2964: Mismatch between order of matching in clauses and case tree; subject reduction broken
#2969: Module parameter is erased from dot pattern
#2979: Rewriting matching does not respect eta rules
#2993: Quadratic (failing) instance search
#3010: Field of opened record does not get highlighted
#3032: spurious meta in dot pattern
#3056: Matching on irrelevant variable of dependent record type should not be allowed
#3057: A module can export two definitions with the same name
#3068: Add option to turn off syntactic equality check
#3095: Would like to make hidden variable visible but it is created ambiguous
#3102: Performance regression: very slow reduction in the presence of many module parameters
#3114: Missing alpha-renaming when printing constraints
#3120: No tooltips for record field names in record expressions
#3122: Hidden record fields are not picked up from module in record expression
#3124: De Bruijn index in lhs checking error message
#3125: Internal error in InstanceArguments.hs:292
#3127: Notation for out-of-scope variables conflicts with notation for irrelevance
#3128: Sigma builtin not added to setup, agdai file missing.
#3130: Conflict between dot pattern and postfix projection
#3137: Preserve Markdown as-is when outputting HTML
#3138: Result splitter introduces pattern variable that conflicts with constructor
#3139: Internal error in parser
#3147: Non-linear as-patterns
#3152: give in a do-block inserts spurious parentheses
#3153: Type checker fails to infer missing signature of module parameter.
#3161: Case splitter produces end-of-comment
#3169: Doc for rewriting
#3170: UnicodeDeclare fails with pdflatex from TeX Live 2018
#3175: Instance resolution fails with defined method
#3176: Empty lambdas are sometimes considered definitionally equal, other times not
#3180: Remove feature --guardedness-preserving-type-constructors
#3188: Warnings disappear when fatal error is encountered
#3195: Internal error at Auto/Typecheck.hs:373
#3196: Turning MissingDefinition into a warning
#3200: Function marked as irrelevant when it isn't
#3201: [ warning ] AbsurdPatternRequiresNoRHS
#3205: [ cleanup + warning ] ModuleDoesntExport can be recovered from
#3224: Switch from utf8x to utf8? Make agda.sty easier to maintain?
#3235: Cannot pass backend flags via emacs variable agda2-program-args
#3247: Support cabal-install >= 2.4.1.0 in the Makefile
#3248: Max of two sizes less than i
#3253: [ fix ] ignore duplicate declarations of libraries
#3254: cpphs doesn't build with GHC 8.6.*
#3256: Internal error at src/full/Agda/TypeChecking/Reduce.hs:148
#3257: Anonymous top-level modules can have names with multiple components
#3258: Ordering the constructor names at Definition.
#3262: Suboptimal placement of "missing with-clauses" error
#3264: When refine leads to a termination error it should say so rather than "cannot refine"
#3268: [ haddock ] Fix haddock formatting
#3285: Internal error for syntax declaration
#3302: Multiple definitions called _ are sometimes allowed, sometimes not
#3307: --no-unicode bug: case splitting inside a pattern matching lambda still produces unicode arrows
#3309: Use of irrelevant arguments with copatterns and irrelevant fields
#3313: Add --html-highlight support for the HTML backend
#3315: The primErase primitive is not safe
#3318: Lots of primitives and builtins are not declared in the primitive/builtin modules
#3320: Extra indentation when code is hidden
#3323: Internal error with inconsistent irrelevance info between declaration and definition of data type
#3338: Missing Definitions not recognised in instance search
#3342: GHC panic on stack and GHC 7.10.3
#3344: Disable compilation with GHC 8.6.1
#3356: C-c C-s prints postfix projections by default
#3363: The wiki should support HTTPS
#3364: Funny scope error when trying to import as qualified
#3366: Add a command line flag to change the extension of the files generated by the HTML backend
#3368: Support GHC 8.6.2
#3370: [ fix ] < and > need to be in math mode in latex
#3371: Document common LaTeX backend pitfalls
#3372: Provide some simple LaTeX backend templates
#3373: Wrap HTML in raw directive when working with ReStructuredText
#3379: Adding a tutorial set in the readthedocs frontpage
#3380: Too much erasure in strict backends
#3394: Internal error in mutual block with unsolved implicit argument in termination checker
#3400: Obscure parse error with copattern and infix field
#3403: Internal error in Agda.TypeChecking.Rules.Term
#3404: Positivity checker marks postulates as constant in mutual block
#3407: Internal error at "src/full/Agda/TypeChecking/Reduce/Fast.hs:1338"
#3409: No error if mapping the empty type to non-empty Haskell type
#3410: ghc backend generates program that segfaults
#3419: Allow unconstrained instances & disallow overlapping instances
#3420: Inductive definitions live in a larger set --without-K
#3425: Internal error at src/full/Agda/Termination/Monad.hs:177
#3426: Termination checking false positive when using "where"
#3428: Another interal error in Substitute:72 when filling a hole
#3431: Rewrite rule doesn't fire during conversion checking
#3434: Regression related to instance resolution
#3435: Performance regression
#3439: Setω doesn’t respect --type-in-type
#3441: Generate Level expressions with fewer parentheses
#3442: Support GHC 8.6.3
#3443: "internal error" in Agda of December 7, 2018
#3444: Setup.hs is not generating the interface files
#3445: case splitting attempts to shadow constructor
#3451: The --no-sized-types option is broken
#3452: Case split on irrelevant argument goes through but is later rejected
#3454: Highlighting for incomplete pattern matching should be above highliting for non-exact split
#3456: [ new ] Injectivity of prim(NatToChar/StringToList)
#3461: Macro loop
#3463: Impossible to give certain instance arguments by name?
#3466: two definitionally equal terms are not equal
#3471: Can't install via cabal-install on current Haskell Platform
#3480: Parse error at EOF should be reported before EOF (especially if there is a long comment before EOF)
#3483: Internal error at TypeChecking/Monad/Signature.hs:732
#3485: [ warnings ] for empty primitive blocks
#3491: Internal error src/full/Agda/TypeChecking/Rules/LHS.hs:294 after pattern matching
#3498: Internal error in activateLoadedFileCache
#3501: Case split in let clause causes internal error
#3503: Internal error in BasicOps
#3514: Accidential language change in 2.5.3: hiding is now part of name when resolving hidden argument insertion
#3517: Option consistency checking bug
#3518: Performance regression
#3521: Documentation: fixes a plural issue in copatterns
#3526: Do not generate trivially impossible clause when case-splitting
#3533: [ fix #3526 ] Remove trivially impossible clauses from case-split
#3534: Problem finding higher-order instances
#3536: Patternmatching on coinductive record fields breaks
#3544: internal error @ TypeChecking/Forcing.hs:227
#3548: [ new ] Add support for compiling literate Org documents
#3554: Type checker explosion
#3561: fix typo: "FreBSD" => "FreeBSD"
#3566: Missing name when printing type of definition of a record
#3578: Pattern matching unifier normalizes too much
#3586: Internal error in ConcreteToAbstract.hs:2217
#3590: Superlinear time required for simple code
#3597: Agda loops on simple code with a record and a hole
#3600: Size solver complains, explicit sizes work
#3610: Support GHC 8.6.4
#3621: performance problem
#3631: Performance with --no-universe-polymorphism
#3638: Rewrite rules do not fire in goal normalization in parametrized module
#3639: Argument to function created by tactic is lost
#3640: Polarity: Size index check crashes due to wrong parameter number calculation
#3641: Remove old compiler pragmas
#3648: Agda could fail to build if a .agda-lib file exists in a parent directory
#3651: internal error ghc backend
#3657: Disable compilation with Windows and GHC 8.6.3
#3678: Two out-of-scope variables are given the same name
#3687: Show module contents (C-c C-o) prints garbled names in clause

2.6.0.md 43 KB 永久連結 文件歷史 原始文件