27cd063 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -237,6 +237,9 @@ Extra-source-files:

237 test/reg041/run

238 test/reg041/*.idr

239 test/reg041/expected

240+ test/reg042/run

241+ test/reg042/*.idr

242+ test/reg042/expected

240

243

241 test/basic001/run

244 test/basic001/run

242 test/basic001/*.idr

245 test/basic001/*.idr

test/reg042/expectednew file+1

@@ -0,0 +1 @@

1+7

test/reg042/reg042.idrnew file+24

@@ -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)

test/reg042/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ reg042 -o reg042 --warnreach

3+./reg042

4+rm -f reg042 *.ibc