diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr
index fa18ea0..43b2b49 100644
--- a/libs/base/Data/Vect.idr
+++ b/libs/base/Data/Vect.idr
@@ -787,20 +787,20 @@ transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
 --------------------------------------------------------------------------------
 -- Applicative/Monad/Traversable
 --------------------------------------------------------------------------------
--- TODO: Need to work out how to deal with name visibility here
+-- These only work if the length is known at run time! 
+
+implementation {k : Nat} -> Applicative (Vect k) where
+    pure = replicate _
+    fs <*> vs = zipWith apply fs vs
 
--- implementation Applicative (Vect k) where
---     pure = replicate _
---     fs <*> vs = zipWith apply fs vs
--- 
 -- ||| This monad is different from the List monad, (>>=)
 -- ||| uses the diagonal.
--- implementation Monad (Vect len) where
---     m >>= f = diag (map f m)
--- 
--- implementation Traversable (Vect n) where
---     traverse f []        = pure []
---     traverse f (x :: xs) = pure (::) <*> (f x) <*> (traverse f xs)
+implementation {len : Nat} -> Monad (Vect len) where
+    m >>= f = diag (map f m)
+
+implementation {n : Nat} -> Traversable (Vect n) where
+    traverse f []        = pure []
+    traverse f (x :: xs) = pure (::) <*> (f x) <*> (traverse f xs)
 
 --------------------------------------------------------------------------------
 -- Elem
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index d83c928..4a674a9 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -457,8 +457,8 @@ mutual
   --         implementation headers (i.e. note their existence, but not the bodies)
   -- Everything else on the second pass
   getDecl : Pass -> PDecl -> Maybe PDecl
-  getDecl p (PImplementation fc vis _ cons n ps iname ds)
-      = Just (PImplementation fc vis p cons n ps iname ds)
+  getDecl p (PImplementation fc vis _ is cons n ps iname ds)
+      = Just (PImplementation fc vis p is cons n ps iname ds)
 
   getDecl p (PNamespace fc ns ds)
       = Just (PNamespace fc ns (mapMaybe (getDecl p) ds))
@@ -567,21 +567,24 @@ mutual
       expandConstraint (Nothing, p)
           = map (\x => (Nothing, x)) (pairToCons p)
 
