@@ -293,7 +293,7 @@ elab ist info emode opts fn tm
293293 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
294294 && isTypeConst c
295295 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
296− | pattern && e_nomatching ina
296+ | pattern && not reflection && e_nomatching ina
297297 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
298298 | otherwise = do apply (RConstant c) []; solve
299299 elab' ina fc (PQuote r) = do fill r; solve
@@ -396,7 +396,7 @@ elab ist info emode opts fn tm
396396 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
397397 && isTConName n (tt_ctxt ist)
398398 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
399− | pattern && e_nomatching ec
399+ | pattern && not reflection && e_nomatching ec
400400 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
401401 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
402402 = do let ina = e_inarg ec
@@ -424,7 +424,7 @@ elab ist info emode opts fn tm
424424 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
425425 && isTConName n (tt_ctxt ist)
426426 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
427− | pattern && e_nomatching ina
427+ | pattern && not reflection && e_nomatching ina
428428 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
429429 | otherwise = erun fc $ do apply (Var n) []; solve
430430 elab' ina fc (PLam n Placeholder sc)
@@ -582,7 +582,7 @@ elab ist info emode opts fn tm
582582-- = lift $ tfail (Msg "Typecase is not allowed")
583583 -- if f is local, just do a simple_app
584584 elab' ina _ tm@(PApp fc (PRef _ f) args)
585− | pattern && e_nomatching ina
585+ | pattern && not reflection && e_nomatching ina
586586 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
587587 | otherwise
588588 = do env <- get_env