The following code results in an internal error:
{-# OPTIONS --cubical #-}
open import Agda.Builtin.Cubical.Path
p : Set ≡ Set
p i with _
... | _ = Set
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Telescope/Path.hs:71:14 in Agda-2.8.0-2UHLkJpHripCLhmKYbjPID:Agda.TypeChecking.Telescope.Path
which is located at:
_ -> __IMPOSSIBLE__ -- 2024-10-07 Andreas, issue #7413 -- Andrea writes in https://github.com/agda/agda/issues/7413#issuecomment-2396146135 -- -- I believe this is actually impossible at the moment -- unless generalized Path types were implemented while I wasn't looking: -- -- telePathPi only does this check if there's a boundary, -- which should only be introduced by a PathP copattern, -- which then should ensure the result type is in Type lvl -- for some lvl that does not depend on on the interval -- variable of the path. -- -- WAS: generic error with message -- text "The type is non-fibrant or its sort depends on an interval variable" <+> prettyTCM (unAbs b)with a comment referencing
#7413.
#7539changed it from a
GenericError
to an
__IMPOSSIBLE__
.
So the code above was a reproducer for the error in the issue, since 2.7.0.1 used to throw:
The type is non-fibrant or its sort depends on an interval variable
_4 (i = i) → Set₁
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4