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