dcc8d46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make more type classes resolve, by matching rather than unification

Change 'apply' to 'match_apply' so that missing arguments are filled in by matching on normal forms. This is safe (we think), since type class resolution is merely looking for one instance which works, and this will make more instances work. Fixes #527

commitdcc8d46dfa7c1f58b0f8acfebc0a2b2a96cb4b94 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 14 Oct 2013, 11:32 (13 years ago) parentb75246b

2 files changed+22−4

compare with master

unifiedsplit

src/Core/Unify.hs+20−3 src/Idris/ElabTerm.hs+2−1

src/Core/Unify.hs+20−3

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

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

3535 TC [(Name, TT Name)]

3636match_unify ctxt env topx topy dont holes =

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

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

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

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

4040 res ->

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

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

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

5858 | 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

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

6064 = do hf <- un names fx fy

6165 ha <- un names ax ay

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

7175 lift $ tfail err

7276

7377

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+

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

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

7693

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

391408

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

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

394− h2 <- un' False bnames ty vy

411+ h2 <- un' False bnames vx vy

395412 sc 1

396413 combine bnames h1 h2

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

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

399− h2 <- un' False bnames ty vy

416+ h2 <- un' False bnames vx vy

400417 sc 1

401418 combine bnames h1 h2

402419 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

726726 [] -> []

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

728728 ps <- get_probs

729− args <- apply (Var n) imps

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

730+ (match_apply (Var n) imps)

730731 ps' <- get_probs

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

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