6dffcc7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix reporting of infinite unification

6dffcc7Edwin Brady10 years ago

src/Idris/Core/Evaluate.hs+12

compare with master

unifiedsplit

@@ -26,6 +26,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

26 lookupRigCount, lookupRigCountExact,

27 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

28 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

29+ conGuarded,

29 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

30 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

30 isUniverse, linearCheck, linearCheckArg) where

31 isUniverse, linearCheck, linearCheckArg) where

@@ -1137,6 +1138,17 @@ isTCDict n ctxt

1137 Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

1138 Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

1138 _ -> False

1139 _ -> False

1139

1140

1141+-- Is the name guarded by constructors in the term?

1142+-- We assume the term is normalised, so no looking under 'let' for example.

1143+conGuarded :: Context -> Name -> Term -> Bool

1144+conGuarded ctxt n tm = guarded n tm

1145+ where

1146+ guarded n (P _ n' _) = n == n'

1147+ guarded n ap@(App _ _ _)

1148+ | (P _ f _, as) <- unApply ap,

1149+ isConName f ctxt = any (guarded n) as

1150+ guarded _ _ = False

1151+

1140lookupP :: Name -> Context -> [Term]

1152lookupP :: Name -> Context -> [Term]

1141lookupP = lookupP_all False False

1153lookupP = lookupP_all False False

1142

1154

src/Idris/Core/Unify.hs+21−19

@@ -105,10 +105,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

105

106 un names tx@(P _ x _) tm

107 | tx /= tm && holeIn env x || x `elem` holes

108− = do sc 1; checkCycle names (x, tm)

108+ = do sc 1; checkCycle names tx (x, tm)

109 un names tm ty@(P _ y _)

110 | ty /= tm && holeIn env y || y `elem` holes

111− = do sc 1; checkCycle names (y, tm)

111+ = do sc 1; checkCycle names ty (y, tm)

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

113 | length bnames > i,

114 fst (fst (bnames!!i)) == x ||

@@ -183,11 +183,12 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

183

184-- substN n tm (var, sol) = (var, subst n tm sol)

185

186− checkCycle ns p@(x, P _ x' _) | x == x' = return []

186+ checkCycle ns xtm p@(x, P _ x' _) | x == x' = return []

187− checkCycle ns p@(x, P _ _ _) = return [p]

187+ checkCycle ns xtm p@(x, P _ _ _) = return [p]

188− checkCycle ns (x, tm)

188+ checkCycle ns xtm (x, tm)

189− | not (x `elem` freeNames tm) = checkScope ns (x, tm)

190− | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

189+ | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))

190+ | x `elem` freeNames tm = unifyFail xtm tm

191+ | otherwise = checkScope ns (x, tm)

191

192

192 checkScope ns (x, tm) =

193 checkScope ns (x, tm) =

193-- case boundVs (envPos x 0 env) tm of

194-- case boundVs (envPos x 0 env) tm of

@@ -368,8 +369,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

368 | tx /= ty && (holeIn env x || x `elem` holes)

369 | tx /= ty && (holeIn env x || x `elem` holes)

369 && (holeIn env y || y `elem` holes)

370 && (holeIn env y || y `elem` holes)

370 = case compare (envPos 0 x env) (envPos 0 y env) of

371 = case compare (envPos 0 x env) (envPos 0 y env) of

371− LT -> do sc 1; checkCycle bnames (x, ty)

372+ LT -> do sc 1; checkCycle bnames tx (x, ty)

372− _ -> do sc 1; checkCycle bnames (y, tx)

373+ _ -> do sc 1; checkCycle bnames ty (y, tx)

373 where envPos i n ((n',_,_):env) | n == n' = i

374 where envPos i n ((n',_,_):env) | n == n' = i

374 envPos i n (_:env) = envPos (i+1) n env

375 envPos i n (_:env) = envPos (i+1) n env

375 envPos _ _ _ = 100000

376 envPos _ _ _ = 100000

@@ -377,7 +378,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

377 | pureTerm tm, holeIn env x || x `elem` holes

378 | pureTerm tm, holeIn env x || x `elem` holes

378 = do UI s f <- get

379 = do UI s f <- get

379 -- injectivity check

380 -- injectivity check

380− x <- checkCycle bnames (x, tm)

381+ x <- checkCycle bnames xtm (x, tm)

381 if (notP tm && fn)

382 if (notP tm && fn)

382-- trace (show (x, tm, normalise ctxt env tm)) $

383-- trace (show (x, tm, normalise ctxt env tm)) $

383-- put (UI s ((tm, topx, topy) : i) f)

384-- put (UI s ((tm, topx, topy) : i) f)

@@ -385,13 +386,13 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

385 else do sc 1

386 else do sc 1

386 return x

387 return x

387 | pureTerm tm, not (injective xtm) && injective tm

388 | pureTerm tm, not (injective xtm) && injective tm

388− = do checkCycle bnames (x, tm)

389+ = do checkCycle bnames xtm (x, tm)

389 unifyTmpFail xtm tm

390 unifyTmpFail xtm tm

390 un' env fn bnames tm ytm@(P _ y _)

391 un' env fn bnames tm ytm@(P _ y _)

391 | pureTerm tm, holeIn env y || y `elem` holes

392 | pureTerm tm, holeIn env y || y `elem` holes

392 = do UI s f <- get

393 = do UI s f <- get

393 -- injectivity check

394 -- injectivity check

394− x <- checkCycle bnames (y, tm)

395+ x <- checkCycle bnames ytm (y, tm)

395 if (notP tm && fn)

396 if (notP tm && fn)

396-- trace (show (y, tm, normalise ctxt env tm)) $

397-- trace (show (y, tm, normalise ctxt env tm)) $

397-- put (UI s ((tm, topx, topy) : i) f)

398-- put (UI s ((tm, topx, topy) : i) f)

@@ -399,7 +400,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

399 else do sc 1

400 else do sc 1

400 return x

401 return x

401 | pureTerm tm, not (injective ytm) && injective tm

402 | pureTerm tm, not (injective ytm) && injective tm

402− = do checkCycle bnames (y, tm)

403+ = do checkCycle bnames ytm (y, tm)

403 unifyTmpFail tm ytm

404 unifyTmpFail tm ytm

404 un' env fn bnames (V i) (P _ x _)

405 un' env fn bnames (V i) (P _ x _)

405 | length bnames > i,

406 | length bnames > i,

@@ -415,14 +416,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

415

416

416-- Pattern unification rule

417-- Pattern unification rule

417 un' env fn bnames tm app@(App _ _ _)

418 un' env fn bnames tm app@(App _ _ _)

418− | (P _ mv _, args) <- unApply app,

419+ | (mvtm@(P _ mv _), args) <- unApply app,

419 holeIn env mv || mv `elem` holes,

420 holeIn env mv || mv `elem` holes,

420 all rigid args,

421 all rigid args,

421 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm

422 containsOnly (mapMaybe getname args) (mapMaybe getV args) tm

422 -- && TODO: tm does not refer to any variables other than those

423 -- && TODO: tm does not refer to any variables other than those

423 -- in 'args'

424 -- in 'args'

424 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

425 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

425− checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))

426+ checkCycle bnames mvtm (mv, eta [] $ bindLams args (substEnv env tm))

426 where rigid (V i) = True

427 where rigid (V i) = True

427 rigid (P _ t _) = t `elem` map fstEnv env &&

428 rigid (P _ t _) = t `elem` map fstEnv env &&

428 not (holeIn env t || t `elem` holes)

429 not (holeIn env t || t `elem` holes)

@@ -658,10 +659,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

658 env, err, from, Unify) : f))

