git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1678 from edwinb/unify-fix

Unification fix for chains of solutions

commite380d0c098223907f2bfe4be57fa592dd2e280d2 authorEdwin Brady <edwin.brady@gmail.com> dateSun 26 Oct 2014, 12:37 (12 years ago) parent3172f4837b11f8
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