2f5c756 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better error message for 'Not a guess'

At least in a case where we can tell what's caused it! Specifically, when there is a missing solution for a type in a binder. Fixes #708

commit2f5c7568e8bf19c1afd16bbd1cdd509307878ec5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 23 Dec 2013, 13:09 (13 years ago) parent8ac3356

1 file changed+9−1

unifiedsplit

src/Idris/Core/ProofState.hs+9−1

@@ -490,7 +490,15 @@ solve ctxt env (Bind x (Guess ty val) sc)

490490 | otherwise = lift $ tfail $ IncompleteTerm val

491491solve _ _ h@(Bind x t sc)

492492 = do ps <- get

493− fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

493+ case findType x sc of

494+ Just t -> lift $ tfail (CantInferType (show t))

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

494502

495503introTy :: Raw -> Maybe Name -> RunTactic

496504introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =