{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
postulate
coe : {A B : Set} → A → B
coe-id : {A : Set} {a : A} → coe a ≡ a
{-# REWRITE coe-id #-}
record Fam : Set₁ where
field
S : Set
P : S → Set
module _ (F : Fam) where
open Fam F
postulate
R : (T : Set) → (T → Set) → Set
r : (Q : ((s : S) → P s) → Set) → R (Σ S P) (λ t → Q (λ _ → coe (t .snd)))
r' : (Q : ((s : S) → P s) → Set) → R (Σ S P) (λ t → Q (λ _ → coe (t .snd)))
-- r' Q = r Q -- works
r' Q = r _ -- internal error
Type checking this (with -v impossible:10) results in:
de Bruijn index out of scope: 3 in context [t, Q, F]
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Monad/Context.hs:498:9 in Agda-2.8.0-1QHovOf0r0W5y0ByuxgAwH:Agda.TypeChecking.Monad.Context
The error disappears if the module parameter (F : Fam) is replaced with (S : Set) (P : S → 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