@@ -261,26 +261,27 @@ elab ist info pattern opts fn tm
261 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
261 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
262 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
262 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
263 elab' ina@(_, a, inty) (PLam n Placeholder sc)
263 elab' ina@(_, a, inty) (PLam n Placeholder sc)
264− = do ptm <- get_term
264+ = do -- if n is a type constructor name, this makes no sense...
265− g <- goal
265+ ctxt <- get_context
266+ when (isTConName n ctxt) $
267+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
266 checkPiGoal n
268 checkPiGoal n
267 attack; intro (Just n);
269 attack; intro (Just n);
268 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
270 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
269 elabE (True, a, inty) sc; solve
271 elabE (True, a, inty) sc; solve
270 elab' ina@(_, a, inty) (PLam n ty sc)
272 elab' ina@(_, a, inty) (PLam n ty sc)
271− = do hsin <- get_holes
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...
276+ when (isTConName n ctxt) $
277+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
274 checkPiGoal n
278 checkPiGoal n
275 claim tyn RType
279 claim tyn RType
276 explicit tyn
280 explicit tyn
278 ptm <- get_term
282 ptm <- get_term
279 hs <- get_holes
283 hs <- get_holes
280− -- trace ("BEFORE:\n" ++ show hsin ++ "\n" ++ show ptmin ++
281− -- "\nNOW:\n" ++ show hs ++ "\n" ++ show ptm) $
282 introTy (Var tyn) (Just n)
284 introTy (Var tyn) (Just n)
284 focus tyn
285 focus tyn
285 elabE (True, a, True) ty
286 elabE (True, a, True) ty
286 elabE (True, a, inty) sc
287 elabE (True, a, inty) sc