Unification tweak for unifying types and metavariable applications
Fixes #507
commitd7ba624beb90db47b221809382cb210254af487d
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 14 Oct 2013, 12:02 (13 years ago)
parentdcc8d46
src/Core/Unify.hs+2−1
@@ -337,7 +337,8 @@ unify ctxt env topx topy dont holes =
337337 unArgs vs xs ys
338338
339339 metavarApp tm = let (f, args) = unApply tm in
340− all (\x -> metavar x) (f : args)
340+ metavar f &&
341+ all (\x -> metavarApp x) args
341342 && nub args == args
342343 metavarArgs tm = let (f, args) = unApply tm in
343344 all (\x -> metavar x || inenv x) args
src/Idris/ElabTerm.hs+1−2
@@ -726,8 +726,7 @@ resolveTC depth fn ist
726726 [] -> []
727727 [args] -> map isImp (snd args) -- won't be overloaded!
728728 ps <- get_probs
729− args <- -- try (apply (Var n) imps)
730− (match_apply (Var n) imps)
729+ args <- match_apply (Var n) imps
731730 ps' <- get_probs
732731 when (length ps < length ps') $ fail "Can't apply type class"
733732-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $