[Agda] new generalize feature, first version

[Peter Divianszky]

 >>  >>      {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
 >>  >>
 >>  >> [...]
 >>  >>
 >>  >>      {x : ⊤} (p : tt ≡ x) → p ≡ p
 >>  >
 >>  > These two types are definitionally equal.
 >>
 >> Right, I just wanted to be precise with naming.
 >> The former is the current type signature and the latter is the desired
 >> one.
 >
 > There is no difference between these type signatures, even if you take
 > the names of implicit arguments into account. [...]

Ok, I saw how

     {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁

is equal to

     {x : ⊤} (p₁ : tt ≡ x) → p₁ ≡ p₁

but I missed that this is further equal to

     {x : ⊤} (p : tt ≡ x) → p ≡ p

because the second argument is not hidden.


 >> postulate
 >>    ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
 >>
 >> [...]
 > [...] and this is what you actually end up
 > with:
 >
 >    {Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
 >    {σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
 >    ((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
 >
 > The telescope contains /three/ implicit arguments all named Γ.

The naming of arguments is not yet fully implemented, only the ordering.

I just implemented another simplified naming which is stable too.
The result is:

     {σ.Γ σ.Δ δ.Γ ν.Γ : Con}
     {σ = σ₁ : Sub σ.Γ σ.Δ}
     {δ = δ₁ : Sub δ.Γ σ.Γ}
     {ν = ν₁ : Sub ν.Γ δ.Γ} →
         (σ₁ ∘ δ₁) ∘ ν₁ ≡ σ₁ ∘ (δ₁ ∘ ν₁)

if

     Sub : (Γ Δ : Con) → Set

otherwise, if

     Sub : Con → Con → Set

then it becomes

     {σ.1 σ.2 δ.1 ν.1 : Con}
     {σ = σ₁ : Sub σ.1 σ.2}
     {δ = δ₁ : Sub δ.1 σ.1}
     {ν = ν₁ : Sub ν.1 δ.1} →
         (σ₁ ∘ δ₁) ∘ ν₁ ≡ σ₁ ∘ (δ₁ ∘ ν₁)

 > I still don't quite understand why you get one occurrence of Σ but three
 > occurrences of Γ. Does it depend on arbitrary choices made by the
 > unifier?

It depends on the unifier, but not arbitrarily. Metavariables of 
generalized variables defined earlier wins.


 > Furthermore I'm not sure that it's a good idea to use names subject to
 > α-conversion (like Π-bound names) in a setting in which α-conversion is
 > not applicable (like in implicit Π binders).

I'm also not sure.
It is nice though that the naming of automatic implicit parameters can 
be influenced be existing syntactic constructs.


 > I tried to figure out what would happen if one of the bound names in the
 > type signature of Sub shadowed another name by parametrising the
 > module:
 >
 >    module _ {Σ : Set} where
 >
 > However, this triggered some kind of error:
 >
 >    meta var MetaId 48 was generalized
 >    CallStack (from HasCallStack):
 >      error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86
 > in [...]

This bug is fixed now.


On 2018-03-31 11:58, Nils Anders Danielsson wrote:
> On 2018-03-31 00:00, Peter Divianszky wrote:
>>  >>      {x = x₁ : ⊤} (p₁ : tt ≡ x₁) → p₁ ≡ p₁
>>  >>
>>  >> [...]
>>  >>
>>  >>      {x : ⊤} (p : tt ≡ x) → p ≡ p
>>  >
>>  > These two types are definitionally equal.
>>
>> Right, I just wanted to be precise with naming.
>> The former is the current type signature and the latter is the desired 
>> one.
> 
> There is no difference between these type signatures, even if you take
> the names of implicit arguments into account. Agda sometimes prints type
> signatures using the {x = y : A} notation in order to avoid issues
> related to shadowing. Here is one example:
> 
>    F : (Set → Set) → Set₁
>    F G = {A : Set} → G A
> 
>    T : Set₁
>    T = {A : Set} → F (λ X → A → X)
> 
> How should the normal form of T be printed? Agda prints
> 
>    {A : Set} {A = A₁ : Set} → A → A₁.
> 
> Note that this notation is not parsed by Agda.
> 
>>  > One property I did not bring up was that of stability. I hope that we
>>  > will not end up in a situation in which one can break lots of code by,
>>  > say, adding one variable name to a generalize block.
>>
>> My idea would be stable in this sense.
> 
> You presented the following example in your first message:
> 
>> For example,
>>
>> postulate
>>    ass : (σ ∘ δ) ∘ ν ≡ σ ∘ (δ ∘ ν)
>>
>> means
>>
>> postulate
>>    ass   : ∀{Γ Δ Σ Ω}{σ : Sub Σ Ω}{δ : Sub Δ Σ}{ν : Sub Γ Δ}
>>          → ((σ ∘ δ) ∘ ν) ≡ (σ ∘ (δ ∘ ν))
> 
> This suggested to me that if I replaced
> 
>    {Γ Δ Θ} : Con
> 
> with
> 
>    {Γ whatever Δ Θ} : Con,
> 
> then the type signature would change. However, I see now that your
> example uses the names Σ and Ω which are not listed in any generalize
> block. I tried your example myself, and this is what you actually end up
> with:
> 
>    {Γ = Γ₁ : Con} {Δ = Δ₁ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
>    {σ = σ₁ : Sub Γ₁ Δ₁} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
>    ((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
> 
> The telescope contains /three/ implicit arguments all named Γ.
> 
> (I'm not sure why the {x = y : A} notation is used for all the other
> implicit arguments. My guess would be that it has something to do with
> the implementation of generalize.)
> 
> If you perform the change that I mentioned above, then you still end up
> with the type signature above. Thus the type signature is stable under
> this particular kind of change.
> 
> After some experimentation I managed to figure out where the names in
> the type signature come from. If I replace
> 
>    Sub : (Γ Δ : Con) → Set
> 
> with
> 
>    Sub : (Γ Σ : Con) → Set,
> 
> then I get a different type signature:
> 
>    {Γ = Γ₁ : Con} {Σ : Con} {Γ = Γ₂ : Con} {Γ = Γ₃ : Con}
>    {σ = σ₁ : Sub Γ₁ Σ} {δ = δ₁ : Sub Γ₂ Γ₁} {ν = ν₁ : Sub Γ₃ Γ₂} →
>    ((σ₁ ∘ δ₁) ∘ ν₁) ≡ (σ₁ ∘ (δ₁ ∘ ν₁))
> 
> I still don't quite understand why you get one occurrence of Σ but three
> occurrences of Γ. Does it depend on arbitrary choices made by the
> unifier?
> 
> Furthermore I'm not sure that it's a good idea to use names subject to
> α-conversion (like Π-bound names) in a setting in which α-conversion is
> not applicable (like in implicit Π binders).
> 
> I tried to figure out what would happen if one of the bound names in the
> type signature of Sub shadowed another name by parametrising the
> module:
> 
>    module _ {Σ : Set} where
> 
> However, this triggered some kind of error:
> 
>    meta var MetaId 48 was generalized
>    CallStack (from HasCallStack):
>      error, called at src/full/Agda/TypeChecking/Rules/Term.hs:1580:86 
> in [...]
>