e380d0c · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -270,6 +270,9 @@ Extra-source-files:

270 test/reg052/run

271 test/reg052/*.idr

272 test/reg052/expected

273+ test/reg053/run

274+ test/reg053/*.idr

275+ test/reg053/expected

273

276

274 test/basic001/run

277 test/basic001/run

275 test/basic001/*.idr

278 test/basic001/*.idr

src/Idris/Core/Unify.hs+8−2

@@ -222,7 +222,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

222 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

223 explicitHole t = t

224

225−trimSolutions ns = dropPairs ns

225+trimSolutions ns = followSols (dropPairs ns)

226 where dropPairs [] = []

227 dropPairs (n@(x, P _ x' _) : ns)

228 | x == x' = dropPairs ns

@@ -232,7 +232,13 @@ trimSolutions ns = dropPairs ns

232 (n, P _ n' _) -> not (n == x' && n' == x)

233 _ -> True) ns)

234 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+

236expandLets env (x, tm) = (x, doSubst (reverse env) tm)

242expandLets env (x, tm) = (x, doSubst (reverse env) tm)

237 where

243 where

238 doSubst [] tm = tm

244 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