diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index 14aece68d..c53dcca8e 100644 --- a/src/Idris/Elab/Clause.hs +++ b/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 diff --git a/test/error006/WithPatsNoWith.idr b/test/error006/WithPatsNoWith.idr new file mode 100644 index 000000000..9e0cf8749 --- /dev/null +++ b/test/error006/WithPatsNoWith.idr @@ -0,0 +1,6 @@ +module WithPatsNoWith + +foo : Int -> Bool +foo 1 | 2 | 3 = True +foo _ = False + diff --git a/test/error006/expected b/test/error006/expected new file mode 100644 index 000000000..c225f50e2 --- /dev/null +++ b/test/error006/expected @@ -0,0 +1,2 @@ +WithPatsNoWith.idr:4:5:When checking left hand side of foo: +unexpected patterns outside of "with" block diff --git a/test/error006/run b/test/error006/run new file mode 100755 index 000000000..efcae4972 --- /dev/null +++ b/test/error006/run @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +idris --consolewidth 80 $@ --check --nocolour WithPatsNoWith.idr +rm -f *.ibc