@@ -490,7 +490,15 @@ solve ctxt env (Bind x (Guess ty val) sc)
490 | otherwise = lift $ tfail $ IncompleteTerm val
490 | otherwise = lift $ tfail $ IncompleteTerm val
491solve _ _ h@(Bind x t sc)
491solve _ _ h@(Bind x t sc)
492 = do ps <- get
492 = do ps <- get
493+ case findType x sc of
494+ Just t -> lift $ tfail (CantInferType (show t))
493− fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
495+ _ -> fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
496+ where findType x (Bind n (Let t v) sc)
497+ = findType x v `mplus` findType x sc
498+ findType x (Bind n t sc)
499+ | P _ x' _ <- binderTy t, x == x' = Just n
500+ | otherwise = findType x sc
501+ findType x _ = Nothing
495introTy :: Raw -> Maybe Name -> RunTactic
503introTy :: Raw -> Maybe Name -> RunTactic
496introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
504introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =