Add %unbound_implicits directive

This is the same as %auto_implicits in Idris 1, but with a more
appropriate name, because auto implicits are something else.
'%unbound_implicits off' turns off implicit forall bindings. See test
basic033 for an example.

src/Core/Context.idr

@@ -1765,11 +1765,11 @@ lazyActive a
          put Ctxt (record { options->elabDirectives->lazyActive = a } defs)
 
 export
-autoImplicits : {auto c : Ref Ctxt Defs} ->
+setUnboundImplicits : {auto c : Ref Ctxt Defs} ->
                 Bool -> Core ()
-autoImplicits a
+setUnboundImplicits a
     = do defs <- get Ctxt
-         put Ctxt (record { options->elabDirectives->autoImplicits = a } defs)
+         put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
 
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
@@ -1779,11 +1779,11 @@ isLazyActive
          pure (lazyActive (elabDirectives (options defs)))
 
 export
-isAutoImplicits : {auto c : Ref Ctxt Defs} ->
+isUnboundImplicits : {auto c : Ref Ctxt Defs} ->
                   Core Bool
-isAutoImplicits
+isUnboundImplicits
     = do defs <- get Ctxt
-         pure (autoImplicits (elabDirectives (options defs)))
+         pure (unboundImplicits (elabDirectives (options defs)))
 
 export
 setPair : {auto c : Ref Ctxt Defs} ->

src/Core/Options.idr

@@ -83,7 +83,7 @@ public export
 record ElabDirectives where
   constructor MkElabDirectives
   lazyActive : Bool
-  autoImplicits : Bool
+  unboundImplicits : Bool
 
 public export
 record Session where

src/Core/Unify.idr

@@ -1327,5 +1327,3 @@ checkDots
                          _ => do put UST (record { dotConstraints = [] } ust)
                                  throw err)
     checkConstraint _ = pure ()
-
-

src/Idris/Desugar.idr

@@ -708,6 +708,7 @@ mutual
              Hide n => pure [IPragma (\c, nest, env => hide fc n)]
              Logging i => pure [ILog i]
              LazyOn a => pure [IPragma (\c, nest, env => lazyActive a)]
+             UnboundImplicits a => pure [IPragma (\c, nest, env => setUnboundImplicits a)]
              PairNames ty f s => pure [IPragma (\c, nest, env => setPair fc ty f s)]
              RewriteName eq rw => pure [IPragma (\c, nest, env => setRewrite fc eq rw)]
              PrimInteger n => pure [IPragma (\c, nest, env => setFromInteger n)]

src/Idris/Parser.idr

@@ -934,6 +934,10 @@ directive fname indents
          b <- onoff
          atEnd indents
          pure (LazyOn b)
+  <|> do exactIdent "unbound_implicits"
+         b <- onoff
+         atEnd indents
+         pure (UnboundImplicits b)
   <|> do exactIdent "pair"
          ty <- name
          f <- name

src/Idris/Syntax.idr

@@ -150,6 +150,7 @@ mutual
        Hide : Name -> Directive
        Logging : Nat -> Directive
        LazyOn : Bool -> Directive
+       UnboundImplicits : Bool -> Directive
        PairNames : Name -> Name -> Name -> Directive
        RewriteName : Name -> Name -> Directive
        PrimInteger : Name -> Directive

src/TTImp/BindImplicits.idr

@@ -110,7 +110,7 @@ export
 bindNames : {auto c : Ref Ctxt Defs} ->
             (arg : Bool) -> RawImp -> Core (List Name, RawImp)
 bindNames arg tm
-    = if !isAutoImplicits
+    = if !isUnboundImplicits
          then do let ns = nub (findBindableNames arg [] [] tm)
                  pure (map UN (map snd ns), doBind ns tm)
          else pure ([], tm)
@@ -125,7 +125,7 @@ bindTypeNames : {auto c : Ref Ctxt Defs} ->
                 List Name -> RawImp-> Core RawImp
 bindTypeNames uimpls env tm_in
     = let tm = addUsing uimpls tm_in in
-          if !isAutoImplicits
+          if !isUnboundImplicits
              then do let ns = nub (findBindableNames True env [] tm)
                      pure (doBind ns tm)
              else pure tm
