Reorganise implicit binding

This should be done at the surface language level only, not during
elaboration. This fixes #107

src/Idris/Desugar.idr

@@ -160,8 +160,9 @@ mutual
                         (Implicit fc False)
                         !(traverse (desugarClause ps True) xs)
   desugarB side ps (PLocal fc xs scope)
-      = pure $ ILocal fc (concat !(traverse (desugarDecl ps) xs))
-                         !(desugar side (definedIn xs ++ ps) scope)
+      = let ps' = definedIn xs ++ ps in
+            pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
+                             !(desugar side ps' scope)
   desugarB side ps (PApp pfc (PUpdate fc fs) rec)
       = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
                            !(desugarB side ps rec)

src/TTImp/ProcessData.idr

@@ -65,7 +65,6 @@ checkCon : {vars : _} ->
            ImpTy -> Core Constructor
 checkCon {vars} opts nest env vis tn (MkImpTy fc cn_in ty_raw)
     = do cn <- inCurrentNS cn_in
-         ty_raw <- bindTypeNames [] vars ty_raw
 
          defs <- get Ctxt
          -- Check 'cn' is undefined

src/TTImp/ProcessDecls.idr

@@ -8,6 +8,7 @@ import Core.UnifyState
 
 import Parser.Support
 
+import TTImp.BindImplicits
 import TTImp.Elab.Check
 import TTImp.Parser
 import TTImp.ProcessData
@@ -65,6 +66,40 @@ processDecls nest env decls
     = do traverse_ (processDecl [] nest env) decls
          pure True -- TODO: False on error
 
+processTTImpDecls : {vars : _} ->
+                    {auto c : Ref Ctxt Defs} ->
+                    {auto m : Ref MD Metadata} ->
+                    {auto u : Ref UST UState} ->
+                    NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool
+processTTImpDecls {vars} nest env decls
+    = do traverse_ (\d => do d' <- bindNames d
+                             processDecl [] nest env d') decls
+         pure True -- TODO: False on error
+  where
+    bindConNames : ImpTy -> Core ImpTy
+    bindConNames (MkImpTy fc n ty)
+        = do ty' <- bindTypeNames [] vars ty
+             pure (MkImpTy fc n ty')
+
+    bindDataNames : ImpData -> Core ImpData
+    bindDataNames (MkImpData fc n t opts cons)
+        = do t' <- bindTypeNames [] vars t
+             cons' <- traverse bindConNames cons
+             pure (MkImpData fc n t' opts cons')
+    bindDataNames (MkImpLater fc n t)
+        = do t' <- bindTypeNames [] vars t
+             pure (MkImpLater fc n t')
+
+    -- bind implicits to make raw TTImp source a bit friendlier
+    bindNames : ImpDecl -> Core ImpDecl
+    bindNames (IClaim fc c vis opts (MkImpTy tfc n ty))
+        = do ty' <- bindTypeNames [] vars ty
+             pure (IClaim fc c vis opts (MkImpTy tfc n ty'))
+    bindNames (IData fc vis d)
+        = do d' <- bindDataNames d
+             pure (IData fc vis d')
+    bindNames d = pure d
+
 export
 processTTImpFile : {auto c : Ref Ctxt Defs} ->
                    {auto m : Ref MD Metadata} ->
@@ -78,7 +113,7 @@ processTTImpFile fname
                | Left err => do coreLift (putStrLn (show err))
                                 pure False
          logTime "Elaboration" $
-            catch (do processDecls (MkNested []) [] tti
+            catch (do processTTImpDecls (MkNested []) [] tti
                       Nothing <- checkDelayedHoles
                           | Just err => throw err
                       pure True)

src/TTImp/ProcessType.idr

@@ -103,7 +103,6 @@ processType : {vars : _} ->
               List FnOpt -> ImpTy -> Core ()
 processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
     = do n <- inCurrentNS n_in
-         ty_raw <- bindTypeNames [] vars ty_raw
 
          log 1 $ "Processing " ++ show n
          log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw