From a422294f36339dc0a0a12f0ce9733f4e1b00a4b0 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Wed, 10 Jul 2019 16:54:40 +0200
Subject: [PATCH] Pass auto implicits through interfaces

This allows 'traverse' to work now (it was treating them as normal
implicits, so building the wrong form of application)
---
 libs/prelude/Prelude.idr          | 40 +++++++++++++++++++++++++++++++
 src/Idris/Elab/Implementation.idr |  5 +++-
 tests/idris2/total006/expected    |  2 +-
 3 files changed, 45 insertions(+), 2 deletions(-)

diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr
index a9449af..afe4508 100644
--- a/libs/prelude/Prelude.idr
+++ b/libs/prelude/Prelude.idr
@@ -522,6 +522,36 @@ public export
 product : (Foldable t, Num a) => t a -> a
 product = foldr (*) 1
 
+public export
+traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
+traverse_ f = foldr ((*>) . f) (pure ())
+
+||| Evaluate each computation in a structure and discard the results
+public export
+sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
+sequence_ = foldr (*>) (pure ())
+
+||| Like `traverse_` but with the arguments flipped
+public export
+for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
+for_ = flip traverse_
+
+public export
+interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
+  ||| Map each element of a structure to a computation, evaluate those
+  ||| computations and combine the results.
+  traverse : Applicative f => (a -> f b) -> t a -> f (t b)
+
+||| Evaluate each computation in a structure and collect the results
+public export
+sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
+sequence = traverse id
+
+||| Like `traverse` but with the arguments flipped
+public export
+for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
+for = flip traverse
+
 -----------
 -- NATS ---
 -----------
@@ -640,6 +670,11 @@ Foldable Maybe where
   foldr _ z Nothing  = z
   foldr f z (Just x) = f x z
 
+public export
+Traversable Maybe where
+  traverse f Nothing = pure Nothing
+  traverse f (Just x) = (pure Just) <*> (f x)
+
 ---------
 -- DEC --
 ---------
@@ -753,6 +788,11 @@ public export
 Monad List where
   m >>= f = concatMap f m
 
+public export
+Traversable List where
+  traverse f [] = pure []
+  traverse f (x::xs) = pure (::) <*> (f x) <*> (traverse f xs)
+
 public export
 elem : Eq a => a -> List a -> Bool
 x `elem` [] = False
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index f838d79..4a795a2 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -146,6 +146,7 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
                -- parent constraints, then the method implementations
                defs <- get Ctxt
                let fldTys = getFieldArgs !(normaliseHoles defs [] conty)
+               log 5 $ "Field types " ++ show fldTys
                let irhs = apply (IVar fc con)
                                 (map (const (ISearch fc 500)) (parents cdata)
                                  ++ map (mkMethField impsp fldTys) fns)
@@ -198,7 +199,9 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
     applyTo fc tm [] = tm
     applyTo fc tm ((x, c, Explicit) :: xs)
         = applyTo fc (IApp fc tm (IVar fc x)) xs
-    applyTo fc tm ((x, c, _) :: xs)
+    applyTo fc tm ((x, c, AutoImplicit) :: xs)
+        = applyTo fc (IImplicitApp fc tm Nothing (IVar fc x)) xs
+    applyTo fc tm ((x, c, Implicit) :: xs)
         = applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
 
     -- When applying the method in the field for the record, eta expand
diff --git a/tests/idris2/total006/expected b/tests/idris2/total006/expected
index a5b6b5f..b92c2bf 100644
--- a/tests/idris2/total006/expected
+++ b/tests/idris2/total006/expected
@@ -1,7 +1,7 @@
 1/1: Building Total (Total.idr)
 Welcome to Idris 2 version 0.0. Enjoy yourself!
 Main> Main.count is total
-Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:770:1--774:1 -> Prelude.map
+Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:810:1--814: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