agda/doc/release-notes/2.5.1.md

Release notes for Agda version 2.5.1

Documentation

• There is now an official Agda User Manual: https://agda.readthedocs.io/

Installation and infrastructure

• Builtins and primitives are now defined in a new set of modules available to all users, independent of any particular library. The modules are

  Agda.Builtin.Bool
  Agda.Builtin.Char
  Agda.Builtin.Coinduction
  Agda.Builtin.Equality
  Agda.Builtin.Float
  Agda.Builtin.FromNat
  Agda.Builtin.FromNeg
  Agda.Builtin.FromString
  Agda.Builtin.IO
  Agda.Builtin.Int
  Agda.Builtin.List
  Agda.Builtin.Nat
  Agda.Builtin.Reflection
  Agda.Builtin.Size
  Agda.Builtin.Strict
  Agda.Builtin.String
  Agda.Builtin.TrustMe
  Agda.Builtin.Unit

The standard library reexports the primitives from the new modules.

The Agda.Builtin modules are installed in the same way as Agda.Primitive, but unlike Agda.Primitive they are not loaded automatically.

Pragmas and options

• Library management

There is a new 'library' concept for managing include paths. A library consists of

- a name,
- a set of libraries it depends on, and
- a set of include paths.

A library is defined in a .agda-lib file using the following format:

  name: LIBRARY-NAME  -- Comment
  depend: LIB1 LIB2
    LIB3
    LIB4
  include: PATH1
    PATH2
    PATH3

Dependencies are library names, not paths to .agda-lib files, and include paths are relative to the location of the library-file.

To be useable, a library file has to be listed (with its full path) in AGDA_DIR/libraries (or AGDA_DIR/libraries-VERSION, for a given Agda version). AGDA_DIR defaults to ~/.agda on Unix-like systems and C:/Users/USERNAME/AppData/Roaming/agda or similar on Windows, and can be overridden by setting the AGDA_DIR environment variable.

Environment variables in the paths (of the form $VAR or ${VAR}) are expanded. The location of the libraries file used can be overridden using the --library-file=FILE flag, although this is not expected to be very useful.

