Skip to content

Commit bb5f086

Browse files
zeroeightysixjespercockx
authored andcommitted
Add a fail test for issue #437
1 parent 9fe431d commit bb5f086

File tree

3 files changed

+8
-0
lines changed

3 files changed

+8
-0
lines changed

test/AllFailTests.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ import Fail.NonCanonicalSuperclass
4040
import Fail.Issue125
4141
import Fail.Issue357a
4242
import Fail.Issue357b
43+
import Fail.Issue437
4344
import Fail.DerivingParseFailure
4445
import Fail.Issue306a
4546
import Fail.Issue306b

test/Fail/Issue437.agda

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module Fail.Issue437 where
2+
3+
data Indexed : (a : Set) Set₁ where
4+
MkIndexed : { a : Set } Indexed a
5+
{-# COMPILE AGDA2HS Indexed #-}

test/golden/Issue437.err

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
test/Fail/Issue437.agda:3.6-13: error: [CustomBackendError]
2+
agda2hs: Not supported: indexed datatypes

0 commit comments

Comments
 (0)