Fix issue #2666 ("with" patterns accepted outside of "with" block)

Parser parses clauses independently so there is no parsing error
in code like this:

    foo : Int -> Bool
    foo 1 | 2 | 3 = True
    foo _ = False

Elaborator can check if it sees with patterns but no enclosing with block,
so we report error in situations like this.

src/Idris/Elab/Clause.hs

@@ -551,6 +551,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         -- pattern bindings
         i <- getIState
         inf <- isTyInferred fname
+
+        -- Check if we have "with" patterns outside of "with" block
+        when (isOutsideWith lhs_in && (not $ null withs)) $
+            ierror $ (At fc (Elaborating "left hand side of " fname Nothing
+                             (Msg "unexpected patterns outside of \"with\" block")))
+
         -- get the parameters first, to pass through to any where block
         let fn_ty = case lookupTy fname (tt_ctxt i) of
                          [t] -> t
@@ -803,6 +809,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         isArg' _ = False
     isArg _ _ = False
 
+    -- term is not within "with" block
+    isOutsideWith :: PTerm -> Bool
+    isOutsideWith (PApp _ (PRef _ _ (SN (WithN _ _))) _) = False
+    isOutsideWith _ = True
+
 elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
    = do let tcgen = Dictionary `elem` opts
         ctxt <- getContext

test/error006/WithPatsNoWith.idr

@@ -0,0 +1,6 @@
+module WithPatsNoWith
+
+foo : Int -> Bool
+foo 1 | 2 | 3 = True
+foo _ = False
+

test/error006/expected

@@ -0,0 +1,2 @@
+WithPatsNoWith.idr:4:5:When checking left hand side of foo:
+unexpected patterns outside of "with" block

test/error006/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --consolewidth 80 $@ --check --nocolour WithPatsNoWith.idr
+rm -f *.ibc