@@ -366,6 +366,9 @@ elab ist info emode opts fn tm
366366-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
367367-- = lift $ tfail (Msg "Typecase is not allowed")
368368 elab' ec _ (PRef fc n)
369+ | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
370+ && isTConName n (tt_ctxt ist)
371+ = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
369372 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
370373 = do let ina = e_inarg ec
371374 guarded = e_guarded ec