postulate
A : Set
x : A
f : (P : A → Set) → P x
g : (P : ((A → A) → A) → Set) → P (λ k → k x)
g P = f (λ x → P {! !})
Running C-c C-a in the hole results in:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Telescope.hs:688:24 in Agda-2.8.0-8OtZvJ9h6Mn4rrWgQM63zA:Agda.TypeChecking.Telescope
which is at:
piApplyM = piApplyM' __IMPOSSIBLE__called from:
bodyType <- bench [Bench.Reduce] $ reduce =<< piApplyM goalType' (Var 0 []) -- TODO: Good place to reduce?There's no internal error if P : ((A → A) → A) → Set is a postulate instead of a parameter.
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