[Agda] new generalize feature, first version

[Martin Stone Davis]

Respect the privacy of --generalize'd identifiers!

```
{-# OPTIONS --generalize #-}

postulate
   Nat : Set
   Fin : Nat → Set

module _ where

   private
     generalize
       n : Nat
   {-
     Using private here has no effect. Private applies only to
     declarations that introduce new identifiers into the module, like
     type signatures and data, record, and module declarations.
     when scope checking the declaration
       module _ where
   -}

   postulate foo : Fin n

postulate n : Nat
{-
Multiple definitions of n. Previous definition at
[snip]
when scope checking the declaration
   n : Nat
-}
```


On 03/29/2018 05:13 AM, Peter Divianszky wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda