dcc8d46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make more type classes resolve, by matching rather than unification

dcc8d46Edwin Brady13 years ago

src/Core/Unify.hs+20−3

compare with master

unifiedsplit

@@ -34,7 +34,7 @@ data UResult a = UOK a

34match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

35 TC [(Name, TT Name)]

36match_unify ctxt env topx topy dont holes =

37−-- trace ("Matching " ++ show (topx, topy)) $

37+-- trace ("Matching " ++ show (topx, topy)) $

38 case runStateT (un [] topx topy) (UI 0 []) of

39 OK (v, UI _ []) -> return (filter notTrivial v)

40 res ->

@@ -56,6 +56,10 @@ match_unify ctxt env topx topy dont holes =

56 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

57 un bnames (P _ x _) (V i)

58 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

59+ un bnames (Bind x bx sx) (Bind y by sy)

60+ = do h1 <- uB bnames bx by

61+ h2 <- un ((x, y) : bnames) sx sy

62+ combine bnames h1 h2

59 un names (App fx ax) (App fy ay)

63 un names (App fx ax) (App fy ay)

60 = do hf <- un names fx fy

64 = do hf <- un names fx fy

61 ha <- un names ax ay

65 ha <- un names ax ay

@@ -71,6 +75,19 @@ match_unify ctxt env topx topy dont holes =

71 lift $ tfail err

75 lift $ tfail err

78+ uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty

79+ h2 <- un bnames vx vy

80+ combine bnames h1 h2

81+ uB bnames (Lam tx) (Lam ty) = un bnames tx ty

82+ uB bnames (Pi tx) (Pi ty) = un bnames tx ty

83+ uB bnames x y = do UI s f <- get

84+ let r = recoverable (binderTy x) (binderTy y)

85+ let err = CantUnify r topx topy

86+ (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s)

87+ (errEnv env) s

88+ put (UI s ((binderTy x, binderTy y, env, err) : f))

89+ return []

90+

74 -- TODO: there's an annoying amount of repetition between this and the

91 -- TODO: there's an annoying amount of repetition between this and the

75 -- main unification function. Consider lifting it out.

92 -- main unification function. Consider lifting it out.

@@ -391,12 +408,12 @@ unify ctxt env topx topy dont holes =

391

408

392 uB bnames (Let tx vx) (Let ty vy)

409 uB bnames (Let tx vx) (Let ty vy)

393 = do h1 <- un' False bnames tx ty

410 = do h1 <- un' False bnames tx ty

394− h2 <- un' False bnames ty vy

411+ h2 <- un' False bnames vx vy

395 sc 1

412 sc 1

396 combine bnames h1 h2

413 combine bnames h1 h2

397 uB bnames (Guess tx vx) (Guess ty vy)

414 uB bnames (Guess tx vx) (Guess ty vy)

398 = do h1 <- un' False bnames tx ty

415 = do h1 <- un' False bnames tx ty

399− h2 <- un' False bnames ty vy

416+ h2 <- un' False bnames vx vy

400 sc 1

417 sc 1

401 combine bnames h1 h2

418 combine bnames h1 h2

402 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

419 uB bnames (Lam tx) (Lam ty) = do sc 1; un' False bnames tx ty

src/Idris/ElabTerm.hs+2−1

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

726 [] -> []

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

728 ps <- get_probs

729− args <- apply (Var n) imps

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

730+ (match_apply (Var n) imps)

730 ps' <- get_probs

731 ps' <- get_probs

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

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

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

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