[ fix #4093 ] Bye bye Set

[jespercockx]

This PR implements my proposed solution for #4093. It consists of the following changes:

• Set and Prop are removed as keywords, as are Set0, Set1, Prop0, ... and their unicode variants.
• Agda.Primitive now declares two new builtins {-# BUILTIN SET Set #-} and {-# BUILTIN PROP Prop #-}, which can be renamed when importing this module.
• All modules automatically start with an implicit statement open import Agda.Primitive using (Set; Prop), unless the flag --no-auto-import-primitive is used.
• The scope checker has been extended to recognize suffixed versions of whatever names are bound to the builtins SET and PROP, so for example Type0, Type1, ... are now accepted when Set has been renamed to Type.
• The pretty-printer will also use the builtin names of SET and PROP, so the renamed versions are used in error messages and interactive commands.

If there is a consensus that this is a good design, I will add a changelog entry, some documentation, and a test case before merging.

[nad]

What happens if you rename Set to, say, _X_X_?

[jespercockx]

This file is accepted:

{-# OPTIONS --no-auto-import-primitive #-}

open import Agda.Primitive renaming (Set to _X_X_)

test : _X_X₁_
test = _X_X_

[guillaumebrunerie]

What if you rename Set to Set and Prop to Set₁? 😃

[jespercockx]

{-# OPTIONS --no-auto-import-primitive --prop #-}

open import Agda.Primitive renaming (Set to Set; Prop to Set₁)

test : Set₁
test = Set

gives

Set₁ != Set₁
when checking that the expression Set has type Set₁

:(

[guillaumebrunerie]

Oh, sorry…
But, apart from that, I think that turning Set and Prop into pragmas that can be renamed is a great idea, thank you for making it possible!

[MatthewDaggitt]

So next on the list is the ability to rename the record and data keywords right? Followed shortly by where and module... Then no Agda code will ever be able to be taken at face value 😄

[jespercockx]

So next on the list is the ability to rename the record and data keywords right? Followed shortly by where and module... Then no Agda code will ever be able to be taken at face value smile

Agda won't truly be configurable until we make it possible to rename : and -> :P

[guillaumebrunerie]

So next on the list is the ability to rename the record and data keywords right? Followed shortly by where and module... Then no Agda code will ever be able to be taken at face value smile

Agda won't truly be configurable until we make it possible to rename : and -> :P

Yes! It should be possible to rename : to the Unicode colon, so that we can finally use a regular colon in syntax declarations!

[nad]

What about the following code?

{-# OPTIONS --no-auto-import-primitive #-}

open import Agda.Primitive using (Prop)

postulate
  Set₁ : Prop

open import Agda.Primitive using (Set)

postulate
  A : Set₁

[jespercockx]

What about the following code?

{-# OPTIONS --no-auto-import-primitive #-}

open import Agda.Primitive using (Prop)

postulate
  Set₁ : Prop

open import Agda.Primitive using (Set)

postulate
  A : Set₁

The code is accepted if you add the --prop flag. The disambiguation favors the postulated Set₁ over the suffixed version of the imported Set. Perhaps there should be a warning for this situation.

[andreasabel]

Perhaps there should be a warning for this situation.

Yes, we should have a bit of insurance against such obfuscation.

If there is a consensus that this is a good design,

In the spirit of looking forward, I suggest to rename the SET builtin to TYPE.

{-# BUILTIN TYPE Set #-}

[nad]

In the spirit of looking forward, I suggest to rename the SET builtin to TYPE.

{-# BUILTIN TYPE Set #-}

I agree.

[pnlph]

I was leaving this comment without seeing this discussion.

Could not be the default behaviour without implicit import and {-# OPTIONS --auto-import-primitive #-} to get the old behaviour? It is a bit strange having Set in scope in an empty module without options...

[jespercockx]

Could not be the default behaviour without implicit import and {-# OPTIONS --auto-import-primitive #-} to get the old behaviour? It is a bit strange having Set in scope in an empty module without options...

But currently Set is a keyword so it is always considered in scope. Not adding the implicit import would meant all old Agda files that mention Set would break, which is not something we'd want to do.

[pnlph]

Sorry, I did not think about backward compatibility. Of course Set is practically everywhere... 🤦

In that case, I would upvote this comment from Andreas, --bare would be a short and descriptive new option.

Otherwise, would not be better --no-auto-import-set than --no-auto-import-primitive? Because the implicit import is only affecting Set, not the rest of the primitives like Level, Setω... Is that correct?

[jespercockx]

Sorry, I did not think about backward compatibility. Of course Set is practically everywhere... facepalm

In that case, I would upvote this comment from Andreas, --bare would be a short and descriptive new option.

Otherwise, would not be better --no-auto-import-set than --no-auto-import-primitive? Because the implicit import is only affecting Set, not the rest of the primitives like Level, Setω... Is that correct?

It affects Set and Prop.

[laMudri]

Maybe, aiming for forward compatibility, the --no-auto-import-primitive flag should be more specific. We might in the future have code that uses --no-auto-import-primitive in order to rename Set, but then we use this mechanism to allow renaming of something else. Then code not using --no-auto-import-primitive inherits the shim, whereas code using it doesn't. Or, we might have to remember that --no-auto-import-primitive is just for Prop and Set, and introduce a more specific name for the flag for the other thing we end up renaming.

I would suggest having modules Agda.Primitive.Set and Agda.Primitive.Prop, and then options --no-import-set and --no-import-prop, or something like that.

[jespercockx]

I've updated the PR with better handling of cases with ambiguous names, e.g.

{-# OPTIONS --no-auto-import-primitive --prop #-}

open import Agda.Primitive renaming (Set to Set; Prop to Set₁)

test : Set₁
test = Set

now gives

Ambiguous name Set₁. It could refer to any one of
  Set bound at AmbiguousSet1.agda:3,45-48
  Set₁ bound at
    AmbiguousSet1.agda:3,58-62

and

{-# OPTIONS --no-auto-import-primitive #-}

open import Agda.Primitive using (Prop)

postulate
  Set₁ : Prop

open import Agda.Primitive using (Set)

postulate
  A : Set₁

gives

Ambiguous name Set₁. It could refer to any one of
  Set bound at
    agda-default-include-path/Agda/Primitive.agda:13,18-21
  Set₁ bound at AmbiguousSet1b.agda:6,3-7

I also renamed the SET builtin to TYPE, and I've added entries to the changelog and user manual.

Finally, I renamed the --no-auto-import-primitive flag to --no-import-sorts, I hope this strikes a decent balance between brevity and clarity.

[jespercockx]

This can be merged once the CI passes.

[jespercockx]

My rebase messed things up, plz send help

[jespercockx]

That looks better, let's hope CI passes this time.

[andreasabel]

This might have connections to #5706.