Fix checkPossible when unifying bound vars
It's not a rigid fail if it's two bound variables that differ.
Fixes #1108
commit57cd38ae1106d6f8be2d469e3d97afd340fe88b3
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 20 Dec 2014, 22:33 (12 years ago)
parent8789717
idris.cabal+3
@@ -279,6 +279,9 @@ Extra-source-files:
279279 test/reg055/run
280280 test/reg055/*.idr
281281 test/reg055/expected
282+ test/reg056/run
283+ test/reg056/*.idr
284+ test/reg056/expected
282285
283286 test/basic001/run
284287 test/basic001/*.idr
src/Idris/Elab/Clause.hs+1
@@ -497,6 +497,7 @@ checkPossible info fc tcgen fname lhs_in
497497
498498 ntRec x y | Ref <- x = True
499499 | Ref <- y = True
500+ | (Bound, Bound) <- (x, y) = True
500501 | otherwise = False -- name is different, unrecoverable
501502
502503propagateParams :: 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