659 env, err, from, Unify) : f))

659 return [] -- lift $ tfail err

660 return [] -- lift $ tfail err

660

661

661− checkCycle ns p@(x, P _ _ _) = return [p]

662+ checkCycle ns xtm p@(x, P _ _ _) = return [p]

662− checkCycle ns (x, tm)

663+ checkCycle ns xtm (x, tm)

663− | not (x `elem` freeNames tm) = checkScope ns (x, tm)

664− | otherwise = lift $ tfail (InfiniteUnify x tm (errEnv env))

664+ | conGuarded ctxt x tm = lift $ tfail (InfiniteUnify x tm (errEnv env))

665+ | x `elem` freeNames tm = unifyTmpFail xtm tm

666+ | otherwise = checkScope ns (x, tm)

665

667

666 checkScope ns (x, tm) | pureTerm tm =

668 checkScope ns (x, tm) | pureTerm tm =

667-- case boundVs (envPos x 0 env) tm of

669-- case boundVs (envPos x 0 env) tm of

src/Idris/Coverage.hs+1

@@ -403,6 +403,7 @@ recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

403 | Bound <- x = True

404 | Bound <- y = True

405 | otherwise = False -- name is different, unrecoverable

406+recoverableCoverage ctxt (InfiniteUnify _ _ _) = False -- always unrecoverable

406recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

407recoverableCoverage ctxt (At _ e) = recoverableCoverage ctxt e

407recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e

408recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e

408recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

409recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e

test/TestData.hs+2−1

@@ -280,7 +280,8 @@ testFamiliesData = [

280 ( 16, ANY ),

281 ( 17, ANY ),

282 ( 18, ANY ),

283− ( 19, ANY )]),

283+ ( 19, ANY ),

284+ ( 20, ANY )]),

284 ("tutorial", "Tutorial examples",

285 ("tutorial", "Tutorial examples",

285 [ ( 1, ANY ),

286 [ ( 1, ANY ),

286 ( 2, ANY ),

287 ( 2, ANY ),

test/totality020/expectednew file+1

@@ -0,0 +1 @@

1+totality020.idr:4:5:bug _ _ Refl is a valid case

test/totality020/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality020.idr --check

3+rm -f *.ibc

test/totality020/totality020.idrnew file+4

@@ -0,0 +1,4 @@

1+%default total

3+bug : (n, m : Nat) -> n + m = n -> Void

4+bug _ _ Refl impossible