[Agda] new generalize feature, first version

[Martin Stone Davis]

Peter, many accolades to you for developing and sharing. Now for the 
complaints!

My trouble is shown in the code below, which is failing on the last 
line. Is this a bug in the new feature?

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

postulate
   Class : Set -> Set
   method : {X : Set} {{_ : Class X}} -> X -> Set
   Nat : Set
   Fin : Nat -> Set

generalize
   {n} : Nat
   {x} : Fin _

postulate
   instance ClassFin : Class (Fin n)
   works1 : {x : Fin n} -> method x
   works2 : method {{ClassFin}} x
   works3 : method {X = Fin n} x
   fails  : method x
{-
Unsolved meta not generalized
when checking that the expression method x has type Set _22
-}
```

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