@@ -309,7 +309,7 @@ elab ist info emode opts fn tm
309309 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
310310 && isTypeConst c
311311 = 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
313313 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
314314 | otherwise = do apply (RConstant c) []; solve
315315 elab' ina fc (PQuote r) = do fill r; solve
@@ -433,7 +433,7 @@ elab ist info emode opts fn tm
433433 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
434434 && isTConName n (tt_ctxt ist)
435435 = 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
437437 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
438438 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
439439 = do let ina = e_inarg ec
@@ -461,7 +461,7 @@ elab ist info emode opts fn tm
461461 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
462462 && isTConName n (tt_ctxt ist)
463463 = 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
465465 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
466466 | otherwise =
467467 do fty <- get_type (Var n) -- check for implicits
@@ -622,7 +622,7 @@ elab ist info emode opts fn tm
622622 -- if f is local, just do a simple_app
623623 -- FIXME: Anyone feel like refactoring this mess? - EB
624624 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
626626 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
627627 | otherwise = implicitApp $
628628 do env <- get_env