search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Allow unsolved metas in imported files #964

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From guillaum...@gmail.com on November 15, 2013 15:54:34

File A.agda

module A where

B : Set1 B = Set

C : Set C = ?

File B.agda

open import A

module B where

D : Set1 D = B

In the previous situation, when loading the file B.agda in emacs, the Agda mode complains about unsolved metas in A.agda, which is a bit annoying because C is not even used in B.agda. I think Agda should allow importing files containing unsolved metas (as long as they are not used elsewhere).

Original issue: http://code.google.com/p/agda/issues/detail?id=964

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 15, 2013 11:25:40

I support this idea. A module with {-# OPTIONS --allow-unsolved-metas #-} and unsolved metas should be serialized.

However, serializing unsolved metas as such seems problematic. (Maybe they could be deserialized as frozen metas with new numbers, but still that would not be faithful with the current implementation. They would have to be deep-frosted (in permafrost soil, never to be unfrozen)).

When serializing a file with unsolved metas, these metas could be turned into postulates. They would not have to be inserted at the position where they make sense in terms of scope (so I think), since just the signature-soup is serialized. And they should definitely not be in scope at point of unserialization (i.e., in the module that imports them).

Labels: Type-Enhancement Priority-Medium Meta Interface

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 15, 2013 23:46:38

An alternative, which might be easier to implement is to not serialise modules with unsolved metas, but still allow them to be imported. That way they would be re-type checked every time you load the file, but it would mean they would behave as proper metas (e.g. they'd show up as unsolved in the emacs mode). That has the advantage that you won't forget about unsolved metas deep down in your project.

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 16, 2013 00:44:40

Ah, I somehow was assuming serialization was a prerequisite for import, which isn't. Serialization may give you the benefit of introducing sharing, but maybe that is second-rank for this issue.

If your suggestion is easier to implement (maybe quite easy?), we should of course start with this.

NB: The other thing (turning metas into postulates) could be solved by my rejected proposal to have a built-in

"postulated"

which has any type. The proposal was rejected since there is an easy implementation

postulate postulated : {a : Level}{A : Set a} -> A

which is an atomic bomb when using instance search or auto. Maybe I should reopen [can't find it](and implement) my proposal since I still think it is a good idea.