You can find out the precise location of the 'libraries' file by calling agda -l fjdsk Dummy.agda and looking at the error message (assuming you don't have a library called fjdsk installed).

There are three ways a library gets used:

- You supply the `--library=LIB` (or `-l LIB`) option to
  Agda. This is equivalent to adding a `-iPATH` for each of the
  include paths of `LIB` and its (transitive) dependencies.

- No explicit `--library` flag is given, and the current project
  root (of the Agda file that is being loaded) or one of its
  parent directories contains a `.agda-lib` file defining a
  library `LIB`. This library is used as if a `--librarary=LIB`
  option had been given, except that it is not necessary for the
  library to be listed in the `AGDA_DIR/libraries` file.

- No explicit `--library` flag, and no `.agda-lib` file in the
  project root. In this case the file `AGDA_DIR/defaults` is read
  and all libraries listed are added to the path. The defaults
  file should contain a list of library names, each on a separate
  line. In this case the current directory is also added to the
  path.

  To disable default libraries, you can give the flag
  `--no-default-libraries`.

Library names can end with a version number (for instance, mylib-1.2.3). When resolving a library name (given in a --library flag, or listed as a default library or library dependency) the following rules are followed:

- If you don't give a version number, any version will do.

- If you give a version number an exact match is required.

- When there are multiple matches an exact match is preferred, and
  otherwise the latest matching version is chosen.

For example, suppose you have the following libraries installed: mylib, mylib-1.0, otherlib-2.1, and otherlib-2.3. In this case, aside from the exact matches you can also say --library=otherlib to get otherlib-2.3.

• New Pragma COMPILED_DECLARE_DATA for binding recursively defined Haskell data types to recursively defined Agda data types.

If you have a Haskell type like

  {-# LANGUAGE GADTs #-}

  module Issue223 where

  data A where
    BA :: B -> A

  data B where
    AB :: A -> B
    BB :: B

You can now bind it to corresponding mutual Agda inductive data types as follows:

  {-# IMPORT Issue223 #-}

  data A : Set
  {-# COMPILED_DECLARE_DATA A Issue223.A #-}
  data B : Set
  {-# COMPILED_DECLARE_DATA B Issue223.B #-}

  data A where
    BA : B → A

  {-# COMPILED_DATA A Issue223.A Issue223.BA #-}
  data B where
    AB : A → B
    BB : B

  {-# COMPILED_DATA B Issue223.B Issue223.AB Issue223.BB #-}

This fixes Issue #223.

• New pragma HASKELL for adding inline Haskell code (GHC backend only)

Arbitrary Haskell code can be added to a module using the HASKELL pragma. For instance,

  {-# HASKELL
    echo :: IO ()
    echo = getLine >>= putStrLn
  #-}

  postulate echo : IO ⊤
  {-# COMPILED echo echo #-}

• New option --exact-split.

The --exact-split flag causes Agda to raise an error whenever a clause in a definition by pattern matching cannot be made to hold definitionally (i.e. as a reduction rule). Specific clauses can be excluded from this check by means of the {-# CATCHALL #-} pragma.

For instance, the following definition will be rejected as the second clause cannot be made to hold definitionally:

  min : Nat → Nat → Nat
  min zero    y       = zero
  min x       zero    = zero
  min (suc x) (suc y) = suc (min x y

Catchall clauses have to be marked as such, for instance:

  eq : Nat → Nat → Bool
  eq zero    zero    = true
  eq (suc m) (suc n) = eq m n
  {-# CATCHALL #-}
  eq _       _       = false

• New option: --no-exact-split.

This option can be used to override a global --exact-split in a file, by adding a pragma {-# OPTIONS --no-exact-split #-}.

• New options: --sharing and --no-sharing.

These options are used to enable/disable sharing and call-by-need evaluation. The default is --no-sharing.

Note that they cannot appear in an OPTIONS pragma, but have to be given as command line arguments or added to the Agda Program Args from Emacs with M-x customize-group agda2.

• New pragma DISPLAY.

  {-# DISPLAY f e1 .. en = e #-}

This causes f e1 .. en to be printed in the same way as e, where ei can bind variables used in e. The expressions ei and e are scope checked, but not type checked.

For example this can be used to print overloaded (instance) functions with the overloaded name:

  instance
    NumNat : Num Nat
    NumNat = record { ..; _+_ = natPlus }

  {-# DISPLAY natPlus a b = a + b #-}

Limitations

• Left-hand sides are restricted to variables, constructors, defined functions or types, and literals. In particular, lambdas are not allowed in left-hand sides.

• Since DISPLAY pragmas are not type checked implicit argument insertion may not work properly if the type of f computes to an implicit function space after pattern matching.

• Removed pragma {-# ETA R #-}

The pragma {-# ETA R #-} is replaced by the eta-equality directive inside record declarations.

• New option --no-eta-equality.

The --no-eta-equality flag disables eta rules for declared record types. It has the same effect as no-eta-equality inside each declaration of a record type R.

If used with the OPTIONS pragma it will not affect records defined in other modules.

• The semantics of {-# REWRITE r #-} pragmas in parametrized modules has changed (see Issue #1652).

Rewrite rules are no longer lifted to the top context. Instead, they now only apply to terms in (extensions of) the module context. If you want the old behaviour, you should put the {-# REWRITE r #-} pragma outside of the module (i.e. unindent it).

• New pragma {-# INLINE f #-} causes f to be inlined during compilation.

• The STATIC pragma is now taken into account during compilation.

Calls to a function marked STATIC are normalised before compilation. The typical use case for this is to mark the interpreter of an embedded language as STATIC.

• Option --type-in-type no longer implies --no-universe-polymorphism, thus, it can be used with explicit universe levels. [Issue #1764] It simply turns off error reporting for any level mismatch now. Examples:

  {-# OPTIONS --type-in-type #-}

  Type : Set
  Type = Set

  data D {α} (A : Set α) : Set where
    d : A → D A

  data E α β : Set β where
    e : Set α → E α β

• New NO_POSITIVITY_CHECK pragma to switch off the positivity checker for data/record definitions and mutual blocks.

The pragma must precede a data/record definition or a mutual block.

The pragma cannot be used in --safe mode.

Examples (see Issue1614*.agda and Issue1760*.agda in test/Succeed/):

1. Skipping a single data definition.

    {-# NO_POSITIVITY_CHECK #-}
    data D : Set where
      lam : (D → D) → D
   

2. Skipping a single record definition.

    {-# NO_POSITIVITY_CHECK #-}
    record U : Set where
      field ap : U → U
   

3. Skipping an old-style mutual block: Somewhere within a mutual block before a data/record definition.

    mutual
      data D : Set where
        lam : (D → D) → D
   
      {-# NO_POSITIVITY_CHECK #-}
      record U : Set where
        field ap : U → U
   

4. Skipping an old-style mutual block: Before the mutual keyword.

    {-# NO_POSITIVITY_CHECK #-}
    mutual
      data D : Set where
        lam : (D → D) → D
   
      record U : Set where
        field ap : U → U
   

5. Skipping a new-style mutual block: Anywhere before the declaration or the definition of data/record in the block.

    record U : Set
    data D   : Set
   
    record U where
      field ap : U → U
   
    {-# NO_POSITIVITY_CHECK #-}
    data D where
      lam : (D → D) → D
   

• Removed --no-coverage-check option. [Issue #1918]

Language

Operator syntax

• The default fixity for syntax declarations has changed from -666 to 20.

• Sections.

Operators can be sectioned by replacing arguments with underscores. There must not be any whitespace between these underscores and the adjacent nameparts. Examples:

  pred : ℕ → ℕ
  pred = _∸ 1

  T : Bool → Set
  T = if_then ⊤ else ⊥

  if : {A : Set} (b : Bool) → A → A → A
  if b = if b then_else_

Sections are translated into lambda expressions. Examples:

  _∸ 1              ↦  λ section → section ∸ 1

  if_then ⊤ else ⊥  ↦  λ section → if section then ⊤ else ⊥

  if b then_else_   ↦  λ section section₁ →
                           if b then section else section₁

Operator sections have the same fixity as the underlying operator (except in cases like if b then_else_, in which the section is "closed", but the operator is not).

Operator sections are not supported in patterns (with the exception of dot patterns), and notations coming from syntax declarations cannot be sectioned.

• A long-standing operator fixity bug has been fixed. As a consequence some programs that used to parse no longer do.

Previously each precedence level was (incorrectly) split up into five separate ones, ordered as follows, with the earlier ones binding less tightly than the later ones:

- Non-associative operators.

- Left associative operators.

- Right associative operators.

- Prefix operators.

- Postfix operators.

Now this problem has been addressed. It is no longer possible to mix operators of a given precedence level but different associativity. However, prefix and right associative operators are seen as having the same associativity, and similarly for postfix and left associative operators.

Examples

---

The following code is no longer accepted:

  infixl 6 _+_
  infix  6 _∸_

  rejected : ℕ
  rejected = 1 + 0 ∸ 1

However, the following previously rejected code is accepted:

  infixr 4 _,_
  infix  4 ,_

  ,_ : {A : Set} {B : A → Set} {x : A} → B x → Σ A B
  , y = _ , y

  accepted : Σ ℕ λ i → Σ ℕ λ j → Σ (i ≡ j) λ _ → Σ ℕ λ k → j ≡ k
  accepted = 5 , , refl , , refl

• The classification of notations with binders into the categories infix, prefix, postfix or closed has changed. [Issue #1450]

The difference is that, when classifying the notation, only regular holes are taken into account, not binding ones.

Example: The notation

  syntax m >>= (λ x → f) = x <- m , f

was previously treated as infix, but is now treated as prefix.

• Notation can now include wildcard binders.

Example: syntax Σ A (λ _ → B) = A × B

• If an overloaded operator is in scope with several distinct precedence levels, then several instances of this operator will be included in the operator grammar, possibly leading to ambiguity. Previously the operator was given the default fixity [Issue #1436].

There is an exception to this rule: If there are multiple precedences, but at most one is explicitly declared, then only one instance will be included in the grammar. If there are no explicitly declared precedences, then this instance will get the default precedence, and otherwise it will get the declared precedence.

If multiple occurrences of an operator are "merged" in the grammar, and they have distinct associativities, then they are treated as being non-associative.

The three paragraphs above also apply to identical notations (coming from syntax declarations) for a given overloaded name.

Examples:

  module A where

    infixr 5 _∷_
    infixr 5 _∙_
    infixl 3 _+_
    infix  1 bind

    syntax bind c (λ x → d) = x ← c , d

  module B where

    infix  5 _∷_
    infixr 4 _∙_
    -- No fixity declaration for _+_.
    infixl 2 bind

    syntax bind c d = c ∙ d

  module C where

    infixr 2 bind

    syntax bind c d = c ∙ d

  open A
  open B
  open C

  -- _∷_ is infix 5.
  -- _∙_ has two fixities: infixr 4 and infixr 5.
  -- _+_ is infixl 3.
  -- A.bind's notation is infix 1.
  -- B.bind and C.bind's notations are infix 2.

  -- There is one instance of "_ ∷ _" in the grammar, and one
  -- instance of "_ + _".

  -- There are three instances of "_ ∙ _" in the grammar, one
  -- corresponding to A._∙_, one corresponding to B._∙_, and one
  -- corresponding to both B.bind and C.bind.

Reflection

• The reflection framework has received a massive overhaul.

A new type of reflected type checking computations supplants most of the old reflection primitives. The quoteGoal, quoteContext and tactic primitives are deprecated and will be removed in the future, and the unquoteDecl and unquote primitives have changed behaviour. Furthermore the following primitive functions have been replaced by builtin type checking computations:

  - primQNameType              --> AGDATCMGETTYPE
  - primQNameDefinition        --> AGDATCMGETDEFINITION
  - primDataConstructors       --> subsumed by AGDATCMGETDEFINITION
  - primDataNumberOfParameters --> subsumed by AGDATCMGETDEFINITION

See below for details.

• Types are no longer packaged with a sort.

The AGDATYPE and AGDATYPEEL built-ins have been removed. Reflected types are now simply terms.

• Reflected definitions have more information.

The type for reflected definitions has changed to

  data Definition : Set where
    fun-def     : List Clause  → Definition
    data-type   : Nat → List Name → Definition -- parameters and constructors
    record-type : Name → Definition            -- name of the data/record type
    data-con    : Name → Definition            -- name of the constructor
    axiom       : Definition
    prim-fun    : Definition

Correspondingly the built-ins for function, data and record definitions (AGDAFUNDEF, AGDAFUNDEFCON, AGDADATADEF, AGDARECORDDEF) have been removed.

• Reflected type checking computations.

There is a primitive TC monad representing type checking computations. The unquote, unquoteDecl, and the new unquoteDef all expect computations in this monad (see below). The interface to the monad is the following

  -- Error messages can contain embedded names and terms.
  data ErrorPart : Set where
    strErr  : String → ErrorPart
    termErr : Term → ErrorPart
    nameErr : Name → ErrorPart

  {-# BUILTIN AGDAERRORPART       ErrorPart #-}
  {-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
  {-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
  {-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}

  postulate
    TC         : ∀ {a} → Set a → Set a
    returnTC   : ∀ {a} {A : Set a} → A → TC A
    bindTC     : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B

    -- Unify two terms, potentially solving metavariables in the process.
    unify      : Term → Term → TC ⊤

    -- Throw a type error. Can be caught by catchTC.
    typeError  : ∀ {a} {A : Set a} → List ErrorPart → TC A

    -- Block a type checking computation on a metavariable. This will abort
    -- the computation and restart it (from the beginning) when the
    -- metavariable is solved.
    blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A

    -- Backtrack and try the second argument if the first argument throws a
    -- type error.
    catchTC    : ∀ {a} {A : Set a} → TC A → TC A → TC A

    -- Infer the type of a given term
    inferType  : Term → TC Type

    -- Check a term against a given type. This may resolve implicit arguments
    -- in the term, so a new refined term is returned. Can be used to create
    -- new metavariables: newMeta t = checkType unknown t
    checkType  : Term → Type → TC Term

    -- Compute the normal form of a term.
    normalise  : Term → TC Term

    -- Get the current context.
    getContext : TC (List (Arg Type))

    -- Extend the current context with a variable of the given type.
    extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A

    -- Set the current context.
    inContext     : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A

    -- Quote a value, returning the corresponding Term.
    quoteTC : ∀ {a} {A : Set a} → A → TC Term

    -- Unquote a Term, returning the corresponding value.
    unquoteTC : ∀ {a} {A : Set a} → Term → TC A

    -- Create a fresh name.
    freshName  : String → TC QName

    -- Declare a new function of the given type. The function must be defined
    -- later using 'defineFun'. Takes an Arg Name to allow declaring instances
    -- and irrelevant functions. The Visibility of the Arg must not be hidden.
    declareDef : Arg QName → Type → TC ⊤

    -- Define a declared function. The function may have been declared using
    -- 'declareDef' or with an explicit type signature in the program.
    defineFun  : QName → List Clause → TC ⊤

    -- Get the type of a defined name. Replaces 'primQNameType'.
    getType    : QName → TC Type

    -- Get the definition of a defined name. Replaces 'primQNameDefinition'.
    getDefinition : QName → TC Definition

  {-# BUILTIN AGDATCM                   TC                 #-}
  {-# BUILTIN AGDATCMRETURN             returnTC           #-}
  {-# BUILTIN AGDATCMBIND               bindTC             #-}
  {-# BUILTIN AGDATCMUNIFY              unify              #-}
  {-# BUILTIN AGDATCMNEWMETA            newMeta            #-}
  {-# BUILTIN AGDATCMTYPEERROR          typeError          #-}
  {-# BUILTIN AGDATCMBLOCKONMETA        blockOnMeta        #-}
  {-# BUILTIN AGDATCMCATCHERROR         catchTC            #-}
  {-# BUILTIN AGDATCMINFERTYPE          inferType          #-}
  {-# BUILTIN AGDATCMCHECKTYPE          checkType          #-}
  {-# BUILTIN AGDATCMNORMALISE          normalise          #-}
  {-# BUILTIN AGDATCMGETCONTEXT         getContext         #-}
  {-# BUILTIN AGDATCMEXTENDCONTEXT      extendContext      #-}
  {-# BUILTIN AGDATCMINCONTEXT          inContext          #-}
  {-# BUILTIN AGDATCMQUOTETERM          quoteTC            #-}
  {-# BUILTIN AGDATCMUNQUOTETERM        unquoteTC          #-}
  {-# BUILTIN AGDATCMFRESHNAME          freshName          #-}
  {-# BUILTIN AGDATCMDECLAREDEF         declareDef         #-}
  {-# BUILTIN AGDATCMDEFINEFUN          defineFun          #-}
  {-# BUILTIN AGDATCMGETTYPE            getType            #-}
  {-# BUILTIN AGDATCMGETDEFINITION      getDefinition      #-}

• Builtin type for metavariables

There is a new builtin type for metavariables used by the new reflection framework. It is declared as follows and comes with primitive equality, ordering and show.

  postulate Meta : Set
  {-# BUILTIN AGDAMETA Meta #-}
  primitive primMetaEquality : Meta → Meta → Bool
  primitive primMetaLess : Meta → Meta → Bool
  primitive primShowMeta : Meta → String

There are corresponding new constructors in the Term and Literal data types:

  data Term : Set where
    ...
    meta : Meta → List (Arg Term) → Term

  {-# BUILTIN AGDATERMMETA meta #-}

  data Literal : Set where
    ...
    meta : Meta → Literal

  {-# BUILTIN AGDALITMETA meta #-}

• Builtin unit type

The type checker needs to know about the unit type, which you can allow by

  record ⊤ : Set where
  {-# BUILTIN UNIT ⊤ #-}

• Changed behaviour of unquote

The unquote primitive now expects a type checking computation instead of a pure term. In particular unquote e requires

  e : Term → TC ⊤

where the argument is the representation of the hole in which the result should go. The old unquote behaviour (where unquote expected a Term argument) can be recovered by

  OLD: unquote v
  NEW: unquote λ hole → unify hole v

• Changed behaviour of unquoteDecl

The unquoteDecl primitive now expects a type checking computation instead of a pure function definition. It is possible to define multiple (mutually recursive) functions at the same time. More specifically

  unquoteDecl x₁ .. xₙ = m

requires m : TC ⊤ and that x₁ .. xₙ are defined (using declareDef and defineFun) after executing m. As before x₁ .. xₙ : QName in m, but have their declared types outside the unquoteDecl.

• New primitive unquoteDef

There is a new declaration

  unquoteDef x₁ .. xₙ = m

This works exactly as unquoteDecl (see above) with the exception that x₁ .. xₙ are required to already be declared.

The main advantage of unquoteDef over unquoteDecl is that unquoteDef is allowed in mutual blocks, allowing mutually recursion between generated definitions and hand-written definitions.

• The reflection interface now exposes the name hint (as a string) for variables. As before, the actual binding structure is with de Bruijn indices. The String value is just a hint used as a prefix to help display the variable. The type Abs is a new builtin type used for the constructors Term.lam, Term.pi, Pattern.var (bultins AGDATERMLAM, AGDATERMPI and AGDAPATVAR).

  data Abs (A : Set) : Set where
    abs : (s : String) (x : A) → Abs A
  {-# BUILTIN ABS    Abs #-}
  {-# BUILTIN ABSABS abs #-}

Updated constructor types:

  Term.lam    : Hiding   → Abs Term → Term
  Term.pi     : Arg Type → Abs Type → Term
  Pattern.var : String   → Pattern

• Reflection-based macros

Macros are functions of type t1 → t2 → .. → Term → TC ⊤ that are defined in a macro block. Macro application is guided by the type of the macro, where Term arguments desugar into the quoteTerm syntax and Name arguments into the quote syntax. Arguments of any other type are preserved as-is. The last Term argument is the hole term given to unquote computation (see above).

For example, the macro application f u v w where the macro f has the type Term → Name → Bool → Term → TC ⊤ desugars into unquote (f (quoteTerm u) (quote v) w)

Limitations:

- Macros cannot be recursive. This can be worked around by defining the
  recursive function outside the macro block and have the macro call the
  recursive function.

Silly example:

  macro
    plus-to-times : Term → Term → TC ⊤
    plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
    plus-to-times v hole = unify hole v

  thm : (a b : Nat) → plus-to-times (a + b) ≡ a * b
  thm a b = refl

Macros are most useful when writing tactics, since they let you hide the reflection machinery. For instance, suppose you have a solver

  magic : Type → Term

that takes a reflected goal and outputs a proof (when successful). You can then define the following macro

  macro
    by-magic : Term → TC ⊤
    by-magic hole =
      bindTC (inferType hole) λ goal →
      unify hole (magic goal)

This lets you apply the magic tactic without any syntactic noise at all:

  thm : ¬ P ≡ NP
  thm = by-magic

Literals and built-ins

• Overloaded number literals.

You can now overload natural number literals using the new builtin FROMNAT:

  {-# BUILTIN FROMNAT fromNat #-}

The target of the builtin should be a defined name. Typically you would do something like

  record Number (A : Set) : Set where
    field fromNat : Nat → A

  open Number {{...}} public

  {-# BUILTIN FROMNAT fromNat #-}

This will cause number literals n to be desugared to fromNat n before type checking.

• Negative number literals.

Number literals can now be negative. For floating point literals it works as expected. For integer literals there is a new builtin FROMNEG that enables negative integer literals:

  {-# BUILTIN FROMNEG fromNeg #-}

This causes negative literals -n to be desugared to fromNeg n.

• Overloaded string literals.

String literals can be overladed using the FROMSTRING builtin:

  {-# BUILTIN FROMSTRING fromString #-}

The will cause string literals s to be desugared to fromString s before type checking.

• Change to builtin integers.

The INTEGER builtin now needs to be bound to a datatype with two constructors that should be bound to the new builtins INTEGERPOS and INTEGERNEGSUC as follows:

  data Int : Set where
    pos    : Nat -> Int
    negsuc : Nat -> Int
  {-# BUILTIN INTEGER       Int    #-}
  {-# BUILTIN INTEGERPOS    pos    #-}
  {-# BUILTIN INTEGERNEGSUC negsuc #-}

where negsuc n represents the integer -n - 1. For instance, -5 is represented as negsuc 4. All primitive functions on integers except primShowInteger have been removed, since these can be defined without too much trouble on the above representation using the corresponding functions on natural numbers.

The primitives that have been removed are

  primIntegerPlus
  primIntegerMinus
  primIntegerTimes
  primIntegerDiv
  primIntegerMod
  primIntegerEquality
  primIntegerLess
  primIntegerAbs
  primNatToInteger

• New primitives for strict evaluation

  primitive
    primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
    primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x

primForce x f evaluates to f x if x is in weak head normal form, and primForceLemma x f evaluates to refl in the same situation. The following values are considered to be in weak head normal form:

- constructor applications
- literals
- lambda abstractions
- type constructor (data/record types) applications
- function types
- Set a

Modules

• Modules in import directives

When you use using/hiding/renaming on a name it now automatically applies to any module of the same name, unless you explicitly mention the module. For instance,

  open M using (D)

is equivalent to

  open M using (D; module D)

if M defines a module D. This is most useful for record and data types where you always get a module of the same name as the type.

With this feature there is no longer useful to be able to qualify a constructor (or field) by the name of the data type even when it differs from the name of the corresponding module. The follow (weird) code used to work, but doesn't work anymore:

  module M where
    data D where
      c : D
  open M using (D) renaming (module D to MD)
  foo : D
  foo = D.c

If you want to import only the type name and not the module you have to hide it explicitly:

  open M using (D) hiding (module D)

See discussion on Issue #836.

• Private definitions of a module are no longer in scope at the Emacs mode top-level.

The reason for this change is that .agdai-files are stripped of unused private definitions (which can yield significant performance improvements for module-heavy code).

To test private definitions you can create a hole at the bottom of the module, in which private definitions will be visible.

Records

• New record directives eta-equality/no-eta-equality

The keywords eta-equality/no-eta-equality enable/disable eta rules for the (inductive) record type being declared.

  record Σ (A : Set) (B : A -> Set) : Set where
    no-eta-equality
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ

  -- fail : ∀ {A : Set}{B : A -> Set} → (x : Σ A B) → x ≡ (fst x , snd x)
  -- fail x = refl
  --
  -- x != fst x , snd x of type Σ .A .B
  -- when checking that the expression refl has type x ≡ (fst x , snd x)

• Building records from modules.

The record { <fields> } syntax is now extended to accept module names as well. Fields are thus defined using the corresponding definitions from the given module.

For instance assuming this record type R and module M:

  record R : Set where
    field
      x : X
      y : Y
      z : Z

  module M where
    x = {! ... !}
    y = {! ... !}

  r : R
  r = record { M; z = {! ... !} }

Previously one had to write record { x = M.x; y = M.y; z = {! ... !} }.

More precisely this construction now supports any combination of explicit field definitions and applied modules.

If a field is both given explicitly and available in one of the modules, then the explicit one takes precedence.

If a field is available in more than one module then this is ambiguous and therefore rejected. As a consequence the order of assignments does not matter.

The modules can be both applied to arguments and have import directives such as hiding, using, and renaming. In particular this construct subsumes the record update construction.

Here is an example of record update:

  -- Record update. Same as: record r { y = {! ... !} }
  r2 : R
  r2 = record { R r; y = {! ... !} }

A contrived example showing the use of hiding/renaming:

  module M2 (a : A) where
    w = {! ... !}
    z = {! ... !}

  r3 : A → R
  r3 a = record { M hiding (y); M2 a renaming (w to y) }

• Record patterns are now accepted.

Examples:

  swap : {A B : Set} (p : A × B) → B × A
  swap record{ proj₁ = a; proj₂ = b } = record{ proj₁ = b; proj₂ = a }

  thd3 : ...
  thd3 record{ proj₂ = record { proj₂ = c }} = c

• Record modules now properly hide all their parameters [Issue #1759]

Previously parameters to parent modules were not hidden in the record module, resulting in different behaviour between

  module M (A : Set) where
    record R (B : Set) : Set where

and

  module M where
    record R (A B : Set) : Set where

where in the former case, A would be an explicit argument to the module M.R, but implicit in the latter case. Now A is implicit in both cases.

Instance search

• Performance has been improved, recursive instance search which was previously exponential in the depth is now only quadratic.

• Constructors of records and datatypes are not anymore automatically considered as instances, you have to do so explicitely, for instance:

  -- only [b] is an instance of D
  data D : Set where
    a : D
    instance
      b : D
    c : D

  -- the constructor is now an instance
  record tt : Set where
    instance constructor tt

• Lambda-bound variables are no longer automatically considered instances.

Lambda-bound variables need to be bound as instance arguments to be considered for instance search. For example,

  _==_ : {A : Set} {{_ : Eq A}} → A → A → Bool

  fails : {A : Set} → Eq A → A → Bool
  fails eqA x = x == x

  works : {A : Set} {{_ : Eq A}} → A → Bool
  works x = x == x

• Let-bound variables are no longer automatically considered instances.

To make a let-bound variable available as an instance it needs to be declared with the instance keyword, just like top-level instances. For example,

  mkEq : {A : Set} → (A → A → Bool) → Eq A

  fails : {A : Set} → (A → A → Bool) → A → Bool
  fails eq x = let eqA = mkEq eq in x == x

  works : {A : Set} → (A → A → Bool) → A → Bool
  works eq x = let instance eqA = mkEq eq in x == x

• Record fields can be declared instances.

For example,

  record EqSet : Set₁ where
    field
      set : Set
      instance eq : Eq set

This causes the projection function eq : (E : EqSet) → Eq (set E) to be considered for instance search.

• Instance search can now find arguments in variable types (but such candidates can only be lambda-bound variables, they can’t be declared as instances)

  module _ {A : Set} (P : A → Set) where

    postulate
      bla : {x : A} {{_ : P x}} → Set → Set

    -- Works, the instance argument is found in the context
    test :  {x : A} {{_ : P x}} → Set → Set
    test B = bla B

    -- Still forbidden, because [P] could be instantiated later to anything
    instance
     postulate
      forbidden : {x : A} → P x

• Instance search now refuses to solve constraints with unconstrained metavariables, since this can lead to non-termination.

See [Issue #1532] for an example.

• Top-level instances are now only considered if they are in scope. [Issue #1913]

Note that lambda-bound instances need not be in scope.

Other changes

• Unicode ellipsis character is allowed for the ellipsis token ... in with expressions.

• Prop is no longer a reserved word.

Type checking

• Large indices.

Force constructor arguments no longer count towards the size of a datatype. For instance, the definition of equality below is accepted.

  data _≡_ {a} {A : Set a} : A → A → Set where
    refl : ∀ x → x ≡ x

This gets rid of the asymmetry that the version of equality which indexes only on the second argument could be small, but not the version above which indexes on both arguments.

• Detection of datatypes that satisfy K (i.e. sets)

Agda will now try to detect datatypes that satisfy K when --without-K is enabled. A datatype satisfies K when it follows these three rules:

• The types of all non-recursive constructor arguments should satisfy K.

• All recursive constructor arguments should be first-order.

• The types of all indices should satisfy K.

For example, the types Nat, List Nat, and x ≡ x (where x : Nat) are all recognized by Agda as satisfying K.

• New unifier for case splitting

The unifier used by Agda for case splitting has been completely rewritten. The new unifier takes a much more type-directed approach in order to avoid the problems in issues #1406, #1408, #1427, and #1435.

The new unifier also has eta-equality for record types built-in. This should avoid unnecessary case splitting on record constructors and improve the performance of Agda on code that contains deeply nested record patterns (see issues #473, #635, #1575, #1603, #1613, and #1645).

In some cases, the locations of the dot patterns computed by the unifier did not correspond to the locations given by the user (see Issue #1608). This has now been fixed by adding an extra step after case splitting that checks whether the user-written patterns are compatible with the computed ones.

In some rare cases, the new unifier is still too restrictive when --without-K is enabled because it cannot generalize over the datatype indices (yet). For example, the following code is rejected:

  data Bar : Set₁ where
    bar : Bar
    baz : (A : Set) → Bar

  data Foo : Bar → Set where
    foo : Foo bar

  test : foo ≡ foo → Set₁
  test refl = Set

• The aggressive behaviour of with introduced in 2.4.2.5 has been rolled back [Issue #1692]. With no longer abstracts in the types of variables appearing in the with-expressions. [Issue #745]

This means that the following example no longer works:

  fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  fails f b with a | f b
  fails f b | .b | refl = f b

The with no longer abstracts the type of f over a, since f appears in the second with-expression f b. You can use a nested with to make this example work.

This example does work again:

  test : ∀{A : Set}{a : A}{f : A → A} (p : f a ≡ a) → f (f a) ≡ a
  test p rewrite p = p

After rewrite p the goal has changed to f a ≡ a, but the type of p has not been rewritten, thus, the final p solves the goal.

The following, which worked in 2.4.2.5, no longer works:

  fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  fails f b rewrite f b = f b

The rewrite with f b : a ≡ b is not applied to f as the latter is part of the rewrite expression f b. Thus, the type of f remains untouched, and the changed goal b ≡ b is not solved by f b.

• When using rewrite on a term eq of type lhs ≡ rhs, the lhs is no longer abstracted in rhs [Issue #520]. This means that

  f pats rewrite eq = body

is more than syntactic sugar for

  f pats with lhs | eq
  f pats | _ | refl = body

In particular, the following application of rewrite is now possible

  id : Bool → Bool
  id true  = true
  id false = false

  is-id : ∀ x → x ≡ id x
  is-id true  = refl
  is-id false = refl

  postulate
    P : Bool → Set
    b : Bool
    p : P (id b)

  proof : P b
  proof rewrite is-id b = p

Previously, this was desugared to

  proof with b | is-id b
  proof | _ | refl = p

which did not type check as refl does not have type b ≡ id b. Now, Agda gets the task of checking refl : _ ≡ id b leading to instantiation of _ to id b.

Compiler backends

• Major Bug Fixes:

  • Function clauses with different arities are now always compiled correctly by the GHC/UHC backends. (Issue #727)

• Co-patterns

  • The GHC/UHC backends now support co-patterns. (Issues #1567, #1632)

• Optimizations

  • Builtin naturals are now represented as arbitrary-precision Integers. See the user manual, section "Agda Compilers -> Optimizations" for details.

• GHC Haskell backend (MAlonzo)

  • Pragmas

  Since builtin naturals are compiled to Integer you can no longer give a {-# COMPILED_DATA #-} pragma for Nat. The same goes for builtin booleans, integers, floats, characters and strings which are now hard-wired to appropriate Haskell types.

• UHC compiler backend

A new backend targeting the Utrecht Haskell Compiler (UHC) is available. It targets the UHC Core language, and it's design is inspired by the Epic backend. See the user manual, section "Agda Compilers -> UHC Backend" for installation instructions.

• FFI

  The UHC backend has a FFI to Haskell similar to MAlonzo's. The target Haskell code also needs to be compilable using UHC, which does not support the Haskell base library version 4.*.

  FFI pragmas for the UHC backend are not checked in any way. If the pragmas are wrong, bad things will happen.

• Imports

  Additional Haskell modules can be brought into scope with the IMPORT_UHC pragma:

  {-# IMPORT_UHC Data.Char #-}
  

  The Haskell modules UHC.Base and UHC.Agda.Builtins are always in scope and don't need to be imported explicitly.

• Datatypes

  Agda datatypes can be bound to Haskell datatypes as follows:

  Haskell:

  data HsData a = HsCon1 | HsCon2 (HsData a)
  

  Agda:

  data AgdaData (A : Set) : Set where
    AgdaCon1 : AgdaData A
    AgdaCon2 : AgdaData A -> AgdaData A
  {-# COMPILED_DATA_UHC AgdaData HsData HsCon1 HsCon2 #-}
  

  The mapping has to cover all constructors of the used Haskell datatype, else runtime behavior is undefined!

  There are special reserved names to bind Agda datatypes to certain Haskell datatypes. For example, this binds an Agda datatype to Haskell's list datatype:

  Agda:

  data AgdaList (A : Set) : Set where
    Nil : AgdaList A
    Cons : A -> AgdaList A -> AgdaList A
  {-# COMPILED_DATA_UHC AgdaList __LIST__ __NIL__ __CONS__ #-}
  

  The following "magic" datatypes are available:

  HS Datatype | Datatype Pragma | HS Constructor | Constructor Pragma
  ()            __UNIT__          ()               __UNIT__
  List          __LIST__          (:)              __CONS__
                                  []               __NIL__
  Bool          __BOOL__          True             __TRUE__
                                  False            __FALSE__
  

• Functions

  Agda postulates can be bound to Haskell functions. Similar as in MAlonzo, all arguments of type Set need to be dropped before calling Haskell functions. An example calling the return function:

  Agda:

  postulate hs-return : {A : Set} -> A -> IO A
  {-# COMPILED_UHC hs-return (\_ -> UHC.Agda.Builtins.primReturn) #-}
  

Emacs mode and interaction

• Module contents (C-c C-o) now also works for records. [See Issue #1926 ] If you have an inferable expression of record type in an interaction point, you can invoke C-c C-o to see its fields and types. Example

  record R : Set where
    field f : A

  test : R → R
  test r = {!r!}  -- C-c C-o here

• Less aggressive error notification.

Previously Emacs could jump to the position of an error even if the type-checking process was not initiated in the current buffer. Now this no longer happens: If the type-checking process was initiated in another buffer, then the cursor is moved to the position of the error in the buffer visiting the file (if any) and in every window displaying the file, but focus should not change from one file to another.

In the cases where focus does change from one file to another, one can now use the go-back functionality to return to the previous position.

• Removed the agda-include-dirs customization parameter.

Use agda-program-args with -iDIR or -lLIB instead, or add libraries to ~/.agda/defaults (C:/Users/USERNAME/AppData/Roaming/agda/defaults or similar on Windows). See Library management, above, for more information.

Tools

LaTeX-backend

• The default font has been changed to XITS (which is part of TeX Live):

  http://www.ctan.org/tex-archive/fonts/xits/

This font is more complete with respect to Unicode.

agda-ghc-names

• New tool: The command

  agda-ghc-names fixprof <compile-dir> <ProgName>.prof

converts *.prof files obtained from profiling runs of MAlonzo-compiled code to *.agdaIdents.prof, with the original Agda identifiers replacing the MAlonzo-generated Haskell identifiers.

For usage and more details, see src/agda-ghc-names/README.txt.

Highlighting and textual backends

• Names in import directives are now highlighted and are clickable. [Issue #1714] This leads also to nicer printing in the LaTeX and html backends.

Fixed issues

See bug tracker (milestone 2.5.1)