Add support for Setω+n

[jespercockx]

This PR adds internal syntax and typing rules for a second universe hierarchy Setω+n, which sits on top of Agda's regular universe hierarchy. Unlike Set i, this hierarchy is not polymorphic, so it is not possible to quantify over all Setω+n at once. This is my proposed answer to #4595 and fixes issues #2119, #4109, and #4585.

Note that there is no concrete syntax yet for Setω+n (except in error messages). I tried to add it in the same way as I did for Setω, but adding an infinite number of builtins is hard. Instead, it might be necessary to add hardcoded support for it in the parser, unless someone can think of a better solution.

[dylanede]

I'm just trying this out, and fixing #4109 in particular has made it much easier to do some reasoning about reflected terms in macros, so thanks for that! In particular I can now have a data structure

data _Reflects_ : {a : Level} {A : Set a} → Term → A → Setω where
  ...

to express that a reflected term corresponds to a particular real term, which then makes it easier to safely manipulate and analyse real terms according to their structure.

[dylanede]

Quick note:

When I try C-c C-c to case split on an instance of a data type in Setω, I get this error message:

Cannot split on datatype in sort Setω

Is that something that should be changed?

Edit: Actually, it won't let me pattern match at all on such a datatype. It's not just the editor integration. I guess that needs to be fixed to make data types in Setω useful.

[dylanede]

Would it just be a case of stopping it from triggering the error, in this code?

agda/src/full/Agda/TypeChecking/Rules/LHS.hs

