@@ -0,0 +1,24 @@
1+-- This regtest tests for incorrect erasure from underapplied data constructors.
2+
3+data T : Type where
4+ C : Nat -> Nat -> Nat -> T
5+
6+data Q : Type where
7+ D : (Nat -> T) -> Q
8+
9+-- The bug was here: (C 3 4) would compile to plain data,
10+-- not to a function that would expect another (albeit erased) argument.
11+f : Q
12+f = D (C 3 4)
13+
14+proj : Nat -> Q -> Nat -> T
15+proj Z (D f) = f
16+proj (S n) q = proj n q
17+
18+g : T -> Nat
19+g (C x y z) = x + y
20+
21+-- Here, we'd apply the not-a-function to the erased argument 4,
22+-- which would make the program go wrong.
23+main : IO ()
24+main = print $ g (proj 3 f 4)