Version-2–2−6

 ------------------------------------------------------------------------
 -- Release notes for Agda 2 version 2.2.6
 ------------------------------------------------------------------------
 
 Important changes since 2.2.4:
 
 Language
 --------
 
 * Universe polymorphism (experimental extension).
 
   To enable universe polymorphism give the flag
   --universe-polymorphism on the command line or (recommended) as an
   OPTIONS pragma.
 
   When universe polymorphism is enabled Set takes an argument which is
   the universe level. For instance, the type of universe polymorphic
   identity is
 
     id : {a : Level} {A : Set a} → A → A.
 
   The type Level is isomorphic to the unary natural numbers and should be
   specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:
 
     data Level : Set where
       zero : Level
       suc  : Level → Level
 
     {-# BUILTIN LEVEL     Level #-}
     {-# BUILTIN LEVELZERO zero  #-}
     {-# BUILTIN LEVELSUC  suc   #-}
 
   There is an additional BUILTIN LEVELMAX for taking the maximum of two
   levels:
 
     max : Level → Level → Level
     max  zero    m      = m
     max (suc n)  zero   = suc n
     max (suc n) (suc m) = suc (max n m)
 
     {-# BUILTIN LEVELMAX max #-}
 
   The non-polymorphic universe levels Set, Set₁ and so on are sugar
   for Set zero, Set (suc zero), etc.
 
   At present there is no automatic lifting of types from one level to
   another. It can still be done (rather clumsily) by defining types
   like the following one:
 
     data Lifted {a} (A : Set a) : Set (suc a) where
       lift : A → Lifted A
 
   However, it is likely that automatic lifting is introduced at some
   point in the future.
 
 * Multiple constructors, record fields, postulates or primitives can
   be declared using a single type signature:
 
     data Bool : Set where
       false true : Bool
 
     postulate
       A B : Set
 
 * Record fields can be implicit:
 
     record R : Set₁ where
       field
         {A}         : Set
         f           : A → A
         {B C} D {E} : Set
         g           : B → C → E
 
   By default implicit fields are not printed.
 
 * Record constructors can be defined:
 
     record Σ (A : Set) (B : A → Set) : Set where
       constructor _,_
       field
         proj₁ : A
         proj₂ : B proj₁
 
   In this example _,_ gets the type
 
      (proj₁ : A) → B proj₁ → Σ A B.
 
   For implicit fields the corresponding constructor arguments become
   implicit.
 
   Note that the constructor is defined in the /outer/ scope, so any
   fixity declaration has to be given outside the record definition.
   The constructor is not in scope inside the record module.
 
   Note also that pattern matching for records has not been implemented
   yet.
 
 * BUILTIN hooks for equality.
 
   The data type
 
     data _≡_ {A : Set} (x : A) : A → Set where
       refl : x ≡ x
 
   can be specified as the builtin equality type using the following
   pragmas:
 
     {-# BUILTIN EQUALITY _≡_  #-}
     {-# BUILTIN REFL     refl #-}
 
   The builtin equality is used for the new rewrite construct and
   the primTrustMe primitive described below.
 
 * New rewrite construct.
 
   If eqn : a ≡ b, where _≡_ is the builtin equality (see above) you
   can now write
 
     f ps rewrite eqn = rhs
 
   instead of
 
     f ps with a | eqn
     ... | ._ | refl = rhs
 
   The rewrite construct has the effect of rewriting the goal and the
   context by the given equation (left to right).
 
   You can rewrite using several equations (in sequence) by separating
   them with vertical bars (|):
 
     f ps rewrite eqn₁ | eqn₂ | … = rhs
 
   It is also possible to add with clauses after rewriting:
 
     f ps rewrite eqns with e
     ... | p = rhs
 
   Note that pattern matching happens before rewriting—if you want to
   rewrite and then do pattern matching you can use a with after the
   rewrite.
 
   See test/succeed/Rewrite.agda for some examples.
 
 * A new primitive, primTrustMe, has been added:
 
     primTrustMe : {A : Set} {x y : A} → x ≡ y
 
   Here _≡_ is the builtin equality (see BUILTIN hooks for equality,
   above).
 
   If x and y are definitionally equal, then
   primTrustMe {x = x} {y = y} reduces to refl.
 
   Note that the compiler replaces all uses of primTrustMe with the
   REFL builtin, without any check for definitional equality. Incorrect
   uses of primTrustMe can potentially lead to segfaults or similar
   problems.
 
   For an example of the use of primTrustMe, see Data.String in version
   0.3 of the standard library, where it is used to implement decidable
   equality on strings using the primitive boolean equality.
 
 * Changes to the syntax and semantics of IMPORT pragmas, which are
   used by the Haskell FFI. Such pragmas must now have the following
   form:
 
     {-# IMPORT <module name> #-}
 
   These pragmas are interpreted as /qualified/ imports, so Haskell
   names need to be given qualified (unless they come from the Haskell
   prelude).
 
 * The horizontal tab character (U+0009) is no longer treated as white
   space.
 
 * Line pragmas are no longer supported.
 
 * The --include-path flag can no longer be used as a pragma.
 
 * The experimental and incomplete support for proof irrelevance has
   been disabled.
 
 Tools
 -----
 
 * New "intro" command in the Emacs mode. When there is a canonical way
   of building something of the goal type (for instance, if the goal
   type is a pair), the goal can be refined in this way. The command
   works for the following goal types:
 
     - A data type where only one of its constructors can be used to
       construct an element of the goal type. (For instance, if the
       goal is a non-empty vector, a "cons" will be introduced.)
 
     - A record type. A record value will be introduced. Implicit
       fields will not be included unless showing of implicit arguments
       is switched on.
 
     - A function type. A lambda binding as many variables as possible
       will be introduced. The variable names will be chosen from the
       goal type if its normal form is a dependent function type,
       otherwise they will be variations on "x". Implicit lambdas will
       only be inserted if showing of implicit arguments is switched
       on.
 
   This command can be invoked by using the refine command (C-c C-r)
   when the goal is empty. (The old behaviour of the refine command in
   this situation was to ask for an expression using the minibuffer.)
 
 * The Emacs mode displays "Checked" in the mode line if the current
   file type checked successfully without any warnings.
 
 * If a file F is loaded, and this file defines the module M, it is an
   error if F is not the file which defines M according to the include
   path.
 
   Note that the command-line tool and the Emacs mode define the
   meaning of relative include paths differently: the command-line tool
   interprets them relative to the current working directory, whereas
   the Emacs mode interprets them relative to the root directory of the
   current project. (As an example, if the module A.B.C is loaded from
   the file <some-path>/A/B/C.agda, then the root directory is
   <some-path>.)
 
 * It is an error if there are several files on the include path which
   match a given module name.
 
 * Interface files are relocatable. You can move around source trees as
   long as the include path is updated in a corresponding way. Note
   that a module M may be re-typechecked if its time stamp is strictly
   newer than that of the corresponding interface file (M.agdai).
 
 * Type-checking is no longer done when an up-to-date interface exists.
   (Previously the initial module was always type-checked.)
 
 * Syntax highlighting files for Emacs (.agda.el) are no longer used.
   The --emacs flag has been removed. (Syntax highlighting information
   is cached in the interface files.)
 
 * The Agate and Alonzo compilers have been retired. The options
   --agate, --alonzo and --malonzo have been removed.
 
 * The default directory for MAlonzo output is the project's root
   directory. The --malonzo-dir flag has been renamed to --compile-dir.
 
 * Emacs mode: C-c C-x C-d no longer resets the type checking state.
   C-c C-x C-r can be used for a more complete reset. C-c C-x C-s
   (which used to reload the syntax highlighting information) has been
   removed. C-c C-l can be used instead.
 
 * The Emacs mode used to define some "abbrevs", unless the user
   explicitly turned this feature off. The new default is /not/ to add
   any abbrevs. The old default can be obtained by customising
   agda2-mode-abbrevs-use-defaults (a customisation buffer can be
   obtained by typing M-x customize-group agda2 RET after an Agda file
   has been loaded).