Panic on record declaration with unknown sort

[JasonGross]

On the code

module foo where
record bar : ? where

I get "Panic: uncaught pattern violation"

Seems distinct from #230 (is it related to #118 though?)

Agda version 2.6.2

[andreasabel]

Thanks for reporting, @JasonGross !

On 2.6.2.1, you will get yellow:

?0 : univSort _2
Sort _2  [ at ... ]

I thought I knew which issue this was, but now cannot find it... (Still, my stomach says it is a duplicate.)

[L-TChen]

The same code but with the option --without-K still fails on 2.6.2.1.

{-# OPTIONS --without-K #-}

record foo : {!!} where

[andreasabel]

Works in 2.6.1:

$ agda-2.6.1 Issue5681.agda
Checking Issue5681.
Failed to solve the following constraints:
  Has bigger sort: _2
Unsolved metas at the following locations:
  ...
Unsolved interaction metas at the following locations:
  ...

[andreasabel]

agda-bisect says: fee1fc7 is the first bad commit. Ping @nad.
Date: Fri Jun 4 10:55:31 2021 +0200
Fixed #5434.

[nad]

I don't know too much about this code. I tried to fix a bug, and @Saizan approved the changes, so I merged the fix.

[andreasabel]

@nad: If you do not accept responsibility, it is probably ok to revert the patch to fix the regression.
Or we could ignore the blocked and simply speculate either fibrant or non-fibrant for blocked sorts. For plain Agda, everything would be ok, but the experimental Cubical Agda might than malfunction if you leave the sort open with a meta-variable.

[nad]

I don't know too much about the "non-fibrant types" feature. Is this feature integral for something in Cubical Agda (like the interval type), or could it be hidden behind a flag and treated as experimental?

I also don't know exactly what infrastructure we have for postponing things. Could isFibrant postpone whatever is currently going on if it encounters an uninstantiated meta-variable, or is more work required?

[andreasabel]

Some postponed checks need to block unfolding of terms to avoid looping or ill-typed terms. I don't know the implications of isFibrant and whether some things need to be blocked until we know about fibrancy.

[nad]

@Saizan, can you answer some of the questions above?

[nad]

Discussion seems to be going on elsewhere (#5692).

[Saizan]

To summarize:

• we have non-fibrant types in --cubical/--erased-cubical, e.g. the Interval (also with just --two-level).
• we do not need to block things to postpone this check, we would just need to make it into a new constraint.

[andreasabel]

@Saizan: Do you think you can make a stab at this? Would be nice if this could be fixed for 2.6.2.2.