@@ -261,26 +261,27 @@ elab ist info pattern opts fn tm
261261 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
262262 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
263263 elab' ina@(_, a, inty) (PLam n Placeholder sc)
264− = do ptm <- get_term
265− g <- goal
264+ = do -- if n is a type constructor name, this makes no sense...
265+ ctxt <- get_context
266+ when (isTConName n ctxt) $
267+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
266268 checkPiGoal n
267269 attack; intro (Just n);
268270 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
269271 elabE (True, a, inty) sc; solve
270272 elab' ina@(_, a, inty) (PLam n ty sc)
271− = do hsin <- get_holes
272− ptmin <- get_term
273− tyn <- getNameFrom (sMN 0 "lamty")
273+ = do tyn <- getNameFrom (sMN 0 "lamty")
274+ -- if n is a type constructor name, this makes no sense...
275+ ctxt <- get_context
276+ when (isTConName n ctxt) $
277+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
274278 checkPiGoal n
275279 claim tyn RType
276280 explicit tyn
277281 attack
278282 ptm <- get_term
279283 hs <- get_holes
280− -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++
281− -- "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $
282284 introTy (Var tyn) (Just n)
283− -- end_unify
284285 focus tyn
285286 elabE (True, a, True) ty
286287 elabE (True, a, inty) sc