TODO

Features
--------

* remembering the last thing in scope when computation gets stuck

* debug information

* Use substitutions for meta dependencies (at least for printing).  We'll need
  to remember the number (or names?) of dependency args. How to show that a
  meta variable cannot depend on a particular variable?

* lazy evaluation (or call by value?)

* unify primitive and {-# BUILTIN #-}

* allow module instantiation before top-level module(?)

* abstract open (need to re-type check to make sure the abstraction is solid)

* extend positivity check to handle function calls

* mutual modules

* more liberal builtin bindings (Nat as a special case of a general sequence)

User interface
--------------

* Highlighting fixity declarations and all module names.

* Point warping for record fields.

* locally nameless representation

Fixes
-----

[Errors]

* DeclarationException when missing a type signature

[Parsing]

* allow more things in postulates (infix, private, ..)

* allow fixity declarations for record fields (where?)

* allow postulates in mutual

* Check out lex/parse errors (what position and what input is reported).

* Enable parsing of non-trivial literate files (see
  examples/syntax/highlighting/Test.lagda).

[Serialisation]

[Printing]

* print patterns in mixfix notation (AbstractToConcrete)

* meta variables are printed with their lambda lifted types

[Scope]

* check that fixity declarations correspond to actual definitions

* change syntax for fixity declarations (infix is a bit strange for prefix and
  postfix operators)

[Evaluation]

* literal patterns are considered neutral when deciding if a match is No or DontKnow
  example

    funny : (A : Set) -> A -> D A -> ..
    funny .Nat zero nat
    funny .String "foo" string

    Here
      funny String "foo" string
    doesn't reduce because we DontKnow that "foo" doesn't match zero.

[Type checking]

* implicit function spaces and records interact badly with meta variables
  solution: postpone type checking problems
    - postpone checking of lambda against blocked types
    - postpone checking of applications where the function has a blocked type
    - postpone checking of records against blocked types

[Testing]

* write better tests

[Bugs]

* The Emacs interface meta variable treatment leads to problems with
  the syntax highlighting/point warping. Fix this by doing most work
  on the Haskell side, using the syntax tree, instead of mucking
  around with regular expressions on the Emacs side.

  Currently there are two known bugs:
  1) _All_ question marks are treated as meta variables.
  2) After a question mark has been converted into {! !} the point
     warping does not work (the offsets into the file have changed).

* importing A after importing A.B causes a clash

* Too many open files

* Evaluation of _==_ loops on something like this:

    open module Eq = Equivalence (Eq'{ℂ}{A}{B}) renaming (_==_ to _=='_)
    f == g = .. ==' ..

* There's a bug in the import chasing where a module can be imported before
  it's type checked. I.e. an old version of the module is stored in an
  interface file of a different module and we can't see that it's not
  up-do-date.

  I think this is what happens in the polydep example if everything is
  up-to-date except TYPE.agda.

[Interaction]

[Errors]

* Remember/figure out range of previous binding in DuplicateBuiltinBinding.

* wrong "When..." reported for f (g x) if g x is well-typed but of wrong type.

* ranges of constructors in patterns are wrong. (also in right-hand sides?)

* give sensible message for too few arguments to constructor in pattern

[Type checking]

* When do we have to turn on abstractMode. When checking anything public? Not
  done at the moment.

[Imports]

* handle clashing builtin things

* create interface for top-level module (not so important)

* allow the source to not exist if there is an interface file
  (what if it needs rebuilding? throw error)

[Builtin]

* check that bindings to list and bool binds to datatypes of the right shape

[Misc]

* Allow qualified names in BUILTIN pragma. Currently pragmas are parsed as
  plain strings, so a qualified name is interpreted as an unqualified name
  containing a dot.

* check that the module name matches the file name. Also when importing the
  module name should be the one we're trying to import.

* Allow modules to be called things like Prop and Set (?)

* Move large parts of the Makefiles to mk/rules.mk (or something)

Speculative
-----------

* make scope checking aware of abstract? or maybe this is too much work

Cleaning
--------

* TypeChecking.Reduce

  - Explicit dictionaries (Kit)? see notes/kit

* Split vim highlighting into a general highlighting module and the vim
  specific parts.

Performance
-----------

* Check what's taking time with new meta var/constraint handling

* a lot of memory created by subst is never used

* space leak in lexer (positions too lazy?)

Done
----

* pattern coverage

* with-clauses

* better algorithm for pattern matching on inductive families

* structured verbosity

* records

* implemented the CHIT-CHAT module system

* polymorphic constructors at run-time (at least at conversion checking)

* Split TypeChecking.Errors into TypeChecking.Pretty and TypeChecking.Errors

* inductive families with pattern matching

* build agda as a package to speed up loading into ghci

* OpenTerm type to simplify deBruijn variable handling

* Monad transformer for checking patterns.

* pretty printing of operator applications

* named implicit arguments, see notes/named-implicit

* Use Data.ByteString (if ghc-6.6) for interface parsing (faster, but still quite slow)

* optimized natural numbers, user view is still zero/suc.

* allow reexporting of things using 'open Foo, public'

* allow import and open before the top level module.

* checking that underscores have been solved (only in batch mode)

* syntax highlighting

* proper make test (agda now exits with failure on error)

* failing test (like in agdaLight)

* throwing not-in-scope error rather than no parse for application wheneven possible

* use interface files in scope checking

* check for cyclic imports (we need to use interface files when scope checking)

* removed list sugar (and made [ and ] valid in names)

* create interface files when importing

* allowing lambda-bound operators by always writing _+_ (hence making underscore
  in names carry semantics).

* allow no type signatures for definitions of the form x = e

* mix-fix operators

* list sugar

* handle absurd patterns

* literal patterns

* literals

* built-in things

* pragmas

* move trace to environment

* name suggestions in telescopes

* forall x y z -> A  =  (x:_)(y:_)(z:_) -> A

* cleaning up of TypeChecking.Monad.*

* Context to abstract thinks that the types are valid in the entire context.

* Hiding info on lambdas.

* flag for printing all implicit arguments (handled in internal to abstract)

* proof irrelevance

* Prop <= Set

* sort checking of datatypes check that all constructor arguments fit inside
  the datatype sort (rather than checking that the types of the constructor fit)

* let-bindings (only x = e definitions)

* insertion of hidden lambdas when appropriate

* optimise

* for an as-pattern x@p x should reduce to p during type checking

* as-patterns

* split TypeChecking.Monad.Context

* better names for implicit args in lhs

* replace explicit Hidden with Arg in Pi and App (and more?)

* independent functions in Type

* local functions

* speed up normalise

* getopts

* When instantiating a module we should generate functions for the axioms and
  constructors and probably for everything else as well (reducing to the
  instantiated versions from the instantiated module). Together with
  monomorphic constructors.

* Monomorphic constructors.

* ? should not be a valid operator characted

* actually check sorts

* Get rid of distinction between hole and underscore. Instead keep a separate
  list of which metas are interaction points.

* Blocked constructor in Terms and Types

* insert hidden arguments in lhss

* ranges in error messages

* abstract info on constraints (TCEnv instead of Context) and interaction meta
  vars.

 vim: sts=2 sw=2 ts=80