Type class resolution shouldn't use match_apply
This can resolve things too early which shouldn't be resolved. We only
had match_apply as a workaround for some earlier bugs...
commit81e19625f2ce040d653848368073ac5ad2a15b6e
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 26 Aug 2015, 10:38 (11 years ago)
parent93761d5
src/Idris/ProofSearch.hs+1−2
@@ -468,8 +468,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist
468468 xs -> error "The impossible happened - overloading is not expected here!"
469469 ps <- get_probs
470470 tm <- get_term
471− args <- map snd <$> try' (apply (Var n) imps)
472− (match_apply (Var n) imps) True
471+ args <- map snd <$> apply (Var n) imps
473472 solven lams -- close any implicit lambdas we introduced
474473 ps' <- get_probs
475474 when (length ps < length ps' || unrecoverable ps') $