@@ -309,7 +309,7 @@ elab ist info emode opts fn tm
309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
310 && isTypeConst c
310 && isTypeConst c
311 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
311 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
312− | pattern && not reflection && e_nomatching ina
312+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
314 | otherwise = do apply (RConstant c) []; solve
314 | otherwise = do apply (RConstant c) []; solve
315 elab' ina fc (PQuote r) = do fill r; solve
315 elab' ina fc (PQuote r) = do fill r; solve
@@ -433,7 +433,7 @@ elab ist info emode opts fn tm
433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
434 && isTConName n (tt_ctxt ist)
434 && isTConName n (tt_ctxt ist)
435 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
435 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
436− | pattern && not reflection && e_nomatching ec
436+ | pattern && not reflection && not (e_qq ec) && e_nomatching ec
437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
439 = do let ina = e_inarg ec
439 = do let ina = e_inarg ec
@@ -461,7 +461,7 @@ elab ist info emode opts fn tm
461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
462 && isTConName n (tt_ctxt ist)
462 && isTConName n (tt_ctxt ist)
463 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
463 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
464− | pattern && not reflection && e_nomatching ina
464+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
466 | otherwise =
466 | otherwise =
467 do fty <- get_type (Var n) -- check for implicits
467 do fty <- get_type (Var n) -- check for implicits
@@ -622,7 +622,7 @@ elab ist info emode opts fn tm
622 -- if f is local, just do a simple_app
622 -- if f is local, just do a simple_app
623 -- FIXME: Anyone feel like refactoring this mess? - EB
623 -- FIXME: Anyone feel like refactoring this mess? - EB
624 elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
624 elab' ina topfc tm@(PApp fc (PRef _ f) args_in)
625− | pattern && not reflection && e_nomatching ina
625+ | pattern && not reflection && not (e_qq ina) && e_nomatching ina
626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
627 | otherwise = implicitApp $
627 | otherwise = implicitApp $
628 do env <- get_env
628 do env <- get_env