57cd38a · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

279 test/reg055/run

280 test/reg055/*.idr

281 test/reg055/expected

282+ test/reg056/run

283+ test/reg056/*.idr

284+ test/reg056/expected

282

285

283 test/basic001/run

286 test/basic001/run

284 test/basic001/*.idr

287 test/basic001/*.idr

src/Idris/Elab/Clause.hs+1

@@ -497,6 +497,7 @@ checkPossible info fc tcgen fname lhs_in

497

498 ntRec x y | Ref <- x = True

499 | Ref <- y = True

500+ | (Bound, Bound) <- (x, y) = True

500 | otherwise = False -- name is different, unrecoverable

501 | otherwise = False -- name is different, unrecoverable

501

502

502propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

503propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

test/reg056/expectednew file+2

@@ -0,0 +1,2 @@

1+reg056.idr:7:7:dodgy n m Refl is a valid case

2+reg056.idr:10:6:nonk Refl is a valid case

test/reg056/reg056.idrnew file+15

@@ -0,0 +1,15 @@

1+k : (a : Type) -> (x, y : a) -> (p, q : x = y) -> p = q

2+k a x x Refl Refl = Refl

3+

4+postulate trap : Z = Z

5+

6+dodgy : (a, b : ()) -> a = b -> Void

7+dodgy n m Refl impossible

8+

9+nonk : (trap = Refl {Z}) -> Void

10+nonk Refl impossible

11+

12+false : Void

13+false = nonk (k Nat Z Z trap Refl)

14+

15+

test/reg056/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg056.idr -o reg056

3+rm -f *.ibc