@@ -293,7 +293,7 @@ elab ist info emode opts fn tm
293 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
293 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
294 && isTypeConst c
294 && isTypeConst c
295 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
295 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
296− | pattern && e_nomatching ina
296+ | pattern && not reflection && e_nomatching ina
297 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
297 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
298 | otherwise = do apply (RConstant c) []; solve
298 | otherwise = do apply (RConstant c) []; solve
299 elab' ina fc (PQuote r) = do fill r; solve
299 elab' ina fc (PQuote r) = do fill r; solve
@@ -396,7 +396,7 @@ elab ist info emode opts fn tm
396 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
396 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
397 && isTConName n (tt_ctxt ist)
397 && isTConName n (tt_ctxt ist)
398 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
398 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
399− | pattern && e_nomatching ec
399+ | pattern && not reflection && e_nomatching ec
400 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
400 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
401 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
401 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
402 = do let ina = e_inarg ec
402 = do let ina = e_inarg ec
@@ -424,7 +424,7 @@ elab ist info emode opts fn tm
424 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
424 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
425 && isTConName n (tt_ctxt ist)
425 && isTConName n (tt_ctxt ist)
426 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
426 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
427− | pattern && e_nomatching ina
427+ | pattern && not reflection && e_nomatching ina
428 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
428 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
429 | otherwise = erun fc $ do apply (Var n) []; solve
429 | otherwise = erun fc $ do apply (Var n) []; solve
430 elab' ina fc (PLam n Placeholder sc)
430 elab' ina fc (PLam n Placeholder sc)
@@ -582,7 +582,7 @@ elab ist info emode opts fn tm
582-- = lift $ tfail (Msg "Typecase is not allowed")
582-- = lift $ tfail (Msg "Typecase is not allowed")
583 -- if f is local, just do a simple_app
583 -- if f is local, just do a simple_app
584 elab' ina _ tm@(PApp fc (PRef _ f) args)
584 elab' ina _ tm@(PApp fc (PRef _ f) args)
585− | pattern && e_nomatching ina
585+ | pattern && not reflection && e_nomatching ina
586 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
586 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
587 | otherwise
587 | otherwise
588 = do env <- get_env
588 = do env <- get_env