Only apply unique implicit conversions (and add test)

src/Core/Elaborate.hs

@@ -45,10 +45,9 @@ proof (ES (p, _) _ _) = p
 proofFail :: Elab' aux a -> Elab' aux a
 proofFail e = do s <- get
                  case runStateT e s of
-                      OK (a, s') -> trace ("OK ACTUALLY") $
-                                     do put s'
-                                        return a
-                      Error err -> trace "BAD" $ lift $ Error (ProofSearchFail err)
+                      OK (a, s') -> do put s'
+                                       return a
+                      Error err -> lift $ Error (ProofSearchFail err)
 
 saveState :: Elab' aux ()
 saveState = do e@(ES p s _) <- get
@@ -65,6 +64,8 @@ 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)
 
@@ -528,7 +529,7 @@ try' t1 t2 proofSearch
   where recoverableErr err@(CantUnify r _ _ _ _ _) 
              = -- traceWhen r (show err) $
                r || proofSearch
-        recoverableErr (ProofSearchFail _) = trace "FAILED" $ False
+        recoverableErr (ProofSearchFail _) = False
         recoverableErr _ = True
 
 tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

src/Idris/ElabTerm.hs

@@ -453,8 +453,8 @@ elab ist info pattern tcgen fn tm
            let t' = case (t, cs) of
                          (PCoerced tm, _) -> tm
                          (_, []) -> t
-                         (_, cs) -> PAlternative False 
-                                       (t : map (mkCoerce t) cs)
+                         (_, cs) -> PAlternative False [t ,
+                                       PAlternative True (map (mkCoerce t) cs)]
            return t'
        where 
          mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!

test/README

@@ -18,5 +18,7 @@ Tests:
 016: codata
 017: mutually recursive totality checking
 018: Message passing concurrency (raw form)
+019: magic with
+020: implicit conversions
 
 regxxx: various regression tests

test/test020/expected

@@ -0,0 +1,6 @@
+test020a.idr:16:Can't unify Vect a n with List a
+
+Specifically:
+	Can't unify Vect a n with List a
+[3, 2, 1]
+Number 42

test/test020/run

@@ -0,0 +1,5 @@
+#!/bin/bash
+idris $@ test020.idr -o test020
+idris $@ test020a.idr --check
+./test020
+rm -f test020 *.ibc

test/test020/test020.idr

@@ -0,0 +1,25 @@
+module Main
+
+implicit 
+natInt : Nat -> Int
+natInt x = cast x
+
+implicit 
+forget : Vect a n -> List a
+forget [] = []
+forget (x :: xs) = x :: forget xs
+
+foo : Vect a n -> List a
+foo xs = reverse xs
+
+implicit intString : Int -> String
+intString = show
+
+test : Int -> String
+test x = "Number " ++ x
+
+main : IO ()
+main = do print (foo [1,2,3])
+          print (test 42)
+
+

test/test020/test020a.idr

@@ -0,0 +1,19 @@
+module Main
+
+implicit 
+forget : Vect a n -> List a
+forget [] = []
+forget (x :: xs) = x :: forget xs
+
+implicit
+forget' : Vect a n -> List a
+forget' [] = []
+forget' (x :: xs) = forget xs
+
+foo : Vect a n -> List a
+foo xs = reverse xs
+
+main : IO ()
+main = print (foo [1,2,3])
+
+