on master help sign in
Change 'Not a guess' error
0a1965eEdwin Brady
src/Idris/Core/ProofState.hs+3−3
@@ -558,7 +558,7 @@ solve _ _ h@(Bind x t sc)
558 = do ps <- get
558 = do ps <- get
559 case findType x sc of
559 case findType x sc of
560 Just t -> lift $ tfail (CantInferType (show t))
560 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)
562 where findType x (Bind n (Let t v) sc)
562 where findType x (Bind n (Let t v) sc)
563 = findType x v `mplus` findType x sc
563 = findType x v `mplus` findType x sc
564 findType x (Bind n t sc)
564 findType x (Bind n t sc)
@@ -859,8 +859,8 @@ mergeNotunified env ns = mnu ns [] [] where
859 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
859 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
860 mnu ((n, t):ns) ns_acc ps_acc
860 mnu ((n, t):ns) ns_acc ps_acc
861 | Just t' <- lookup n ns, t /= t'
861 | Just t' <- lookup n ns, t /= t'
862− = mnu ns ((n,t') : ns_acc)
862+ = mnu ns ((n,t') : ns_acc)
863− ((t,t',env,Msg "", [],Unify) : ps_acc)
863+ ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)
864 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
864 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
865
865
866updateNotunified [] nu = nu
866updateNotunified [] nu = nu