An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Monad/MetaVars.hs:227:24 in Agda-2.6.5-11d9e77a2f3bb91e7e0dc786e2d0ff9d4d66bc0a0c5556df1c60e6ba71185648:Agda.TypeChecking.Monad.MetaVars
Minimized reproducer has two components:
{-# OPTIONS --safe #-}
module Setup where
open import Agda.Primitive public
open import Agda.Builtin.Equality public
open import Agda.Builtin.Sigma public
record Underlying {ℓ} (T : Set ℓ) : Setω where
field
ℓ-underlying : Level
⌞_⌟⁰ : T → Set ℓ-underlying
open Underlying ⦃ ... ⦄ public
private variable
ℓ ℓ′ : Level
A : Set ℓ
B : Set ℓ′
infixr 6 Σ-syntax-und
Σ-syntax-und
: ⦃ _ : Underlying A ⦄
(X : A) (F : ⌞ X ⌟⁰ → Set ℓ′)
→ Set _
Σ-syntax-und X F = Σ ⌞ X ⌟⁰ F
syntax Σ-syntax-und X (λ x → F) = Σ[ x ꞉ X ] F -- -- MODIFIER LETTER COLON, codepoint 42889
instance
Underlying-Type : ∀{ℓ} → Underlying (Set ℓ)
Underlying-Type {ℓ} .ℓ-underlying = ℓ
Underlying-Type .⌞_⌟⁰ x = x
foo : (f : A → B) → Set _
foo {A = A} {B = B} _ = A → B -- must be a function type
-- manually inlining `foo` definition makes the bug disappear
_↝_ : Set ℓ → Set ℓ′ → Set _
A ↝ B = Σ[ f ꞉ (A → B) ] foo f -- must use new syntax to trigger the bug
{-# OPTIONS --safe #-}
module Boom where
open import Setup
Bar : (ℓ : Level) → Set ℓ → Set _
Bar ℓ T = Σ (Set ℓ) λ X → X ↝ T
funny : ∀{ℓ} {T : Set ℓ} (U : Bar ℓ T) → Set ℓ
funny {ℓ} {T = T} (X , f , f-emb) =
let -- boom : Σ (Σ (Set ℓ) λ X′ → (X′ → T)) λ Z → foo f
-- ^ ascribing type makes the bug disappear
boom = ((X , f) , f-emb)
in {!!}
Agda version: master (1c8360d)
The bug is introduced in 2f09379
user@computer:~/Projects/agda$ git bisect good$
2f09379734a5a7ed080032866901c5436d67df03 is the first bad commit$
commit 2f09379734a5a7ed080032866901c5436d67df03$
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