Skip to content

Latest commit

 

History

History
182 lines (134 loc) · 5.76 KB

CHANGELOG.md

File metadata and controls

182 lines (134 loc) · 5.76 KB
Raw

Release notes for Agda version 2.6.5

Highlights

Installation

  • Agda supports GHC versions 8.6.5 to 9.8.2.

Pragmas and options

  • The following options are now considered infective: (Issue #5264)

    • --allow-exec
    • --cumulativity
    • --experimental-irrelevance
    • --injective-type-constructors
    • --omega-in-omega
    • --rewriting
    • --type-in-type

    This means that if a module has one of these flags enabled, then all modules importing it must also have that flag enabled.

  • New warning UselessMacro when a macro block does not contain any function definitions.

  • New warning ConflictingPragmaOptions if giving both --this and --that when --this implies --no-that (and analogous for --no-this implies --that, etc).

  • [Breaking] The option --overlapping-instances, which allows backtracking during instance search, has been renamed to --backtracking-instance-search.

  • New warning WarningProblem when trying to switch an unknown or non-benign warning with the -W option. Used to be a hard error.

  • New option --require-unique-meta-solutions (turned on by default). Disabling it with --no-require-unique-meta-solutions allows the type checker to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below). The --lossy-unification flag implies --no-require-unique-meta-solutions.

  • New pragma INJECTIVE_FOR_INFERENCE, which treats functions as injective for inferring implicit arguments if --no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the file where the function is used, and not necessarily in the file where it is defined. For example:

    postulate
  reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'

[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})

    does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse []. If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.

Syntax

Additions to the Agda syntax.

  • Left-hand side let: using x ← e (PR #7078)

    This new construct can be use in left-hand sides together with with and rewrite to give names to subexpressions. It is the left-hand side counterpart of a let-binding and supports the same limited form of pattern matching on eta-expandable record values.

    It can be quite useful when you have a function doing a series of nested withs that share some expressions. Something like

    fun : A → B
fun x using z ← e with foo z
... | p with bar z
...   | q = r

    Here the expression e doesn't have to be repeated in the two with-expressions.

    As in a with, multiple bindings can be separated by a |, and variables to the left are in scope in bindings to the right.

  • Pattern synonyms can now expose existing instance arguments (PR 7173). Example:

    data D : Set where
  c : {{D}} → D

pattern p {{d}} = c {{d}}

    This allows us to explicitly bind these argument in a pattern match and supply them explicitly when using the pattern synonym in an expression.

    f : D → D
f (p {{d = x}}) = p {{d = x}}

    We cannot create new instance arguments this way, though. The following is rejected:

    data D : Set where
  c : D → D

pattern p {{d}} = c d

Language

Changes to type checker and other components defining the Agda language.

  • Agda now uses discrimination trees to store and look up instance definitions, rather than linearly searching through all instances for a given "class" (PR #7109).

    This is a purely internal change, and should not result in any change to which programs are accepted or rejected. However, it significantly improves the performance of instance search, especially for the case of a "type class" indexed by a single type argument. The new lookup procedure should never be slower than the previous implementation.

Reflection

Changes to the meta-programming facilities.

Library management

Interaction and emacs mode

  • The Auto command has been reimplemented from the ground up (PR #6410). This fixes problems where Auto would fail in the presence of language features it did not know about, such as copatterns or anything cubical.

    The reimplementation does not support case splitting (-c), disproving (-d) or refining (-r).

Backends

API

Highlighting some changes to Agda as a library.

  • New module Agda.Syntax.Common.KeywordRange providing type KwRange isomorphic to Range to indicate source positions that just span keywords (PR #7162). The motivation for KwRange is to distinguish such ranges from ranges for whole subtrees, e.g. in data type Agda.Syntax.Concrete.Declaration.

    API:

    module Agda.Syntax.Common.KeywordRange where

type KwRange

-- From Range to KwRange
kwRange :: HasRange a => a -> KwRange

-- From KwRange to Range
instance HasRange KwRange where
  getRange :: KwRange -> Range

Other issues closed

For 2.6.5, the following issues were also closed (see bug tracker):

NOTE: This section will be filled by output produced with closed-issues-for-milestone 2.6.5.