Showing content from https://github.com/agda/agda/issues/7413 below:
reproducer for error "The type is non-fibrant or its sort depends on an interval variable" · Issue #7413 · agda/agda · GitHub
_ -> typeError . GenericError . show =<< (text "The type is non-fibrant or its sort depends on an interval variable" <+> prettyTCM (unAbs b)) -- TODO better Type Error
@plt-amy
: Do you think you could cook up a test case that triggers this error?
It has to be something with
with
because the function
telePiPath
is called from
withFunctionType
only:
withFunctionType delta1 vtys delta2 b bndry = addContext delta1 $ do reportSLn "tc.with.abstract" 20 $ "preparing for with-abstraction" -- Normalize and η-contract the type @b@ of the rhs and the types @delta2@ -- of the pattern variables not mentioned in @vs : as@. let dbg n s x = reportSDoc "tc.with.abstract" n $ nest 2 $ text (s ++ " =") <+> prettyTCM x d2b <- telePiPath_ delta2 b bndry
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