0a1965e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change 'Not a guess' error

On further investigation, every time this is encountered it means that there are still holes in a subterm, so the appropriate error is "Incomplete Term".

commit0a1965e2f3fba70f6db3e51388e558fb24644eab authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 11:00 (12 years ago) parent82753c9

1 file changed+3−3

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+3−3

src/Idris/Core/ProofState.hs+3−3

@@ -558,7 +558,7 @@ solve _ _ h@(Bind x t sc)

558558 = do ps <- get

559559 case findType x sc of

560560 Just t -> lift $ tfail (CantInferType (show t))

561− _ -> fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

561+ _ -> lift $ tfail (IncompleteTerm h)

562562 where findType x (Bind n (Let t v) sc)

563563 = findType x v `mplus` findType x sc

564564 findType x (Bind n t sc)

@@ -859,8 +859,8 @@ mergeNotunified env ns = mnu ns [] [] where

859859 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

860860 mnu ((n, t):ns) ns_acc ps_acc

861861 | Just t' <- lookup n ns, t /= t'

862− = mnu ns ((n,t') : ns_acc)

863− ((t,t',env,Msg "", [],Unify) : ps_acc)

862+ = mnu ns ((n,t') : ns_acc)

863+ ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

864864 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

865865

866866updateNotunified [] nu = nu