[Agda] new generalize feature, first version

[Nils Anders Danielsson]

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 [...]

-- 
/NAD