-  desugarDecl ps (PImplementation fc vis pass cons tn params impname body)
-      = do cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
+  desugarDecl ps (PImplementation fc vis pass is cons tn params impname body)
+      = do is' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd (snd ntm))
+                                        pure (fst ntm, fst (snd ntm), tm')) is
+           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
                                           pure (fst ntm, tm')) cons
            params' <- traverse (desugar AnyExpr ps) params
            -- Look for bindable names in all the constraints and parameters
            let bnames = concatMap (findBindableNames True ps []) (map snd cons') ++
                         concatMap (findBindableNames True ps []) params'
            let paramsb = map (doBind bnames) params'
+           let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is'
            let consb = map (\ (n, tm) => (n, doBind bnames tm)) cons'
 
            body' <- maybe (pure Nothing)
                           (\b => do b' <- traverse (desugarDecl ps) b
                                     pure (Just (concat b'))) body
            pure [IPragma (\c, nest, env =>
-                             elabImplementation fc vis pass env nest consb
+                             elabImplementation fc vis pass env nest isb consb
                                                 tn paramsb impname 
                                                 body')]
   desugarDecl ps (PRecord fc vis tn params conname fields)
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index b3ba739..83b3fd4 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -37,6 +37,11 @@ bindConstraints fc p [] ty = ty
 bindConstraints fc p ((n, ty) :: rest) sc
     = IPi fc RigW p n ty (bindConstraints fc p rest sc)
 
+bindImpls : FC -> List (Name, RigCount, RawImp) -> RawImp -> RawImp
+bindImpls fc [] ty = ty
+bindImpls fc ((n, r, ty) :: rest) sc
+    = IPi fc r Implicit (Just n) ty (bindImpls fc rest sc)
+
 addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
               List ImpDecl -> 
               (List ImpDecl, List Name) -- Updated body, list of missing methods
@@ -90,6 +95,7 @@ elabImplementation : {auto c : Ref Ctxt Defs} ->
                      {auto m : Ref MD Metadata} ->
                      FC -> Visibility -> Pass ->
                      Env Term vars -> NestedNames vars ->
+                     (implicits : List (Name, RigCount, RawImp)) ->
                      (constraints : List (Maybe Name, RawImp)) ->
                      Name ->
                      (ps : List RawImp) ->
@@ -97,7 +103,7 @@ elabImplementation : {auto c : Ref Ctxt Defs} ->
                      Maybe (List ImpDecl) ->
                      Core ()
 -- TODO: Refactor all these steps into separate functions
-elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
+elabImplementation {vars} fc vis pass env nest is cons iname ps impln mbody
     = do let impName_in = maybe (mkImpl fc iname ps) id impln
          impName <- inCurrentNS impName_in
          syn <- get Syn
@@ -132,7 +138,7 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
          -- Don't make it a hint if it's a named implementation
          let opts = maybe [Inline, Hint True] (const [Inline]) impln
 
-         let initTy = bindConstraints fc AutoImplicit cons 
+         let initTy = bindImpls fc is $ bindConstraints fc AutoImplicit cons 
                          (apply (IVar fc iname) ps)
          let paramBinds = findBindableNames True vars [] initTy
          let impTy = doBind paramBinds initTy
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 919fedc..2595274 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1067,6 +1067,20 @@ constraints fname indents
          pure ((Just n, tm) :: more)
   <|> pure []
 
+implBinds : FileName -> IndentInfo -> EmptyRule (List (Name, RigCount, PTerm))
+implBinds fname indents
+    = do symbol "{"
+         m <- multiplicity
+         rig <- getMult m
+         n <- name
+         symbol ":"
+         tm <- expr pdef fname indents
+         symbol "}"
+         symbol "->"
+         more <- implBinds fname indents
+         pure ((n, rig, tm) :: more)
+  <|> pure []
+
 ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
 ifaceParam fname indents
     = do symbol "("
@@ -1111,6 +1125,7 @@ implDecl fname indents
                                      iname <- name
                                      symbol "]"
                                      pure (Just iname))
+         impls <- implBinds fname indents
          cons <- constraints fname indents
          n <- name
          params <- many (simpleExpr fname indents)
@@ -1119,7 +1134,7 @@ implDecl fname indents
          atEnd indents
          end <- location
          pure (PImplementation (MkFC fname start end)
-                         vis Single cons n params iname 
+                         vis Single impls cons n params iname 
                          (map (collectDefs . concat) body))
 
 fieldDecl : FileName -> IndentInfo -> Rule (List PField)
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 3f8ea7c..83ddad7 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -197,6 +197,7 @@ mutual
                     PDecl
        PImplementation : FC ->
                          Visibility -> Pass ->
+                         (implicits : List (Name, RigCount, PTerm)) ->
                          (constraints : List (Maybe Name, PTerm)) ->
                          Name ->
                          (params : List PTerm) ->
diff --git a/tests/idris2/interactive005/IEdit.idr b/tests/idris2/interactive005/IEdit.idr
index d12c2dc..269251a 100644
--- a/tests/idris2/interactive005/IEdit.idr
+++ b/tests/idris2/interactive005/IEdit.idr
@@ -6,9 +6,9 @@ data Vect : Nat -> Type -> Type where
 
 my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
 
-curry : ((a, b) -> c) -> a -> b -> c
+my_curry : ((a, b) -> c) -> a -> b -> c
 
-uncurry : (a -> b -> c) -> (a, b) -> c
+my_uncurry : (a -> b -> c) -> (a, b) -> c
 
 append : Vect n a -> Vect m a -> Vect (n + m) a
 
diff --git a/tests/idris2/interactive005/expected b/tests/idris2/interactive005/expected
index f766236..a128ec2 100644
--- a/tests/idris2/interactive005/expected
+++ b/tests/idris2/interactive005/expected
@@ -1,12 +1,12 @@
 1/1: Building IEdit (IEdit.idr)
 Main> my_cong x x Refl = Refl
-Main> curry f x y = f (x, y)
-Main> uncurry f x = f (fst x) (snd x)
+Main> my_curry f x y = f (x, y)
+Main> my_uncurry f x = f (fst x) (snd x)
 Main> append [] ys = ys
 append (x :: xs) ys = x :: append xs ys
 Main> zipWith f [] ys = []
 zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 Main> lookup Here (ECons x es) = x
 lookup (There p) (ECons x es) = lookup p es
-Main> Main.uncurry : (a -> b -> c) -> (a, b) -> c
+Main> Main.my_uncurry : (a -> b -> c) -> (a, b) -> c
 Main> Bye for now!
diff --git a/tests/idris2/interactive005/input b/tests/idris2/interactive005/input
index e03404c..8f2ce0c 100644
--- a/tests/idris2/interactive005/input
+++ b/tests/idris2/interactive005/input
@@ -1,8 +1,8 @@
 :gd 7 my_cong
-:gd 9 curry
-:gd 11 uncurry
+:gd 9 my_curry
+:gd 11 my_uncurry
 :gd 13 append
 :gd 15 zipWith
 :gd 27 lookup
-:t uncurry
+:t my_uncurry
 :q
diff --git a/tests/idris2/total006/expected b/tests/idris2/total006/expected
index c876996..a62b99a 100644
--- a/tests/idris2/total006/expected
+++ b/tests/idris2/total006/expected
@@ -1,6 +1,6 @@
 1/1: Building Total (Total.idr)
 Main> Main.count is total
-Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:816:1--820:1 -> Prelude.map
+Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:824:1--828:1 -> Prelude.map
 Main> Main.process is total
 Main> Main.badProcess is not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
 Main> Main.doubleInt is total