Lines 1759 to 1773 in 1f17ae4

	checkSortOfSplitVar :: (MonadTCM m, MonadReduce m, MonadError TCErr m, ReadTCState m, MonadDebug m,
	LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
	=> DataOrRecord -> a -> Maybe ty -> m ()
	checkSortOfSplitVar dr a mtarget = do
	infOk <- optOmegaInOmega <$> pragmaOptions
	liftTCM (reduce $ getSort a) >>= \case
	Type{} -> return ()
	Prop{}
	| IsRecord <- dr -> return ()
	| Just target <- mtarget -> unlessM (isPropM target) splitOnPropError
	| otherwise -> splitOnPropError
	Inf{} | infOk -> return ()
	_ -> softTypeError =<< do
	liftTCM $ GenericDocError <$> sep
	[ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]

[jespercockx]

Would it just be a case of stopping it from triggering the error, in this code?

agda/src/full/Agda/TypeChecking/Rules/LHS.hs

Lines 1759 to 1773 in 1f17ae4

	checkSortOfSplitVar :: (MonadTCM m, MonadReduce m, MonadError TCErr m, ReadTCState m, MonadDebug m,
	LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
	=> DataOrRecord -> a -> Maybe ty -> m ()
	checkSortOfSplitVar dr a mtarget = do
	infOk <- optOmegaInOmega <$> pragmaOptions
	liftTCM (reduce $ getSort a) >>= \case
	Type{} -> return ()
	Prop{}
	| IsRecord <- dr -> return ()
	| Just target <- mtarget -> unlessM (isPropM target) splitOnPropError
	| otherwise -> splitOnPropError
	Inf{} | infOk -> return ()
	_ -> softTypeError =<< do
	liftTCM $ GenericDocError <$> sep
	[ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]

Indeed, that's it. I added a fix.

[jespercockx]

So I noticed that the printing of Setω+n is currently quite horribly broken. In particular, if you have an identifier in scope that's named Setω+1, then Agda will print the sort Setω+1 as Setω+2. The reason is that the printing currently uses a hack to print these sorts by printing them as a variable, but if another identifier with the same name is in scope then the shadowing machinery kicks in to rename the variable. Actually the same problem already appears for other built-in sorts piSort, funSort, and univSort. Maybe we should finally add a mechanism for binding built-in sorts so we can add all of these as proper builtins to Agda.Primitive.

[jespercockx]

I wonder if there would be some way to make Set_n and Prop_n into builtins as well, since this would allow renaming them when importing Agda.Primitive. Then perhaps every Agda file should start with an implicit open import Agda.Primitive using (Set; Prop) to preserve the current behaviour. The tricky part is to deal with the suffixes in Set0, Set1, Set2, etc. We would first need to implement a mechanism for parsing name variants.

[nad]

See #4093.

[andreasabel]

LGTM.
I do not grasp the change in its entirety, but we'll see it once people start using it.

For printing, we should consider using subscripts like for Set_1: Set\omega_1 etc.

[andreasabel]

Looks hackish.

[jespercockx]

I agree. I'm not sure why Inf is needed here in the first place, but I guess it is because there is no dedicated sort for non-fibrant types like the interval / face lattice of cubical. Maybe @Saizan can comment on this.

[Saizan]

Inf is the sort of tSub and a few other cubical primitives.

Indeed that's because it's outside the range of sorts indexed by a Level, which are the ones with composition, is that still the case after this PR?

[jespercockx]

It's still the case that Inf is outside of the range of sorts that are indexed by Level, but it is no longer disallowed to split on types in it. So it would probably be good to move the interval to its own sort if this PR is merged.

[pnlph]

I wonder if there would be some way to make Set_n and Prop_n into builtins as well, since this would allow renaming them when importing Agda.Primitive. Then perhaps every Agda file should start with an implicit open import Agda.Primitive using (Set; Prop) to preserve the current behaviour. The tricky part is to deal with the suffixes in Set0, Set1, Set2, etc. We would first need to implement a mechanism for parsing name variants.

Now Prop only works when the option --prop is enabled, right? (I was checking with 2.6.1), so maybe it is only necessary to use open import Agda.Primitive using (Set) if the current functionality is to be preserved.

But how will the user rename Setif it is already implicitly imported?

An alternative would be to change the current behaviour of the empty module and allowing the old behaviour with a new import command-line option maybe -- classic or something like that ;-) to activate the implicit import.

[Saizan]

Would it just be a case of stopping it from triggering the error, in this code?

agda/src/full/Agda/TypeChecking/Rules/LHS.hs

Lines 1759 to 1773 in 1f17ae4

	checkSortOfSplitVar :: (MonadTCM m, MonadReduce m, MonadError TCErr m, ReadTCState m, MonadDebug m,
	LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
	=> DataOrRecord -> a -> Maybe ty -> m ()
	checkSortOfSplitVar dr a mtarget = do
	infOk <- optOmegaInOmega <$> pragmaOptions
	liftTCM (reduce $ getSort a) >>= \case
	Type{} -> return ()
	Prop{}
	| IsRecord <- dr -> return ()
	| Just target <- mtarget -> unlessM (isPropM target) splitOnPropError
	| otherwise -> splitOnPropError
	Inf{} | infOk -> return ()
	_ -> softTypeError =<< do
	liftTCM $ GenericDocError <$> sep
	[ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]

Indeed, that's it. I added a fix.

Can you make sure it's still impossible to split on the Interval?

[jespercockx]

Can you make sure it's still impossible to split on the Interval?

The most robust way to do this would be to give the interval its own sort.

[jespercockx]

I rebased this PR on the current master after the fix of #4093, and added the concrete syntax Setωᵢ as suggested by Andreas. The main thing still blocking this from being merged is that it possibly makes Cubical Agda inconsistent (?), since it enables splitting on types in Setω, so in particular on the interval. The proper solution would be to have a separate universe of non-fibrant types (see #4091). An alternative would be to add a manual check to the LHS checker that prevents matching on the constructors of the interval directly.

[Saizan]

Actually the coverage checker is forbidding splitting on the interval in the isDatatype function, this was necessary to avoid problems with --omega-in-omega already.

[jespercockx]

Ok, I was already suspecting something like that because there were no failing tests. So I will go ahead and merge this then.

[gallais]

I am hyped. Thanks @jespercockx for this PR!