@@ -134,7 +134,7 @@ export
 bindTypeNamesUsed : {auto c : Ref Ctxt Defs} ->
                     List String -> List Name -> RawImp -> Core RawImp
 bindTypeNamesUsed used env tm
-    = if !isAutoImplicits
+    = if !isUnboundImplicits
          then do let ns = nub (findBindableNames True env used tm)
                  pure (doBind ns tm)
          else pure tm

src/TTImp/ProcessDef.idr

@@ -218,10 +218,10 @@ checkLHS : {vars : _} ->
 checkLHS {vars} mult hashit n opts nest env fc lhs_in
     = do defs <- get Ctxt
          lhs_raw <- lhsInCurrentNS nest lhs_in
-         autoimp <- isAutoImplicits
-         autoImplicits True
+         autoimp <- isUnboundImplicits
+         setUnboundImplicits True
          (_, lhs_bound) <- bindNames False lhs_raw
-         autoImplicits autoimp
+         setUnboundImplicits autoimp
          lhs <- implicitsAs defs vars lhs_bound
 
          log 5 $ "Checking LHS of " ++ show !(getFullName (Resolved n)) ++
@@ -334,10 +334,10 @@ checkClause : {vars : _} ->
 checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
     = do lhs_raw <- lhsInCurrentNS nest lhs
          handleUnify
-           (do autoimp <- isAutoImplicits
-               autoImplicits True
+           (do autoimp <- isUnboundImplicits
+               setUnboundImplicits True
                (_, lhs) <- bindNames False lhs_raw
-               autoImplicits autoimp
+               setUnboundImplicits autoimp
 
                log 5 $ "Checking " ++ show lhs
                logEnv 5 "In env" env

src/TTImp/WithClause.idr

@@ -107,11 +107,11 @@ getNewLHS : {auto c : Ref Ctxt Defs} ->
             RawImp -> RawImp -> Core RawImp
 getNewLHS ploc drop nest wname wargnames lhs_raw patlhs
     = do (mlhs_raw, wrest) <- dropWithArgs drop patlhs
-         autoimp <- isAutoImplicits
-         autoImplicits True
+         autoimp <- isUnboundImplicits
+         setUnboundImplicits True
          (_, lhs) <- bindNames False lhs_raw
          (_, mlhs) <- bindNames False mlhs_raw
-         autoImplicits autoimp
+         setUnboundImplicits autoimp
 
          let (warg :: rest) = reverse wrest
              | _ => throw (GenericMsg ploc "Badly formed 'with' clause")

tests/Main.idr

@@ -29,7 +29,7 @@ idrisTests
        "basic016", "basic017", "basic018", "basic019", "basic020",
        "basic021", "basic022", "basic023", "basic024", "basic025",
        "basic026", "basic027", "basic028", "basic029", "basic030",
-       "basic031", "basic032",
+       "basic031", "basic032", "basic033",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",

tests/idris2/basic033/expected

@@ -0,0 +1,5 @@
+1/1: Building unboundimps (unboundimps.idr)
+unboundimps.idr:18:11--18:14:While processing type of Main.len' at unboundimps.idr:18:1--19:1:
+Undefined name xs
+unboundimps.idr:19:16--19:18:While processing type of Main.append' at unboundimps.idr:19:1--21:1:
+Undefined name n

tests/idris2/basic033/run

@@ -0,0 +1,3 @@
+$1 --check unboundimps.idr
+
+rm -rf build

tests/idris2/basic033/unboundimps.idr

@@ -0,0 +1,20 @@
+import Data.Vect
+
+%unbound_implicits off
+
+append : forall n, m, a . Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys 
+append (x :: xs) ys = x :: append xs ys
+
+data Env : forall n . Vect n Type -> Type where
+     ENil : Env []
+     ECons : forall t, ts . t -> Env ts -> Env (t :: ts)
+
+-- fine because the only name used in bound, and it'll infer types for
+-- xs and its indices
+len : forall xs . Env xs -> Nat
+
+-- neither of these are fine
+len': Env xs -> Nat
+append' : Vect n a -> Vect m a -> Vect (n + m) a
+