d7ba624 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Unification tweak for unifying types and metavariable applications

d7ba624Edwin Brady13 years ago

src/Core/Unify.hs+2−1

@@ -337,7 +337,8 @@ unify ctxt env topx topy dont holes =

337 unArgs vs xs ys

338

339 metavarApp tm = let (f, args) = unApply tm in

340+ metavar f &&

340− all (\x -> metavar x) (f : args)

341+ all (\x -> metavarApp x) args

341 && nub args == args

342 && nub args == args

342 metavarArgs tm = let (f, args) = unApply tm in

343 metavarArgs tm = let (f, args) = unApply tm in

343 all (\x -> metavar x || inenv x) args

344 all (\x -> metavar x || inenv x) args

src/Idris/ElabTerm.hs+1−2

@@ -726,8 +726,7 @@ resolveTC depth fn ist

726 [] -> []

727 [args] -> map isImp (snd args) -- won't be overloaded!

728 ps <- get_probs

729− args <- -- try (apply (Var n) imps)

730− (match_apply (Var n) imps)

729+ args <- match_apply (Var n) imps

731 ps' <- get_probs

730 ps' <- get_probs

732 when (length ps < length ps') $ fail "Can't apply type class"

731 when (length ps < length ps') $ fail "Can't apply type class"

733-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

732-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $