Display binder if it's not implicitly bindable

This is particularly important if we're generating something that needs
to be parsed and checked again. Fixes #185

src/Idris/Resugar.idr

@@ -8,6 +8,7 @@ import Idris.Syntax
 
 import TTImp.TTImp
 import TTImp.Unelab
+import TTImp.Utils
 
 import Data.List
 import Data.Maybe
@@ -161,10 +162,21 @@ mutual
   toPTerm p (IPi fc rig Implicit n arg ret)
       = do imp <- showImplicits
            if imp
-              then do arg' <- toPTerm appPrec arg
+              then do arg' <- toPTerm tyPrec arg
                       ret' <- toPTerm tyPrec ret
                       bracket p tyPrec (PPi fc rig Implicit n arg' ret')
-              else toPTerm p ret
+              else if needsBind n
+                      then do arg' <- toPTerm tyPrec arg
+                              ret' <- toPTerm tyPrec ret
+                              bracket p tyPrec (PPi fc rig Implicit n arg' ret')
+                      else toPTerm p ret
+    where
+      needsBind : Maybe Name -> Bool
+      needsBind (Just (UN t))
+          = let ns = findBindableNames False [] [] ret
+                allNs = findAllNames [] ret in
+                ((UN t) `elem` allNs) && not (t `elem` (map Builtin.fst ns))
+      needsBind _ = False
   toPTerm p (IPi fc rig pt n arg ret)
       = do arg' <- toPTerm appPrec arg
            ret' <- toPTerm tyPrec ret

src/TTImp/Utils.idr

@@ -30,13 +30,13 @@ findBindableNames arg env used (IPi fc rig p mn aty retty)
     = let env' = case mn of
                       Nothing => env
                       Just n => n :: env in
-          findBindableNames True env' used aty ++
+          findBindableNames True env used aty ++
           findBindableNames True env' used retty
 findBindableNames arg env used (ILam fc rig p mn aty sc)
     = let env' = case mn of
                       Nothing => env
                       Just n => n :: env in
-      findBindableNames True env' used aty ++
+      findBindableNames True env used aty ++
       findBindableNames True env' used sc
 findBindableNames arg env used (IApp fc fn av)
     = findBindableNames False env used fn ++ findBindableNames True env used av
@@ -66,6 +66,48 @@ findBindableNames arg env used (IAlternative fc u alts)
 -- name should be bound, leave it to the programmer
 findBindableNames arg env used tm = []
 
+export
+findAllNames : (env : List Name) -> RawImp -> List Name
+findAllNames env (IVar fc n)
+    = if not (n `elem` env) then [n] else []
+findAllNames env (IPi fc rig p mn aty retty)
+    = let env' = case mn of
+                      Nothing => env
+                      Just n => n :: env in
+          findAllNames env aty ++ findAllNames env' retty
+findAllNames env (ILam fc rig p mn aty sc)
+    = let env' = case mn of
+                      Nothing => env
+                      Just n => n :: env in
+      findAllNames env' aty ++ findAllNames env' sc
+findAllNames env (IApp fc fn av)
+    = findAllNames env fn ++ findAllNames env av
+findAllNames env (IImplicitApp fc fn n av)
+    = findAllNames env fn ++ findAllNames env av
+findAllNames env (IWithApp fc fn av)
+    = findAllNames env fn ++ findAllNames env av
+findAllNames env (IAs fc _ n pat)
+    = n :: findAllNames env pat
+findAllNames env (IAs fc _ n pat)
+    = findAllNames env pat
+findAllNames env (IMustUnify fc r pat)
+    = findAllNames env pat
+findAllNames env (IDelayed fc r t)
+    = findAllNames env t
+findAllNames env (IDelay fc t)
+    = findAllNames env t
+findAllNames env (IForce fc t)
+    = findAllNames env t
+findAllNames env (IQuote fc t)
+    = findAllNames env t
+findAllNames env (IUnquote fc t)
+    = findAllNames env t
+findAllNames env (IAlternative fc u alts)
+    = concatMap (findAllNames env) alts
+-- We've skipped case, let and local - rather than guess where the
+-- name should be bound, leave it to the programmer
+findAllNames env tm = []
+
 -- Find the names in a type that affect the 'using' declarations (i.e. 
 -- the ones that mean the declaration will be added).
 export

tests/Main.idr

@@ -97,7 +97,7 @@ idrisTests
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
-       "reg022", "reg023", "reg024",
+       "reg022", "reg023", "reg024", "reg025",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",

tests/idris2/reg024/expected

@@ -6,5 +6,4 @@ notLtz (BLT_OE x) impossible
 notLtz BLT_OE_Eq impossible
 notLtz (BLT_EO x) impossible
 notLtz (BLT_EE x) impossible
-Main> 
-Bye for now!
+Main> Bye for now!

tests/idris2/reg024/input

@@ -1 +1,2 @@
 :cs 13 8 x
+:q

tests/idris2/reg025/expected

@@ -0,0 +1,4 @@
+1/1: Building lift (lift.idr)
+Main> pbz_hole : {0 p : BNat -> Type} -> ((bn : BNat) -> p bn -> p (E bn)) -> ((bn : BNat) -> p bn -> p (O bn)) -> p BZ -> p BZ
+pbz_hole pe po pbz
+Main> Bye for now!

tests/idris2/reg025/input

@@ -0,0 +1,2 @@
+:ml 11 pbz_hole
+:q

tests/idris2/reg025/lift.idr

@@ -0,0 +1,13 @@
+data BNat = BZ | O BNat | E BNat
+
+bnat_ind : {0 p : BNat -> Type}
+        -> p BZ
+        -> ((bn : BNat) -> p bn -> p (O bn))
+        -> ((bn : BNat) -> p bn -> p (E bn))
+        -> (bn : BNat) -> p bn
+bnat_ind pbz po pe = go
+ where
+  go : (bn : BNat) -> p bn
+  go BZ = ?pbz_hole
+  go (O x) = po x (go x)
+  go (E x) = pe x (go x)

tests/idris2/reg025/run

@@ -0,0 +1,3 @@
+$1 --no-banner lift.idr < input
+
+rm -rf build