-- This regtest tests for incorrect erasure from underapplied data constructors. data T : Type where C : Nat -> Nat -> Nat -> T data Q : Type where D : (Nat -> T) -> Q -- The bug was here: (C 3 4) would compile to plain data, -- not to a function that would expect another (albeit erased) argument. f : Q f = D (C 3 4) proj : Nat -> Q -> Nat -> T proj Z (D f) = f proj (S n) q = proj n q g : T -> Nat g (C x y z) = x + y -- Here, we'd apply the not-a-function to the erased argument 4, -- which would make the program go wrong. main : IO () main = printLn $ g (proj 3 f 4)