From 57cd38ae1106d6f8be2d469e3d97afd340fe88b3 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 20 Dec 2014 22:33:33 +0000
Subject: [PATCH] Fix checkPossible when unifying bound vars

It's not a rigid fail if it's two bound variables that differ.
Fixes #1108
---
 idris.cabal              |  3 +++
 src/Idris/Elab/Clause.hs |  1 +
 test/reg056/expected     |  2 ++
 test/reg056/reg056.idr   | 15 +++++++++++++++
 test/reg056/run          |  3 +++
 5 files changed, 24 insertions(+)
 create mode 100644 test/reg056/expected
 create mode 100644 test/reg056/reg056.idr
 create mode 100755 test/reg056/run

diff --git a/idris.cabal b/idris.cabal
index 052657707..751c49819 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -279,6 +279,9 @@ Extra-source-files:
                        test/reg055/run
                        test/reg055/*.idr
                        test/reg055/expected
+                       test/reg056/run
+                       test/reg056/*.idr
+                       test/reg056/expected
 
                        test/basic001/run
                        test/basic001/*.idr
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 3a86ef694..d81929b36 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -497,6 +497,7 @@ checkPossible info fc tcgen fname lhs_in
 
           ntRec x y | Ref <- x = True
                     | Ref <- y = True
+                    | (Bound, Bound) <- (x, y) = True
                     | otherwise = False -- name is different, unrecoverable
 
 propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm
diff --git a/test/reg056/expected b/test/reg056/expected
new file mode 100644
index 000000000..c07e18ffb
--- /dev/null
+++ b/test/reg056/expected
@@ -0,0 +1,2 @@
+reg056.idr:7:7:dodgy n m Refl is a valid case
+reg056.idr:10:6:nonk Refl is a valid case
diff --git a/test/reg056/reg056.idr b/test/reg056/reg056.idr
new file mode 100644
index 000000000..bbf868bf6
--- /dev/null
+++ b/test/reg056/reg056.idr
@@ -0,0 +1,15 @@
+k : (a : Type) -> (x, y : a) -> (p, q : x = y) -> p = q
+k a x x Refl Refl = Refl
+
+postulate trap : Z = Z
+
+dodgy : (a, b : ()) -> a = b -> Void
+dodgy n m Refl impossible
+
+nonk : (trap = Refl {Z}) -> Void
+nonk Refl impossible
+
+false : Void
+false = nonk (k Nat Z Z trap Refl)
+
+
diff --git a/test/reg056/run b/test/reg056/run
new file mode 100755
index 000000000..776f80938
--- /dev/null
+++ b/test/reg056/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ reg056.idr -o reg056
+rm -f *.ibc