Freeze metas in module telescope after checking the module?

[GoogleCodeExporter]

This is on  Development Agda of February 6, 2014.
For

------------------------------------------------------------------
module _ {α α= β} {A : Setoid α α=}
  where
  open Setoid A 
  open IsEquivalence isEquivalence using (sym)

  negatedRespects : (P : Carrier → Set β) → P Respects _≈_ →
                                                         (¬_ ∘ P) Respects _≈_
  negatedRespects P P-resps x=y ¬Px =  ¬Px ∘ P-resps (sym x=y)
------------------------------------------------------------------

the checker does not solve about  β. 
Must it?

Moving  β  from `module' to the signature of  negatedRespects  does make it 
type-checked.
But the first version looks better.

Original issue reported on code.google.com by mech...@botik.ru on 18 Feb 2014 at 12:27

[GoogleCodeExporter]

You can write {α α= β : Level} or even {α α= β : _} to circumvent that 
problem.

As the type of β cannot be infered from the module parameter telescope, it is 
"frozen".  

The question is whether this is the right behavior, or whether the metas of the 
module telescope should be frozen only after checking the whole module.  

Opinion, Ulf?

Original comment by andreas....@gmail.com on 18 Feb 2014 at 4:28

• Changed state: InfoNeeded
• Added labels: Meta, Modules

[GoogleCodeExporter]

I have guessed about `: Level' only after I posted the item.
I am sorry for noise.

Original comment by mech...@botik.ru on 18 Feb 2014 at 5:27

[GoogleCodeExporter]

Since we're freezing metas from the definitions in the module it feels a bit 
weird to leave the module telescope metas open. I'd lean towards the current 
behaviour.

Original comment by ulf.nor...@gmail.com on 18 Feb 2014 at 6:00

[GoogleCodeExporter]

One could argue that

  module _ mtel where
    f : A
    f ps = t

should behave like

  f : mtel -> A
  f mtel ps = t

which would suggest to not freeze the metas of mtel before checking f.

Original comment by andreas....@gmail.com on 22 Feb 2014 at 2:21

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 3 Mar 2014 at 9:41

• Changed title: Freeze metas in module telescope after checking the module?
• Added labels: Priority-Low, Type-Enhancement

[UlfNorell]

The current situation is actually that we freeze metas after the first declaration in the module:

module _ where

module M (A : _) where

  y = Set -- type of A is solved if this is removed

  x : Set
  x = A

This is not a sensible behaviour. Two options:

• (easy) freeze metas after checking the module parameters
• (hard) leave module parameter metas unfrozen

The latter solution would require refactoring the way we freeze metas. At the moment we freeze all metas when freezing, but in this case we'd need to freeze metas from the declarations inside the module, but leave the parameter metas unfrozen. This might also lead to some unpredictable behaviour when there are dependencies between parameter metas and local metas.

I'd lean towards the easy solution.

[jespercockx]

I also vote for freezing metas from the module parameters right away. The alternative just seems to unpredictable/brittle.

[andreasabel]

I vote for a more fine-grained freezing. Modules should behave similarly to the corresponding record types, which can have metas in their telescope which are resolved by the fields and definitions in the record.

[UlfNorell]

How do you propose to deal with the unpredictability/brittleness concerns in this case? Or are you saying we shouldn't freeze any metas inside modules (not even the top-level module?)? This is, I believe, how record types work at the moment.

[jespercockx]

Actually @divipp already implemented the second alternative in 32220e0#diff-74c7bcc666176816c0d565cbaf6ef7c1R181 (without advertising it). So this issue has been fixed for 7 months already. I now feel stupid for wasting my Sunday on implementing the alternative solution, but I'm also happy I don't have to implement it myself.

[nad]

(without advertising it).

I suggest that we document the change. When are module parameter metas frozen?

[jespercockx]

Modules are treated the same as other declarations in this respect, so any metas created while checking a module telescope are frozen at the end of that module. I'll add something to the changelog.