The following code reproduces the bug. The type of test doesn't matter, as long as it's not something immediately constructed by auto. Putting -l into the hole ensures that even in trivial cases the bug is encountered.
open import Agda.Builtin.Sigma using (Σ)
case_of_ : {A B : Set} → A → (A → B) → B
case e of f = f e
test : _
test = {! !}
where
c = case_of_
f = Σ.fst
Error message when trying to run auto on the hole:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at
src/full/Agda/TypeChecking/Telescope.hs:681:24 in
Agda-2.8.0-d11b19132dc042adfc7480ee2dfeb3253bcd55191d852d3b017067bf19d6bcde:Agda.TypeChecking.Telescope
I'm using ghc-9.4.8 and Agda built from master branch (commit e3656c4).
P.S. (Andreas): exception is thrown here:
class PiApplyM a where piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type piApplyM = piApplyM' __IMPOSSIBLE__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