diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -79,6 +79,18 @@
 * More flexible holes.
   Holes can now depend on other holes in a term (such as implicit arguments
   which may be inferred from the definition of the hole).
+* Programs with holes can now be compiled.
+  Attempting to evaluate an expression with a hole results in a run time error.
+* Dependent pairs now can be specified using a telescope-style syntax, without
+  requirement of nesting, e.g. it is possible to now write the following:
+    (a : Type ** n : Nat ** Vect n a)
+* Idris will give a warning if an implicit is bound automatically, but would
+  otherwise be a valid expressio if the name was used as a global
+
+External Dependencies
+---------------------
+
+* Curses has been removed as an external dependancy.
 
 New in 0.10:
 ============
diff --git a/config.mk b/config.mk
--- a/config.mk
+++ b/config.mk
@@ -1,5 +1,12 @@
-CC              ?=cc
-AR              ?=ar
+ifneq (, $(findstring MSYS, $(shell uname -a)))
+	ifeq (cc,$(CC))
+		# In MSYS2, when using the mingw version of gcc, there is no cc -> gcc
+		# symlink. We can't use ?= here because CC is set implicitly to cc.
+		# Cross compiling users can set CC to their cross compiler.
+		CC		=gcc
+	endif
+endif
+
 RANLIB          ?=ranlib
 
 CABAL           :=cabal
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.10.3
+Version:        0.11
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -378,6 +378,9 @@
                        test/basic017/run
                        test/basic017/*.idr
                        test/basic017/expected
+                       test/basic018/run
+                       test/basic018/*.idr
+                       test/basic018/expected
 
                        test/bignum001/run
                        test/bignum001/*.idr
diff --git a/libs/effects/Effects.idr b/libs/effects/Effects.idr
--- a/libs/effects/Effects.idr
+++ b/libs/effects/Effects.idr
@@ -327,6 +327,10 @@
 (<*>) prog v = do fn <- prog
                   arg <- v
                   return (fn arg)
+                  
+(<$>) : (a -> b) ->
+        EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
+(<$>) f v = pure f <*> v
 
 (*>) : EffM m a xs (\v => xs) ->
        EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -93,7 +93,7 @@
 replace Refl prf = prf
 
 ||| Symmetry of propositional equality
-sym : {l:a} -> {r:a} -> l = r -> r = l
+sym : {left:a} -> {right:a} -> left = right -> right = left
 sym Refl = Refl
 
 ||| Transitivity of propositional equality
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -18,6 +18,7 @@
 import Idris.ASTUtils
 import Idris.Erasure
 import Idris.Error
+import Idris.Output
 
 import Debug.Trace
 
@@ -112,7 +113,9 @@
   where checkMVs = do i <- getIState
                       case map fst (idris_metavars i) \\ primDefs of
                             [] -> return ()
-                            ms -> ifail $ "There are undefined holes: " ++ show ms
+                            ms -> do iputStrLn $ "WARNING: There are incomplete holes:\n " ++ show ms
+                                     iputStrLn "\nEvaluation of any of these will crash at run time."
+                                     return ()
         checkTotality = do i <- getIState
                            case idris_totcheckfail i of
                              [] -> return ()
@@ -227,6 +230,9 @@
 irTerm vs env tm@(App _ f a) = do
   ist <- getIState
   case unApply tm of
+    (P _ n _, args)
+        | n `elem` map fst (idris_metavars ist) \\ primDefs
+        -> return $ LError $ "ABORT: Attempt to evaluate hole " ++ show n
     (P _ (UN m) _, args)
         | m == txt "mkForeignPrim"
         -> doForeign vs env (reverse (drop 4 args)) -- drop implicits
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -1471,7 +1471,7 @@
          -- if all of args in ns, then add it
          doAdd (UImplicit n ty : cs) ns t
              | elem n ns
-                   = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)
+                   = PPi (Imp [] Dynamic False Nothing False) n NoFC ty (doAdd cs ns t)
              | otherwise = doAdd cs ns t
 
          -- bind the free names which weren't in the using block
@@ -1479,7 +1479,7 @@
          bindFree (n:ns) tm
              | elem n (map iname uimpls) = bindFree ns tm
              | otherwise
-                    = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
+                    = PPi (Imp [InaccessibleArg] Dynamic False Nothing False) n NoFC Placeholder (bindFree ns tm)
 
          getArgnames (PPi _ n _ c sc)
              = n : getArgnames sc
@@ -1502,9 +1502,9 @@
         getImps (Bind n (Pi _ t _) sc) imps
             | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
          where
-            argInfo n (Imp opt _ _ _) Placeholder
+            argInfo n (Imp opt _ _ _ _) Placeholder
                    = (True, PImp 0 True opt n Placeholder)
-            argInfo n (Imp opt _ _ _) t'
+            argInfo n (Imp opt _ _ _ _) t'
                    = (False, PImp (getPriority i t') True opt n t')
             argInfo n (Exp opt _ _) t'
                    = (InaccessibleArg `elem` opt,
@@ -1536,18 +1536,15 @@
 implicit' info syn ignore n ptm
     = do i <- getIState
          auto <- getAutoImpls
-         if not auto
-           then return ptm
-           else do
-             let (tm', impdata) = implicitise syn ignore i ptm
-             defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
-    --          let (tm'', spos) = findStatics i tm'
-             putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
-             addIBC (IBCImp n)
-             logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
-    --          i <- get
-    --          putIState $ i { idris_statics = addDef n spos (idris_statics i) }
-             return tm'
+         let (tm', impdata) = implicitise auto syn ignore i ptm
+         defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
+--          let (tm'', spos) = findStatics i tm'
+         putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
+         addIBC (IBCImp n)
+         logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
+--          i <- get
+--          putIState $ i { idris_statics = addDef n spos (idris_statics i) }
+         return tm'
   where
     --  Detect unknown names in default arguments and throw error if found.
     defaultArgCheck :: [Name] -> [PArg] -> Idris ()
@@ -1566,15 +1563,17 @@
     notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns --  Known already
     notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n
 
-implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
-implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
+-- Even if auto_implicits is off, we need to call this so we record which
+-- arguments are implicit
+implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
+implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
       let (declimps, ns') = execState (imps True [] tm) ([], [])
-          ns = filter (\n -> implicitable n || elem n (map fst uvars)) $
+          ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
                   ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
           nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
           if null ns
             then (tm, reverse declimps)
-            else implicitise syn ignore ist (pibind uvars nsOrder tm)
+            else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
   where
     uvars = map ipair (filter uimplicit (using syn))
     pvars = syn_params syn
@@ -1599,7 +1598,7 @@
        = do (decls, ns) <- get
             let isn = nub (implNamesIn uvars ty)
             put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
-    imps top env (PPi (Imp l _ _ _) n _ ty sc)
+    imps top env (PPi (Imp l _ _ _ _) n _ ty sc)
         = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
              (decls , ns) <- get
              put (PImp (getPriority ist ty) True l n Placeholder : decls,
@@ -1665,9 +1664,9 @@
     pibind using []     sc = sc
     pibind using (n:ns) sc
       = case lookup n using of
-            Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))
+            Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)) False)
                            n NoFC ty (pibind using ns sc)
-            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))
+            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)) False)
                            n NoFC Placeholder (pibind using ns sc)
 
 -- Add implicit arguments in function calls
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -615,7 +615,8 @@
 data Plicity = Imp { pargopts :: [ArgOpt],
                      pstatic :: Static,
                      pparam :: Bool,
-                     pscoped :: Maybe ImplicitInfo -- Nothing, if top level
+                     pscoped :: Maybe ImplicitInfo, -- Nothing, if top level
+                     pinsource :: Bool -- Explicitly written in source
                    }
              | Exp { pargopts :: [ArgOpt],
                      pstatic :: Static,
@@ -633,13 +634,13 @@
 !-}
 
 is_scoped :: Plicity -> Maybe ImplicitInfo
-is_scoped (Imp _ _ _ s) = s
+is_scoped (Imp _ _ _ s _) = s
 is_scoped _ = Nothing
 
-impl              = Imp [] Dynamic False (Just (Impl False True))
+impl              = Imp [] Dynamic False (Just (Impl False True)) False
 
-forall_imp        = Imp [] Dynamic False (Just (Impl False False))
-forall_constraint = Imp [] Dynamic False (Just (Impl True False))
+forall_imp        = Imp [] Dynamic False (Just (Impl False False)) False
+forall_constraint = Imp [] Dynamic False (Just (Impl True False)) False
 
 expl              = Exp [] Dynamic False
 expl_param        = Exp [] Dynamic True
@@ -784,11 +785,13 @@
                   case_decls :: [(Name, PDecl)],
                   delayed_elab :: [(Int, Elab' EState ())],
                   new_tyDecls :: [RDeclInstructions],
-                  highlighting :: [(FC, OutputAnnotation)]
+                  highlighting :: [(FC, OutputAnnotation)],
+                  auto_binds :: [Name], -- names bound as auto implicits
+                  implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name)
               }
 
 initEState :: EState
-initEState = EState [] [] [] []
+initEState = EState [] [] [] [] [] []
 
 type ElabD a = Elab' EState a
 
@@ -1511,14 +1514,15 @@
                         maxline :: Maybe Int,
                         mut_nesting :: Int,
                         dsl_info :: DSL,
-                        syn_in_quasiquote :: Int }
+                        syn_in_quasiquote :: Int,
+                        syn_toplevel :: Bool }
     deriving Show
 {-!
 deriving instance NFData SyntaxInfo
 deriving instance Binary SyntaxInfo
 !-}
 
-defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True
 
 expandNS :: SyntaxInfo -> Name -> Name
 expandNS syn n@(NS _ _) = n
@@ -1754,7 +1758,7 @@
           case s of
             Static -> text "%static" <> space
             _      -> empty
-    prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
+    prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
       | ppopt_impl ppo =
           depth d . bracket p startPrec $
           lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
@@ -1879,23 +1883,38 @@
                                      align . group . vsep . punctuate (ann comma) $
                                      map (prettySe (decD d) startPrec bnd) elts
         where ann = case pun of
-                      TypeOrTerm  -> id
-                      IsType      -> annName pairTy
-                      IsTerm      -> annName pairCon
-    prettySe d p bnd (PDPair _ _ pun l t r) =
-      depth d $
-      annotated lparen <>
-      left <+>
-      annotated (text "**") <+>
-      prettySe (decD d) startPrec (addBinding bnd) r <>
-      annotated rparen
+                      TypeOrTerm -> id
+                      IsType -> annName pairTy
+                      IsTerm -> annName pairCon
+    prettySe d p bnd dpair@(PDPair _ _ pun l t r)
+      | Just elts <- dPairElts dpair
+      = depth d . enclose (annotated lparen) (annotated rparen) .
+        align . group . vsep . punctuate (space <> annotated (text "**")) $
+        ppElts elts bnd
+      | otherwise
+      = depth d $
+        annotated lparen <>
+        left <+>
+        annotated (text "**") <+>
+        prettySe (decD d) startPrec (addBinding bnd) r <>
+        annotated rparen
       where annotated = case pun of
-              IsType      -> annName sigmaTy
-              IsTerm      -> annName sigmaCon
-              TypeOrTerm  -> id
+              IsType -> annName sigmaTy
+              IsTerm -> annName sigmaCon
+              TypeOrTerm -> id
+
             (left, addBinding) = case (l, pun) of
               (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
-              _                    -> (prettySe (decD d) startPrec bnd l, id)
+              _ ->                    (prettySe (decD d) startPrec bnd l, id)
+
+            ppElts [] bs = []
+            ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
+            ppElts ((PRef _ _ n, t):rs) bs
+              | IsType <- pun
+              =  (bindingOf n False <+> colon <+>
+                  prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
+            ppElts ((l, t):rs) bs
+              = (prettySe (decD d) startPrec bs l) : ppElts rs bs
     prettySe d p bnd (PAlternative ns a as) =
       lparen <> text "|" <> prettyAs <> text "|" <> rparen
         where
@@ -2013,6 +2032,11 @@
     pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
                                | otherwise = Just [x, y]
     pairElts _ = Nothing
+
+    dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
+    dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
+                                   | otherwise = Just [(l, t), (Placeholder, r)]
+    dPairElts _ = Nothing
 
     natns = "Prelude.Nat."
 
diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs
--- a/src/Idris/Core/Elaborate.hs
+++ b/src/Idris/Core/Elaborate.hs
@@ -123,15 +123,21 @@
 errAt thing n ty = transformErr (Elaborating thing n ty)
 
 
+erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
+erunAux f elab 
+    = do s <- get
+         case runStateT elab s of
+            OK (a, s')     -> do put s'
+                                 aux <- getAux
+                                 return $! (a, aux)
+            Error (ProofSearchFail (At f e))
+                           -> lift $ Error (ProofSearchFail (At f e))
+            Error (At f e) -> lift $ Error (At f e)
+            Error e        -> lift $ Error (At f e)
+
 erun :: FC -> Elab' aux a -> Elab' aux a
-erun f elab = do s <- get
-                 case runStateT elab s of
-                    OK (a, s')     -> do put s'
-                                         return $! a
-                    Error (ProofSearchFail (At f e))
-                                   -> lift $ Error (ProofSearchFail (At f e))
-                    Error (At f e) -> lift $ Error (At f e)
-                    Error e        -> lift $ Error (At f e)
+erun f e = do (x, _) <- erunAux f e
+              return x
 
 runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
 runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
@@ -726,7 +732,9 @@
 checkPiGoal :: Name -> Elab' aux ()
 checkPiGoal n
             = do g <- goal
-                 case g of
+                 ctxt <- get_context
+                 env <- get_env
+                 case (normalise ctxt env g) of
                     Bind _ (Pi _ _ _) _ -> return ()
                     _ -> do a <- getNameFrom (sMN 0 "__pargTy")
                             b <- getNameFrom (sMN 0 "__pretTy")
diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -645,8 +645,9 @@
 
 updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
 updateDef n f ctxt
-  = let ds = lookupCtxtName n ctxt in
-        foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds
+  = case lookupCtxtExact n ctxt of
+         Just t -> addDef n (f t) ctxt
+         Nothing -> ctxt
 
 toAlist :: Ctxt a -> [(Name, a)]
 toAlist ctxt = let allns = map snd (Map.toList ctxt) in
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -388,8 +388,8 @@
         rnf _ = ()
 
 instance NFData Plicity where
-        rnf (Imp x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
+        rnf (Imp x1 x2 x3 x4 x5)
+          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
         rnf (Exp x1 x2 x3)
           = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (Constraint x1 x2)
@@ -681,13 +681,13 @@
         rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
 
 instance NFData SyntaxInfo where
-        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
+        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
           = rnf x1 `seq`
               rnf x2 `seq`
                 rnf x3 `seq`
                   rnf x4 `seq`
                     rnf x5 `seq`
-                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()
+                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()
 
 instance NFData OutputMode where
   rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -112,14 +112,14 @@
           = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)
     de env (_ : is) (Bind n (Pi (Just impl) ty _) sc)
        | toplevel_imp impl -- information in 'imps' repeated
-          = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)
+          = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)
     de env is (Bind n (Pi (Just impl) ty _) sc)
        | tcinstance impl
           = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)
        | otherwise
-          = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)
+          = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)
     de env ((PImp { argopts = opts }):is) (Bind n (Pi _ ty _) sc)
-          = PPi (Imp opts Dynamic False Nothing) n NoFC (de env [] ty) (de ((n,n):env) is sc)
+          = PPi (Imp opts Dynamic False Nothing False) n NoFC (de env [] ty) (de ((n,n):env) is sc)
     de env (PConstraint _ _ _ _:is) (Bind n (Pi _ ty _) sc)
           = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)
     de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)
@@ -488,7 +488,7 @@
     else empty
 pprintErr' i (ReflectionFailed msg err) =
   text "When attempting to perform error reflection, the following internal error occurred:" <>
-  indented (pprintErr' i err) <>
+  indented (pprintErr' i err) <+> text msg <+>
   text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
 pprintErr' i (ElabScriptDebug msg tm holes) =
   text "Elaboration halted." <>
diff --git a/src/Idris/Directives.hs b/src/Idris/Directives.hs
--- a/src/Idris/Directives.hs
+++ b/src/Idris/Directives.hs
@@ -29,8 +29,10 @@
 directiveAction (DInclude cgn hdr) = do addHdr cgn hdr
                                         addIBC (IBCHeader cgn hdr)
 
-directiveAction (DHide n) = do setAccessibility n Hidden
-                               addIBC (IBCAccess n Hidden)
+directiveAction (DHide n') = do i <- getIState
+                                ns <- allNamespaces n'
+                                mapM_ (\n -> do setAccessibility n Hidden
+                                                addIBC (IBCAccess n Hidden)) ns
 
 directiveAction (DFreeze n) = do setAccessibility n Frozen
                                  addIBC (IBCAccess n Frozen)
@@ -80,3 +82,10 @@
                               [(n', _)] -> return n'
                               []        -> throwError (NoSuchVariable n)
                               more      -> throwError (CantResolveAlts (map fst more))
+
+allNamespaces :: Name -> Idris [Name]
+allNamespaces n = do i <- getIState
+                     case lookupCtxtName n (idris_implicits i) of
+                              [(n', _)] -> return [n']
+                              []        -> throwError (NoSuchVariable n)
+                              more      -> return (map fst more)
diff --git a/src/Idris/Elab/AsPat.hs b/src/Idris/Elab/AsPat.hs
--- a/src/Idris/Elab/AsPat.hs
+++ b/src/Idris/Elab/AsPat.hs
@@ -28,6 +28,14 @@
     = do as_tm <- mapM collectAs (map getTm as)
          let as' = zipWith (\a tm -> a { getTm = tm }) as as_tm
          return (PApp fc t as') -- only valid on args
+-- only for 'ExactlyOne' since it means the alternatives will have the
+-- same form, so we can assume we only need to extract from the first one
+collectAs tm@(PAlternative ns (ExactlyOne d) (a : as)) 
+    = do a' <- collectAs a
+         pats <- get
+         as' <- mapM collectAs as -- just to drop the '@'
+         put pats -- discard later ones, since they're repeated
+         return (PAlternative ns (ExactlyOne d) (a' : as'))
 collectAs x = return x
 
 -- | Replace _-patterns under @-patterns with fresh names that can be
diff --git a/src/Idris/Elab/Class.hs b/src/Idris/Elab/Class.hs
--- a/src/Idris/Elab/Class.hs
+++ b/src/Idris/Elab/Class.hs
@@ -84,7 +84,7 @@
 
          mapM_ (checkConstraintName (map (\(x, _, _) -> x) ps)) constraintNames
 
-         logElab 1 $ "Building methods " ++ show mnames
+         logElab 2 $ "Building methods " ++ show mnames
          ims <- mapM (tdecl mnames) mdecls
          defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
                       (filter clause ds)
@@ -176,7 +176,7 @@
                 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
                 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
                          (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
-                                              (\ l s p -> Imp l s p Nothing) t'))),
+                                              (\ l s p -> Imp l s p Nothing True) t'))),
                          (n, (nfc, syn, o, t) ) )
     tdecl _ _ = ifail "Not allowed in a class declaration"
 
@@ -250,7 +250,7 @@
              return [PTy doc [] syn fc o m mfc ty',
                      PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
 
-    getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc
+    getMArgs (PPi (Imp _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
     getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc
     getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
     getMArgs _ = []
@@ -270,7 +270,7 @@
     rhsArgs [] _ = []
 
     insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
-    insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
+    insertConstraint c all (PPi p@(Imp _ _ _ _ _) n fc ty sc)
                               = PPi p n fc ty (insertConstraint c all sc)
     insertConstraint c all sc = let dictN = sMN 0 "__class"
                                 in  PPi (constraint { pstatic = Static })
@@ -289,7 +289,7 @@
        addC _ _ tm = tm
 
     -- make arguments explicit and don't bind class parameters
-    toExp ns e (PPi (Imp l s p _) n fc ty sc)
+    toExp ns e (PPi (Imp l s p _ _) n fc ty sc)
         | n `elem` ns = toExp ns e sc
         | otherwise = PPi (e l s p) n fc ty (toExp ns e sc)
     toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs
--- a/src/Idris/Elab/Instance.hs
+++ b/src/Idris/Elab/Instance.hs
@@ -233,7 +233,7 @@
     lamBind i (PPi _ n _ ty sc) sc'
           = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
     lamBind i _ sc = sc
-    methArgs i (PPi (Imp _ _ _ _) n _ ty sc)
+    methArgs i (PPi (Imp _ _ _ _ _) n _ ty sc)
         = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
     methArgs i (PPi (Exp _ _ _) n _ ty sc)
         = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc
@@ -266,7 +266,7 @@
     conbind [] x = x
 
     coninsert :: [(Name, PTerm)] -> PTerm -> PTerm
-    coninsert cs (PPi p@(Imp _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)
+    coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)
     coninsert cs sc = conbind cs sc
 
     -- Reorder declarations to be in the same order as defined in the
diff --git a/src/Idris/Elab/Record.hs b/src/Idris/Elab/Record.hs
--- a/src/Idris/Elab/Record.hs
+++ b/src/Idris/Elab/Record.hs
@@ -441,7 +441,7 @@
 
 -- | Creates a PArg with a given plicity, name, and term.
 asArg :: Plicity -> Name -> PTerm -> PArg
-asArg (Imp os _ _ _) n t = PImp 0 False os n t
+asArg (Imp os _ _ _ _) n t = PImp 0 False os n t
 asArg (Exp os _ _) n t = PExp 0 os n t
 asArg (Constraint os _) n t = PConstraint 0 os n t
 asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
diff --git a/src/Idris/Elab/RunElab.hs b/src/Idris/Elab/RunElab.hs
--- a/src/Idris/Elab/RunElab.hs
+++ b/src/Idris/Elab/RunElab.hs
@@ -36,7 +36,7 @@
         tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState
                  (transformErr RunningElabScript
                    (erun fc (do tm <- runElabAction ist fc [] script ns
-                                EState is _ impls highlights <- getAux
+                                EState is _ impls highlights _ _ <- getAux
                                 ctxt <- get_context
                                 let ds = [] -- todo
                                 log <- getLog
diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -120,7 +120,7 @@
          when tydecl (do mkPat
                          update_term liftPats
                          update_term orderPats)
-         EState is _ impls highlights <- getAux
+         EState is _ impls highlights _ _ <- getAux
          tt <- get_term
          ctxt <- get_context
          let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
@@ -165,7 +165,7 @@
          -- unification
          when (not (null dots)) $
             lift (Error (CantMatch (getInferTerm tm)))
-         EState is _ impls highlights <- getAux
+         EState is _ impls highlights _ _ <- getAux
          tt <- get_term
          ctxt <- get_context
          let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
@@ -232,11 +232,11 @@
          end_unify
          ptm <- get_term
          when (pattern || intransform) -- convert remaining holes to pattern vars
-              (do update_term orderPats
-                  unify_all
+              (do unify_all
                   matchProblems False -- only the ones we matched earlier
                   unifyProblems
-                  mkPat)
+                  mkPat
+                  update_term liftPats)
   where
     pattern = emode == ELHS
     intransform = emode == ETransLHS
@@ -412,16 +412,6 @@
                                                 [pimp (sUN "A") Placeholder False,
                                                  pimp (sUN "B") Placeholder False,
                                                  pexp l, pexp r])
---                         _ -> try' (elab' ina (Just fc) (PApp fc (PRef fc pairCon)
---                                                 [pimp (sUN "A") Placeholder False,
---                                                  pimp (sUN "B") Placeholder False,
---                                                  pexp l, pexp r]))
---                                   (elab' ina (Just fc) (PApp fc (PRef fc upairCon)
---                                                 [pimp (sUN "A") Placeholder False,
---                                                  pimp (sUN "B") Placeholder False,
---                                                  pexp l, pexp r]))
---                                   True
-
     elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
             = case t of
                 Placeholder ->
@@ -589,7 +579,9 @@
       | pattern && not reflection && not (e_qq ec) && e_nomatching ec
               = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
       | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
-        = do let ina = e_inarg ec
+        = do ty <- goal
+             testImplicitWarning fc n ty
+             let ina = e_inarg ec
                  guarded = e_guarded ec
                  inty = e_intype ec
              ctxt <- get_context
@@ -676,6 +668,7 @@
                highlightSource nfc (AnnBoundName n False)
     elab' ina fc (PPi p n nfc Placeholder sc)
           = do attack; arg n (is_scoped p) (sMN 0 "ty")
+               addAutoBind p n
                addPSname n -- okay for proof search
                elabE (ina { e_inarg = True, e_intype = True }) fc sc
                solve
@@ -687,6 +680,7 @@
                         MN _ _ -> unique_hole n
                         _ -> return n
                forall n' (is_scoped p) (Var tyn)
+               addAutoBind p n'
                addPSname n' -- okay for proof search
                focus tyn
                let ec' = ina { e_inarg = True, e_intype = True }
@@ -1207,7 +1201,7 @@
              -- We now have an elaborated term. Reflect it and solve the
              -- original goal in the original proof state, preserving highlighting
              env <- get_env
-             EState _ _ _ hs <- getAux
+             EState _ _ _ hs _ _ <- getAux
              loadState
              updateAux (\aux -> aux { highlighting = hs })
 
@@ -1403,8 +1397,8 @@
     -- case block functions that don't yet exist)
     fullyElaborated :: Term -> ElabD ()
     fullyElaborated (P _ n _) =
-      do EState cases _ _ _ <- getAux
-         case lookup n cases of
+      do estate <- getAux
+         case lookup n (case_decls estate) of
            Nothing -> return ()
            Just _  -> lift . tfail $ ElabScriptStaging n
     fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated
@@ -1548,6 +1542,31 @@
                  return result
     elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
       fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
+
+    addAutoBind :: Plicity -> Name -> ElabD ()
+    addAutoBind (Imp _ _ _ _ False) n
+         = updateAux (\est -> est { auto_binds = n : auto_binds est })
+    addAutoBind _ _ = return ()
+
+    testImplicitWarning :: FC -> Name -> Type -> ElabD ()
+    testImplicitWarning fc n goal 
+       | implicitable n && emode == ETyDecl
+           = do env <- get_env
+                est <- getAux
+                when (n `elem` auto_binds est) $ 
+                    tryUnify env (lookupTyName n (tt_ctxt ist))
+       | otherwise = return ()
+      where
+        tryUnify env [] = return ()
+        tryUnify env ((nm, ty) : ts)
+             = do inj <- get_inj
+                  hs <- get_holes
+                  case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)
+                          inj hs [] [] of
+                    OK _ -> 
+                       updateAux (\est -> est { implicit_warnings =
+                                          (fc, nm) : implicit_warnings est })
+                    _ -> tryUnify env ts
 
 -- For every alternative, look at the function at the head. Automatically resolve
 -- any nested alternatives where that function is also at the head
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -64,12 +64,15 @@
          let ty = addImpl (imp_methods syn) i ty'
 
          logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
-         logElab 5 $ show "with methods " ++ show (imp_methods syn)
+         logElab 5 $ "with methods " ++ show (imp_methods syn)
          logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
 
-         (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-
+         ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-
             tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState
-                     (errAt "type of " n Nothing (erun fc (build i info ETyDecl [] n ty)))
+                     (errAt "type of " n Nothing 
+                        (erunAux fc (build i info ETyDecl [] n ty)))
+
+         displayWarnings est
          setContext ctxt'
          processTacticDecls info newDecls
          sendHighlighting highlights 
diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs
--- a/src/Idris/Elab/Utils.hs
+++ b/src/Idris/Elab/Utils.hs
@@ -395,3 +395,12 @@
     case lookupCtxt n opt of
         [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }
         _    -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }
+
+displayWarnings :: EState -> Idris ()
+displayWarnings est 
+     = mapM_ displayImpWarning (implicit_warnings est)
+  where
+    displayImpWarning :: (FC, Name) -> Idris ()
+    displayImpWarning (fc, n) = 
+       iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
+                   ++ "\tDid you mean to refer to " ++ show n ++ "?"
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -1154,7 +1154,7 @@
 instance Binary Plicity where
         put x
           = case x of
-                Imp x1 x2 x3 x4 ->
+                Imp x1 x2 x3 x4 _ ->
                              do putWord8 0
                                 put x1
                                 put x2
@@ -1181,7 +1181,7 @@
                            x2 <- get
                            x3 <- get
                            x4 <- get
-                           return (Imp x1 x2 x3 x4)
+                           return (Imp x1 x2 x3 x4 False)
                    1 -> do x1 <- get
                            x2 <- get
                            x3 <- get
@@ -1461,7 +1461,7 @@
                     _ -> error "Corrupted binary data for Using"
 
 instance Binary SyntaxInfo where
-        put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)
+        put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _)
           = do put x1
                put x2
                put x3
@@ -1477,7 +1477,7 @@
                x5 <- get
                x6 <- get
                x7 <- get
-               return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)
+               return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True)
 
 instance (Binary t) => Binary (PClause' t) where
         put x
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -487,48 +487,57 @@
     -- Prevent syntax variable capture by making all binders under syntax unique
     -- (the ol' Common Lisp GENSYM approach)
     uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
-    uniquifyBinders userNames = fixBind []
+    uniquifyBinders userNames = fixBind 0 []
       where
-        fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm
-        fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =
+        fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
+        fixBind 0 rens (PRef fc hls n) | Just n' <- lookup n rens =
           return $ PRef fc hls n'
-        fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
+        fixBind 0 rens (PPatvar fc n) | Just n' <- lookup n rens =
           return $ PPatvar fc n'
-        fixBind rens (PLam fc n nfc ty body)
-          | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
+        fixBind 0 rens (PLam fc n nfc ty body)
+          | n `elem` userNames = liftM2 (PLam fc n nfc)
+                                        (fixBind 0 rens ty)
+                                        (fixBind 0 rens body)
           | otherwise =
-            do ty' <- fixBind rens ty
+            do ty' <- fixBind 0 rens ty
                n' <- gensym n
-               body' <- fixBind ((n,n'):rens) body
+               body' <- fixBind 0 ((n,n'):rens) body
                return $ PLam fc n' nfc ty' body'
-        fixBind rens (PPi plic n nfc argTy body)
+        fixBind 0 rens (PPi plic n nfc argTy body)
           | n `elem` userNames = liftM2 (PPi plic n nfc)
-                                        (fixBind rens argTy)
-                                        (fixBind rens body)
+                                        (fixBind 0 rens argTy)
+                                        (fixBind 0 rens body)
           | otherwise =
-            do ty' <- fixBind rens argTy
+            do ty' <- fixBind 0 rens argTy
                n' <- gensym n
-               body' <- fixBind ((n,n'):rens) body
+               body' <- fixBind 0 ((n,n'):rens) body
                return $ (PPi plic n' nfc ty' body')
-        fixBind rens (PLet fc n nfc ty val body)
+        fixBind 0 rens (PLet fc n nfc ty val body)
           | n `elem` userNames = liftM3 (PLet fc n nfc)
-                                        (fixBind rens ty)
-                                        (fixBind rens val)
-                                        (fixBind rens body)
+                                        (fixBind 0 rens ty)
+                                        (fixBind 0 rens val)
+                                        (fixBind 0 rens body)
           | otherwise =
-            do ty' <- fixBind rens ty
-               val' <- fixBind rens val
+            do ty' <- fixBind 0 rens ty
+               val' <- fixBind 0 rens val
                n' <- gensym n
-               body' <- fixBind ((n,n'):rens) body
+               body' <- fixBind 0 ((n,n'):rens) body
                return $ PLet fc n' nfc ty' val' body'
-        fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =
+        fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =
           return $ PMatchApp fc n'
         -- Also rename resolved quotations, to allow syntax rules to
         -- have quoted references to their own bindings.
-        fixBind rens (PQuoteName n True fc) | Just n' <- lookup n rens =
+        fixBind 0 rens (PQuoteName n True fc) | Just n' <- lookup n rens =
           return $ PQuoteName n' True fc
-        fixBind rens x = descendM (fixBind rens) x
 
+        -- Don't mess with quoted terms
+        fixBind q rens (PQuasiquote tm goal) =
+          flip PQuasiquote goal <$> fixBind (q + 1) rens tm
+        fixBind q rens (PUnquote tm) =
+          PUnquote <$> fixBind (q - 1) rens tm
+          
+        fixBind q rens x = descendM (fixBind q rens) x
+
         gensym :: Name -> IdrisParser Name
         gensym n = do ist <- get
                       let idx = idris_name ist
@@ -599,7 +608,9 @@
                         return (doc, argDocs, fc, opts', n, nfc, acc))
                  ty <- typeExpr (allowImp syn)
                  terminator
-                 addAcc n acc
+                 -- If it's a top level function, note the accessibility
+                 -- rules
+                 when (syn_toplevel syn) $ addAcc n acc
                  return (PTy doc argDocs syn fc opts' n nfc ty)
             <|> postulate syn
             <|> caf syn
@@ -1116,7 +1127,7 @@
                         Nothing -> fail "Invalid clause"
               (do r <- rhs syn n
                   let ctxt = tt_ctxt ist
-                  let wsyn = syn { syn_namespace = [] }
+                  let wsyn = syn { syn_namespace = [], syn_toplevel = False }
                   (wheres, nmap) <- choice [do x <- whereBlock n wsyn
                                                popIndent
                                                return x,
diff --git a/src/Idris/Parser/Expr.hs b/src/Idris/Parser/Expr.hs
--- a/src/Idris/Parser/Expr.hs
+++ b/src/Idris/Parser/Expr.hs
@@ -398,7 +398,7 @@
         <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
         <|> proofExpr syn
         <|> tacticsExpr syn
-        <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
+        <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
         <|> do reserved "AnyType"; return $ PUniverse AllTypes
         <|> PType <$> reservedFC "Type"
         <|> do reserved "UniqueType"; return $ PUniverse UniqueType
@@ -440,16 +440,16 @@
 bracketed syn = do (FC fn (sl, sc) _) <- getFC
                    lchar '(' <?> "parenthesized expression"
                    bracketed' (FC fn (sl, sc) (sl, sc+1)) syn
+
 {- |Parses the rest of an expression in braces
 @
 Bracketed' ::=
   ')'
   | Expr ')'
   | ExprList ')'
-  | Expr '**' Expr ')'
+  | DependentPair ')'
   | Operator Expr ')'
   | Expr Operator ')'
-  | Name ':' Expr '**' Expr ')'
   ;
 @
 -}
@@ -458,14 +458,7 @@
             do (FC f start (l, c)) <- getFC
                lchar ')'
                return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
-        <|> try (do (ln, lnfc) <- name
-                    colonFC <- lcharFC ':'
-                    lty <- expr syn
-                    starsFC <- reservedOpFC "**"
-                    fc <- getFC
-                    r <- expr syn
-                    close <- lcharFC ')'
-                    return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))
+        <|> try (dependentPair TypeOrTerm [] open syn)
         <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
                     -- No prefix operators! (bit of a hack here...)
                     if (o == "-" || o == "!")
@@ -486,20 +479,59 @@
         <|> do l <- expr syn
                bracketedExpr syn open l
 
+
+
+{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
+dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
+dependentPair pun prev openFC syn =
+  if prev == [] then
+      nametypePart <|> namePart
+  else
+    case pun of
+      IsType -> nametypePart <|> namePart <|> exprPart True
+      IsTerm -> exprPart False
+      TypeOrTerm -> nametypePart <|> namePart <|> exprPart False
+  where nametypePart = do
+          (ln, lnfc, colonFC) <- try $ do
+            (ln, lnfc) <- name
+            colonFC <- lcharFC ':'
+            return (ln, lnfc, colonFC)
+          lty <- expr' syn
+          starsFC <- reservedOpFC "**"
+          dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
+        namePart = try $ do
+          (ln, lnfc) <- name
+          starsFC <- reservedOpFC "**"
+          dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
+        exprPart isEnd = do
+          e <- expr syn
+          sepFCE <-
+            let stars = (Left <$> reservedOpFC "**")
+                ending = (Right <$> lcharFC ')')
+            in if isEnd then ending else stars <|> ending
+          case sepFCE of
+            Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
+            Right closeFC ->
+              return (mkPDPairs pun openFC closeFC (reverse prev) e)
+        mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =
+              (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)
+                               pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
+        mergePDPairs pun starsFC' [] r = r
+        mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
+           PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
+
 -- | Parse the contents of parentheses, after an expression has been parsed.
 bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
 bracketedExpr syn openParenFC e =
              do lchar ')'; return e
-        <|>  do exprs <- many (do comma <- lcharFC ','
+        <|>  do exprs <- some (do comma <- lcharFC ','
                                   r <- expr syn
                                   return (r, comma))
                 closeParenFC <- lcharFC ')'
                 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
                 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
         <|>  do starsFC <- reservedOpFC "**"
-                r <- expr syn
-                closeParenFC <- lcharFC ')'
-                return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)
+                dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
         <?> "end of bracketed expression"
   where mergePairs :: [(PTerm, FC)] -> PTerm
         mergePairs [(t, fc)]    = t
@@ -1047,10 +1079,10 @@
    sc <- expr syn
    let (im,cl)
           = if implicitAllowed syn
-               then (Imp opts st False (Just (Impl False True)),
+               then (Imp opts st False (Just (Impl False True)) True,
                       constraint)
-               else (Imp opts st False (Just (Impl False False)),
-                     Imp opts st False (Just (Impl True False)))
+               else (Imp opts st False (Just (Impl False False)) True,
+                     Imp opts st False (Just (Impl True False)) True)
    return (bindList (PPi im) xt
            (bindList (PPi cl) cs sc))
 
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,4 +1,4 @@
-resolver: lts-5.5
+resolver: lts-5.9
 
 packages:
   - '.'
diff --git a/test/basic009/expected b/test/basic009/expected
--- a/test/basic009/expected
+++ b/test/basic009/expected
@@ -1,4 +1,6 @@
 MAIN-PASS
+Faulty.idr:6:9-12:WARNING: num is bound as an implicit
+	Did you mean to refer to A.num?
 Faulty.idr:7:7:
 When checking right hand side of fault with expected type
         num = 0
diff --git a/test/basic012/basic012a.idr b/test/basic012/basic012a.idr
new file mode 100644
--- /dev/null
+++ b/test/basic012/basic012a.idr
@@ -0,0 +1,10 @@
+Symmetric : {c : Type} -> (c -> c -> Type) -> Type
+Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a
+
+record Symmetry (t : Type) (rel : t -> t -> Type) where
+  constructor MkSymmetry
+  is_symmetric : Symmetric {c=t} rel
+
+symmetry : {ty : Type} -> Symmetry ty (=)
+symmetry = MkSymmetry sym
+
diff --git a/test/basic012/run b/test/basic012/run
--- a/test/basic012/run
+++ b/test/basic012/run
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
 ${IDRIS:-idris} $@ basic012.idr -o basic012
 ./basic012
+${IDRIS:-idris} $@ basic012a.idr --check
 rm -f basic012 *.ibc
diff --git a/test/basic018/basic018.idr b/test/basic018/basic018.idr
new file mode 100644
--- /dev/null
+++ b/test/basic018/basic018.idr
@@ -0,0 +1,14 @@
+import Data.Vect
+
+thing : Nat
+thing = 42
+
+foo : -- (thing : Nat) ->
+      Vect thing elem
+
+bar : {thing : Nat} ->
+      Vect thing elem
+
+test : thing = S 41
+test = Refl
+
diff --git a/test/basic018/expected b/test/basic018/expected
new file mode 100644
--- /dev/null
+++ b/test/basic018/expected
@@ -0,0 +1,18 @@
+basic018.idr:7:12-17:WARNING: thing is bound as an implicit
+	Did you mean to refer to Main.thing?
+basic018.idr:12:8-13:WARNING: thing is bound as an implicit
+	Did you mean to refer to Main.thing?
+basic018.idr:13:6:
+When checking right hand side of test with expected type
+        thing = S 41
+
+Type mismatch between
+        42 = 42 (Type of Refl)
+and
+        thing = 42 (Expected type)
+
+Specifically:
+        Type mismatch between
+                42
+        and
+                thing
diff --git a/test/basic018/run b/test/basic018/run
new file mode 100644
--- /dev/null
+++ b/test/basic018/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ basic018.idr --check --nocolor
+rm -f *.ibc
diff --git a/test/disambig002/disambig002.idr b/test/disambig002/disambig002.idr
--- a/test/disambig002/disambig002.idr
+++ b/test/disambig002/disambig002.idr
@@ -75,7 +75,7 @@
                     (a : A) ->
                     (p : P a) ->
                     (ss : Vect n (DPair A P)) ->
-                    Elem a (map fst ss) ->
+                    Elem a (map DPair.fst ss) ->
                     Elem (a ** p) ss
 
 toVectComplete : {A   : Type} ->
diff --git a/test/proof003/test015.idr b/test/proof003/test015.idr
--- a/test/proof003/test015.idr
+++ b/test/proof003/test015.idr
@@ -44,11 +44,11 @@
 testBin : Maybe (Binary 8 42)
 testBin = natToBin _ _
 
-pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
-term    syntax bitpair [x] [y] = (_ ** (_ ** (x, y, Refl)))
+pattern syntax bitpair [x] [y] = (_ ** _ ** (x, y, _))
+term    syntax bitpair [x] [y] = (_ ** _ ** (x, y, Refl))
 
 addBit : Bit x -> Bit y -> Bit c ->
-          (bX ** (bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX)))
+          (bX ** bY ** (Bit bX, Bit bY, c + x + y = bY + 2 * bX))
 addBit B0 B0 B0 = bitpair B0 B0
 addBit B0 B0 B1 = bitpair B0 B1
 addBit B0 B1 B0 = bitpair B0 B1
diff --git a/test/proofsearch002/Process.idr b/test/proofsearch002/Process.idr
--- a/test/proofsearch002/Process.idr
+++ b/test/proofsearch002/Process.idr
@@ -123,10 +123,10 @@
             ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->
             Process b iface hs hs'' p p''
 
-     Fork : Process () serveri [] (const []) (runningServer 1) (const doneServer) ->
+     Fork : Process () serveri [] (const []) (runningServer 1) (const Process.doneServer) ->
             Process (ProcID serveri) iface hs (const hs) p (\res => (newServer res p))
      Work : (worker : (pid : ProcID iface) -> Worker [pid] ()) ->
-            (waiter : Process t iface hs (const hs) (runningServer 1) (const doneServer)) ->
+            (waiter : Process t iface hs (const hs) (runningServer 1) (const Process.doneServer)) ->
             Process t iface hs (const hs) p (const p)
 
      Request : (r : ProcID serveri) -> (x : serveri ty) ->
diff --git a/test/reg056/reg056.idr b/test/reg056/reg056.idr
--- a/test/reg056/reg056.idr
+++ b/test/reg056/reg056.idr
@@ -6,7 +6,7 @@
 dodgy : (a, b : ()) -> a = b -> Void
 dodgy n m Refl impossible
 
-nonk : (trap = Refl {x = Z}) -> Void
+nonk : (Main.trap = Refl {x = Z}) -> Void
 nonk Refl impossible
 
 false : Void
diff --git a/test/reg068/expected b/test/reg068/expected
--- a/test/reg068/expected
+++ b/test/reg068/expected
@@ -3,5 +3,7 @@
 This is likely to lead to problems!
 reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
 This is likely to lead to problems!
+reg068.idr:2:8-11:WARNING: nat is bound as an implicit
+	Did you mean to refer to Main.nat?
 reg068.idr:2:6:When checking constructor Main.ze:
 Type level variable nat is not Main.nat