Fix checkPossible when unifying bound vars

It's not a rigid fail if it's two bound variables that differ.
Fixes #1108

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

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

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

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

test/reg056/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ reg056.idr -o reg056
+rm -f *.ibc