[✓] The issue can be reproduced with the latest version of Agda (either released or master branch).
Note: We do not fix issues in older versions of Agda.
[✓] I have supplied all information so the bug can be easily reproduced (in particular, the reproducer is a complete Agda file).
> agda --version
Agda version 2.6.3
> nixos-version
22.11.20230219.0cf4274 (Raccoon)
id : ∀ {A : Set} -> (A -> A)
id = λ{ a -> a }
syntax id = ι
record Arr* A1 A2 (B1 : A1 -> Set) (B2 : A2 -> Set) (f : A1 -> A2) : Set where
field run : ∀ (a : A1) -> B1 a -> B2 (f a)
id* : ∀ {A : Set} {B : A -> Set} -> Arr* A A B B ι
id* = record
{ run = λ{ a b -> b }
}
> agda ~/Repro.agda
Checking Repro (/home/<user>/Repro.agda).
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs:3095:30 in Agda-2.6.3-IodRPUWhXmb829dMFrGuRz:Agda.Syntax
.Translation.ConcreteToAbstract
The trouble is the ι (rather than id) at the end of the type signature in id*.
(It's probably possible to distill further.)
(Yes I'm aware that syntax id = ι is something of an abuse of the syntax declaration feature. In my defense, I'm later going to define compose and compose* which want mixfix operators, and then a one-step-more-complicated version where the associated syntax would have to take dependent arguments out-of-order, and I won't be able to use mixfix operators in that case1, so I must use syntax in my most-complicated version of compose, and I decided to try using syntax instead of mixfix everywhere for symmetry, and ran into this issue.)
Reporting as requested.
kinda like how the syntax a <[ P ] b can't possibly route through a mixfix operator _<[_]_ : Carrier P -> (P : Preorder) -> Carrier P -> 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