diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.11
+Version:        0.9.11.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -207,6 +207,9 @@
                        test/reg032/run
                        test/reg032/*.idr
                        test/reg032/expected
+                       test/reg033/run
+                       test/reg033/*.idr
+                       test/reg033/expected
 
                        test/basic001/run
                        test/basic001/*.idr
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -1744,6 +1744,17 @@
   mkUniq (PPair fc p l r)
          = do l' <- mkUniq l; r' <- mkUniq r
               return $! PPair fc p l' r'
+  mkUniq (PDPair fc (PRef fc' n) t sc)
+      | t /= Placeholder
+         = do env <- get
+              (n', sc') <- if n `elem` env
+                              then do let n' = uniqueName n (env ++ inScope)
+                                      return (n', shadow n n' sc)
+                              else return (n, sc)
+              put (n' : env)
+              t' <- mkUniq t
+              sc'' <- mkUniq sc'
+              return $! PDPair fc (PRef fc' n') t' sc''
   mkUniq (PDPair fc l t r)
          = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
               return $! PDPair fc l' t' r'
diff --git a/test/reg033/expected b/test/reg033/expected
new file mode 100644
--- /dev/null
+++ b/test/reg033/expected
diff --git a/test/reg033/reg033.idr b/test/reg033/reg033.idr
new file mode 100644
--- /dev/null
+++ b/test/reg033/reg033.idr
@@ -0,0 +1,10 @@
+mapFilter : (alpha -> beta) ->
+           (alpha -> Bool) -> 
+           Vect n alpha -> 
+           (n : Nat ** Vect n beta)
+mapFilter f p Nil = (_ ** Nil)
+mapFilter f p (a :: as) with (p a)
+ | True  = (_  ** (f a) :: (getProof (mapFilter f p as)))
+ | False = mapFilter f p as
+
+
diff --git a/test/reg033/run b/test/reg033/run
new file mode 100644
--- /dev/null
+++ b/test/reg033/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ reg033.idr --check
+rm -f reg033 *.ibc