reg042.idr

-- 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 = print $ g (proj 3 f 4)