Add implicit lambdas for top level implicits

They shouldn't really be treated differently from scoped implicits
during elaboration... Fixes #1536

Makefile

@@ -43,7 +43,7 @@ relib: lib_clean
 	$(CABAL) install $(CABALFLAGS)
 
 linecount:
-	wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs
+	wc -l src/Idris/*.hs src/Idris/Elab/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs src/Util/*.hs
 
 #Note: this doesn't yet link to Hackage properly
 doc: dist/setup-config

src/Idris/AbsSyntax.hs

@@ -1393,7 +1393,11 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
             = (n, (p, t)) : collectImps sc
         collectImps _ = []
 
-        getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps
+        scopedimpl (Just i) = not (toplevel_imp i)
+        scopedimpl _ = False
+
+        getImps (Bind n (Pi i _ _) sc) imps 
+             | scopedimpl i = getImps sc imps
         getImps (Bind n (Pi _ t _) sc) imps
             | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
          where
@@ -1556,9 +1560,9 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
     pibind using []     sc = sc
     pibind using (n:ns) sc
       = case lookup n using of
-            Just ty -> PPi (Imp [] Dynamic False Nothing)
+            Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))
                            n NoFC ty (pibind using ns sc)
-            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)
+            Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))
                            n NoFC Placeholder (pibind using ns sc)
 
 -- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs

@@ -587,9 +587,9 @@ is_scoped :: Plicity -> Maybe ImplicitInfo
 is_scoped (Imp _ _ _ s) = s
 is_scoped _ = Nothing
 
-impl = Imp [] Dynamic False Nothing
-forall_imp = Imp [] Dynamic False (Just (Impl False))
-forall_constraint = Imp [] Dynamic False (Just (Impl True))
+impl = Imp [] Dynamic False (Just (Impl False True))
+forall_imp = Imp [] Dynamic False (Just (Impl False False))
+forall_constraint = Imp [] Dynamic False (Just (Impl True False))
 expl = Exp [] Dynamic False
 expl_param = Exp [] Dynamic True
 constraint = Constraint [] Static

src/Idris/Core/Binary.hs

@@ -484,10 +484,11 @@ instance Binary Raw where
 instance Binary ImplicitInfo where
         put x
           = case x of
-                Impl x1 -> put x1
+                Impl x1 x2 -> do put x1; put x2
         get
           = do x1 <- get
-               return (Impl x1)
+               x2 <- get
+               return (Impl x1 x2)
 
 instance (Binary b) => Binary (Binder b) where
         put x

src/Idris/Core/DeepSeq.hs

@@ -167,7 +167,7 @@ instance NFData ErrorReportPart where
   rnf (SubReport x1) = rnf x1 `seq` ()
 
 instance NFData ImplicitInfo where
-        rnf (Impl x1) = rnf x1 `seq` ()
+        rnf (Impl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
 
 instance (NFData b) => NFData (Binder b) where
         rnf (Lam x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs

@@ -811,7 +811,7 @@ deriving instance Binary Raw
 deriving instance NFData Raw
 !-}
 
-data ImplicitInfo = Impl { tcinstance :: Bool }
+data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool }
   deriving (Show, Eq, Ord, Data, Typeable)
 
 {-!

src/Idris/Delaborate.hs

@@ -110,6 +110,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
                                   _ -> PRef un [] n
     de env _ (Bind n (Lam ty) sc)
           = 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)
     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)

src/Idris/Elab/Term.hs

@@ -1415,9 +1415,9 @@ elab ist info emode opts fn tm
     notImplicitable _ = False
 
     insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
-      | tcinstance i
+      | tcinstance i && not (toplevel_imp i)
           = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
-      | otherwise
+      | not (toplevel_imp i)
           = pimp n Placeholder True : insertScopedImps fc sc xs
     insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
         = x : insertScopedImps fc sc xs

src/Idris/IBC.hs

@@ -40,7 +40,7 @@ import System.Directory
 import Codec.Archive.Zip
 
 ibcVersion :: Word16
-ibcVersion = 126
+ibcVersion = 127
 
 data IBCFile = IBCFile { ver :: Word16,
                          sourcefile :: FilePath,

src/Idris/ParseExpr.hs

@@ -1051,10 +1051,10 @@ normalImplicit opts st syn = do
    sc <- expr syn
    let (im,cl)
           = if implicitAllowed syn
-               then (Imp opts st False Nothing,
+               then (Imp opts st False (Just (Impl False True)),
                       constraint)
-               else (Imp opts st False (Just (Impl False)),
-                     Imp opts st False (Just (Impl True)))
+               else (Imp opts st False (Just (Impl False False)),
+                     Imp opts st False (Just (Impl True False)))
    return (bindList (PPi im) xt 
            (bindList (PPi cl) cs sc))
 

src/Idris/REPL.hs

@@ -1059,6 +1059,8 @@ process fn (DebugInfo n)
         when (not (null si)) $ iputStrLn (show si)
         let di = lookupCtxt n (idris_datatypes i)
         when (not (null di)) $ iputStrLn (show di)
+        let imps = lookupCtxt n (idris_implicits i)
+        when (not (null imps)) $ iputStrLn (show imps)
         let d = lookupDef n (tt_ctxt i)
         when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
         let cg = lookupCtxtName n (idris_callgraph i)