@@ -863,7 +863,7 @@ try' t1 t2 proofSearch
863863 ps <- get_probs
864864 ulog <- getUnifyLog
865865 ivs <- get_instances
866− case prunStateT 999999 False ps t1 s of
866+ case prunStateT 999999 False ps Nothing t1 s of
867867 OK ((v, _, _), s') -> do put s'
868868 return $! v
869869 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
@@ -906,8 +906,11 @@ tryWhen False a b = a
906906-- Bool says whether it's okay to create new unification problems. If set
907907-- to False, then the whole tactic fails if there are any new problems
908908tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
909−tryAll [(x, _)] = x
910−tryAll xs = tryAll' [] 999999 xs
909+tryAll = tryAll' True
910+
911+tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a
912+tryAll' _ [(x, _)] = x
913+tryAll' constrok xs = doAll [] 999999 xs
911914 where
912915 cantResolve :: Elab' aux a
913916 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
@@ -915,44 +918,53 @@ tryAll xs = tryAll' [] 999999 xs
915918 noneValid :: Elab' aux a
916919 noneValid = lift $ tfail $ NoValidAlts (map snd xs)
917920
918− tryAll' :: [Elab' aux a] -> -- successes
919− Int -> -- most problems
920− [(Elab' aux a, Name)] -> -- still to try
921− Elab' aux a
922− tryAll' [res] pmax [] = res
923− tryAll' (_:_) pmax [] = cantResolve
924− tryAll' [] pmax [] = noneValid
925− tryAll' cs pmax ((x, msg):xs)
921+ doAll :: [Elab' aux a] -> -- successes
922+ Int -> -- most problems
923+ [(Elab' aux a, Name)] -> -- still to try
924+ Elab' aux a
925+ doAll [res] pmax [] = res
926+ doAll (_:_) pmax [] = cantResolve
927+ doAll [] pmax [] = noneValid
928+ doAll cs pmax ((x, msg):xs)
926929 = do s <- get
927930 ps <- get_probs
928− case prunStateT pmax True ps x s of
931+ ivs <- get_instances
932+ case prunStateT pmax True ps (if constrok then Nothing
933+ else Just ivs) x s of
929934 OK ((v, newps, probs), s') ->
930935 do let cs' = if (newps < pmax)
931936 then [do put s'; return $! v]
932937 else (do put s'; return $! v) : cs
933− tryAll' cs' newps xs
938+ doAll cs' newps xs
934939 Error err -> do put s
935− tryAll' cs pmax xs
940+ doAll cs pmax xs
936941
937−-- Run an elaborator, and fail if any problems are introduced
942+-- Run an elaborator, and fail if any problems or constraints are introduced
938943prunStateT
939944 :: Int
940945 -> Bool
941946 -> [a]
947+ -> Maybe [b] -- constraints left, if we're interested
942948 -> Control.Monad.State.Strict.StateT
943949 (ElabState t) TC t1
944950 -> ElabState t
945951 -> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)
946−prunStateT pmax zok ps x s
952+prunStateT pmax zok ps ivs x s
947953 = case runStateT x s of
948954 OK (v, s'@(ES (p, _) _ _)) ->
949955 let newps = length (problems p) - length ps
956+ ibad = badInstances (instances p) ivs
950957 newpmax = if newps < 0 then 0 else newps in
951958 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
952959 then case reverse (problems p) of
953960 ((_,_,_,_,e,_,_):_) -> Error e
954− else OK ((v, newpmax, problems p), s')
961+ else if ibad
962+ then Error (InternalMsg "Constraint introduced in disambiguation")
963+ else OK ((v, newpmax, problems p), s')
955964 Error e -> Error e
965+ where
966+ badInstances _ Nothing = False
967+ badInstances inow (Just ithen) = length inow > length ithen
956968
957969debugElaborator :: [ErrorReportPart] -> Elab' aux a
958970debugElaborator msg = do ps <- fmap proof get