Allow implementations to have implicits given

See e.g. Applicative instance in Data.Vect. This allows implementations
to use implicits at run time (by default, they'd be 0 multiplicity so
erased, but it might be useful to have an index available at run time).

At the moment, the parser requires implicits to be given before
constraints. Ideally it should be possible to give them in any order.
I'll come back to this.

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

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)

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

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)

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

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
 

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!

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

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