[Agda] new generalize feature, first version

[Peter Divianszky]

Dear Agda users and implementors,

I implemented a first version of forall-generalization, and I would like 
to get feedback on it.


For users
---------

An example Agda file can be found at
https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda

Suppose that the following Set formers were postulated:

postulate
   Con :                       Set
   Ty  : (Γ : Con) →           Set
   Sub : (Γ Δ : Con) →         Set
   Tm  : (Γ : Con)(A : Ty Γ) → Set

There is a new keyword 'generalize', which accept declarations like 
'field' for records:

generalize
   {Γ Δ Θ} : Con
   {A B C} : Ty _
   {σ δ ν} : Sub _ _
   {t u v} : Tm _ _

After these 12 declarations

(1) Γ, Δ and Θ behave as Con-typed terms, but they are automatically 
forall-generalized, so, for example

postulate
   id  : Sub Γ Γ
   _∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ

means

postulate
   id  : ∀ {Γ} → Sub Γ Γ
   _∘_ : ∀ {Γ Δ Θ} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ

(2) A, B and C behaves as (Ty _)-typed terms (their types contain a 
dedicated metavariable for each of them),
and they are also automatically forall-generalized.
For example,

postulate
   _▹_ : ∀ Γ → Ty Γ → Con
   π₁ : Sub Γ (Δ ▹ A) → Sub Γ Δ

means
   _▹_ : ∀ Γ → Ty Γ → Con
   π₁ : ∀{Γ Δ}{A : Ty Δ} → Sub Γ (Δ ▹ A) → Sub Γ Δ

(3) The metavariables of generalizable variables are also automatically 
generalized.
For example,

postulate
   ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)

means

postulate
   ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
         → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))

(4) The place and order of generalized variables are fixed by the 
following rules:

A) generalized bindings are placed at the front of the type signature
B) the dependencies between the generalized variables are always respected
C) whenever possible, introduce A before B if A < B
- for non-metas, A < B if A was declared before B with a 'generalize' 
keyword
- a meta is smaller than a non-meta
- for metas, A < B if A was declared before B with a 'generalize' 
keyword. For example, σ : Sub _1 _2 was declared before δ : Sub _3 _4 so
instances of _1, _2, _3, _4 are ordered according to the indices.

----

The design goals were the following:

- make type signatures shorter
   - the type schema of generalizable variables helps
     to make even more guesses by the type system
- avoid accidental generalization
   - only the given names are generalized
   - the type of generalizable variables are checked
     against the given schema, which adds extra safety
- make generalized type signatures reliable
   (the ordering, and also the naming, see later)

Question:

- What should be the keyword?
   'notation' seems also good for me.
   The idea behind 'notation' is that this language construct
   makes informal sentences like "Let Γ Δ Θ denote contexts." formal.

Plans (not implemented yet)

- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules and between record fields
- make generalizable variables importable?
- Name the generalized metavariables also according by the given 
generalizable variables. For example, if _1 : Con, then take the first 
freely available <Name> : Con, where <Name> was defined by 'generalize'. 
If no more names are available, stop with an error message.

You can try the current implementation with my fork:
https://github.com/divipp/agda


For Agda implementors
---------------------

The main patch is

https://github.com/divipp/agda/commit/d172d1ade15abe26be19311300f7d640563a6a57

It contains several hacks, I'm not sure that this is the right thing to do:
- metavariables of generalizable variables are solved locally during 
typechecking of terms and reverted later
- generalizable variables are stored in the signature as if they were 
introduced by 'postulate'

The Generalize.agda file succeeds when I load it into emacs, but fails 
if I call Agda directly. Somehow I could not filter out metavariables 
introduced by 'generalize', so Agda tries to serialize them.

It would great if you could help me to let this feature in.


Best Regards,

Peter