git.iko.soy/Idris-dev
on master help sign in
Check for cycles in unification results
713776cEdwin Brady
src/Idris/Core/Unify.hs+24−12
compare with master
unifiedsplit
@@ -66,20 +66,24 @@ match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [Fail
66match_unify ctxt env topx topy inj holes from =
66match_unify ctxt env topx topy inj holes from =
67 case runStateT (un [] (renameBindersTm env topx)
67 case runStateT (un [] (renameBindersTm env topx)
68 (renameBindersTm env topy)) (UI 0 []) of
68 (renameBindersTm env topy)) (UI 0 []) of
69+ OK (v, UI _ []) ->
70+ do v' <- trimSolutions topx topy from env v
69− OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v))
71+ return (map (renameBinders env) v')
70 res ->
72 res ->
71 let topxn = renameBindersTm env (normalise ctxt env topx)
73 let topxn = renameBindersTm env (normalise ctxt env topx)
72 topyn = renameBindersTm env (normalise ctxt env topy) in
74 topyn = renameBindersTm env (normalise ctxt env topy) in
73 case runStateT (un [] topxn topyn)
75 case runStateT (un [] topxn topyn)
74 (UI 0 []) of
76 (UI 0 []) of
75 OK (v, UI _ fails) ->
77 OK (v, UI _ fails) ->
78+ do v' <- trimSolutions topx topy from env v
76− return (map (renameBinders env) (trimSolutions v))
79+ return (map (renameBinders env) v')
77 Error e ->
80 Error e ->
78 -- just normalise the term we're matching against
81 -- just normalise the term we're matching against
79 case runStateT (un [] topxn topy)
82 case runStateT (un [] topxn topy)
80 (UI 0 []) of
83 (UI 0 []) of
81 OK (v, UI _ fails) ->
84 OK (v, UI _ fails) ->
85+ do v' <- trimSolutions topx topy from env v
82− return (map (renameBinders env) (trimSolutions v))
86+ return (map (renameBinders env) v')
83 _ -> tfail e
87 _ -> tfail e
84 where
88 where
85 -- This rule is highly dubious... it certainly produces a valid answer
89 -- This rule is highly dubious... it certainly produces a valid answer
@@ -227,7 +231,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm
227 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
231 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
228 explicitHole t = t
232 explicitHole t = t
229
233
230−trimSolutions ns = followSols (dropPairs ns)
234+trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
231 where dropPairs [] = []
235 where dropPairs [] = []
232 dropPairs (n@(x, P _ x' _) : ns)
236 dropPairs (n@(x, P _ x' _) : ns)
233 | x == x' = dropPairs ns
237 | x == x' = dropPairs ns
@@ -238,11 +242,19 @@ trimSolutions ns = followSols (dropPairs ns)
238 _ -> True) ns)
242 _ -> True) ns)
239 dropPairs (n : ns) = n : dropPairs ns
243 dropPairs (n : ns) = n : dropPairs ns
240
244
241− followSols [] = []
245+ followSols vs [] = return []
242− followSols ((n, P _ t _) : ns)
246+ followSols vs ((n, P _ t _) : ns)
243 | Just t' <- lookup t ns
247 | Just t' <- lookup t ns
244− = followSols ((n, t') : ns) -- Are we guaranteed no cycles?
248+ = do vs' <- case t' of
249+ P _ tn _ ->
250+ if (n, tn) `elem` vs then -- cycle
251+ tfail (cantUnify from False topx topy
252+ (Msg "") (errEnv env) 0)
253+ else return ((n, tn) : vs)
254+ _ -> return vs
255+ followSols vs' ((n, t') : ns)
245− followSols (n : ns) = n : followSols ns
256+ followSols vs (n : ns) = do ns' <- followSols vs ns
257+ return $ n : ns'
246
258
247expandLets env (x, tm) = (x, doSubst (reverse env) tm)
259expandLets env (x, tm) = (x, doSubst (reverse env) tm)
248 where
260 where
@@ -267,8 +279,8 @@ unify ctxt env topx topy inj holes usersupp from =
267 -- don't bother if topx and topy are different at the head
279 -- don't bother if topx and topy are different at the head
268 case runStateT (un False [] (renameBindersTm env topx)
280 case runStateT (un False [] (renameBindersTm env topx)
269 (renameBindersTm env topy)) (UI 0 []) of
281 (renameBindersTm env topy)) (UI 0 []) of
282+ OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v
270− OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),
283+ return (map (renameBinders env) v', [])
271− [])
272 res ->
284 res ->
273 let topxn = renameBindersTm env (normalise ctxt env topx)
285 let topxn = renameBindersTm env (normalise ctxt env topx)
274 topyn = renameBindersTm env (normalise ctxt env topy) in
286 topyn = renameBindersTm env (normalise ctxt env topy) in
@@ -276,8 +288,8 @@ unify ctxt env topx topy inj holes usersupp from =
276 case runStateT (un False [] topxn topyn)
288 case runStateT (un False [] topxn topyn)
277 (UI 0 []) of
289 (UI 0 []) of
278 OK (v, UI _ fails) ->
290 OK (v, UI _ fails) ->
291+ do v' <- trimSolutions topx topy from env v
279− return (map (renameBinders env) (trimSolutions v),
292+ return (map (renameBinders env) v', reverse fails)
280− reverse fails)
281-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
293-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
282 Error e -> tfail e
294 Error e -> tfail e
283 where
295 where