git.iko.soy/Idris-dev
on master help sign in
Unification fix for chains of solutions

If we have (x,y), (y,z), etc, we need to have (x,z) as the solution instead, and sometimes this didn't happen. Fixes #1627

commit37b11f84af9cd95d375edf19560aa3f7e32ae073 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 26 Oct 2014, 11:59 (12 years ago) parent3172f48
5 files changed+23−2
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Core/Unify.hs+8−2 test/reg053/expected test/reg053/four.idr+9 test/reg053/run+3
idris.cabal+3
@@ -270,6 +270,9 @@ Extra-source-files:
270270 test/reg052/run
271271 test/reg052/*.idr
272272 test/reg052/expected
273+ test/reg053/run
274+ test/reg053/*.idr
275+ test/reg053/expected
273276
274277 test/basic001/run
275278 test/basic001/*.idr
src/Idris/Core/Unify.hs+8−2
@@ -222,7 +222,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm
222222 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
223223 explicitHole t = t
224224
225−trimSolutions ns = dropPairs ns
225+trimSolutions ns = followSols (dropPairs ns)
226226 where dropPairs [] = []
227227 dropPairs (n@(x, P _ x' _) : ns)
228228 | x == x' = dropPairs ns
@@ -232,7 +232,13 @@ trimSolutions ns = dropPairs ns
232232 (n, P _ n' _) -> not (n == x' && n' == x)
233233 _ -> True) ns)
234234 dropPairs (n : ns) = n : dropPairs ns
235−
235+
236+ followSols [] = []
237+ followSols ((n, P _ t _) : ns)
238+ | Just t' <- lookup t ns
239+ = followSols ((n, t') : ns) -- Are we guaranteed no cycles?
240+ followSols (n : ns) = n : followSols ns
241+
236242expandLets env (x, tm) = (x, doSubst (reverse env) tm)
237243 where
238244 doSubst [] tm = tm
test/reg053/expectednew file

No changes to the content.

test/reg053/four.idrnew file+9
@@ -0,0 +1,9 @@
1+module FourFunctor
2+
3+data FourFunctor y = Four y y y y
4+
5+traverseFourFunctor : Applicative f ->
6+ (x -> f b) -> FourFunctor x -> f (FourFunctor b)
7+traverseFourFunctor constr f (Four w x y z)
8+ = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)
9+
test/reg053/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check four.idr
3+rm -f *.ibc