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

git.iko.soy/Idris-dev

Fix reporting of infinite unification

It's not infinite if there's a function involved which might reduce later, so we should only report if the variable being unified is constructor guarded. This affects coverage checking, because infinite unification is an unrecoverable error. Fixes #3666

commit6dffcc71856a447584dbef0dadffab28b24d5bbc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 5 Mar 2017, 16:30 (10 years ago) parenta865b02

7 files changed+44−20

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+12 src/Idris/Core/Unify.hs+21−19 src/Idris/Coverage.hs+1 test/TestData.hs+2−1 test/totality020/expected+1 test/totality020/run+3 test/totality020/totality020.idr+4

src/Idris/Core/Evaluate.hs+12

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

2626 lookupRigCount, lookupRigCountExact,

2727 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

2828 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

29+ conGuarded,

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

3031 isUniverse, linearCheck, linearCheckArg) where

3132

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

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

11381139 _ -> False

11391140

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+

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

11411153lookupP = lookupP_all False False

11421154

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

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

105105

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

107107 | 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)

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

110110 | 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)

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

113113 | length bnames > i,

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

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

183183

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

185185

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

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

188− checkCycle ns (x, tm)

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

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

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

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

188+ checkCycle ns xtm (x, tm)

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)

191192

192193 checkScope ns (x, tm) =

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

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

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

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

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

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

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

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

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

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

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

375376 envPos _ _ _ = 100000

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

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

378379 = do UI s f <- get

379380 -- injectivity check

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

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

381382 if (notP tm && fn)

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

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

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

385386 else do sc 1

386387 return x

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

388− = do checkCycle bnames (x, tm)

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

389390 unifyTmpFail xtm tm

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

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

392393 = do UI s f <- get

393394 -- injectivity check

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

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

395396 if (notP tm && fn)

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

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

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

399400 else do sc 1

400401 return x

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

402− = do checkCycle bnames (y, tm)

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

403404 unifyTmpFail tm ytm

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

405406 | length bnames > i,

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

415416

416417-- Pattern unification rule

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

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

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

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

420421 all rigid args,

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

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

423424 -- in 'args'

424425 = -- 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))

426427 where rigid (V i) = True

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

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

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

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

659660 return [] -- lift $ tfail err

660661

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

662− checkCycle ns (x, tm)

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

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

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

663+ checkCycle ns xtm (x, tm)

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)

665667

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

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

src/Idris/Coverage.hs+1

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

403403 | Bound <- x = True

404404 | Bound <- y = True

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

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

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

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

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

test/TestData.hs+2−1

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

280280 ( 16, ANY ),

281281 ( 17, ANY ),

282282 ( 18, ANY ),

283− ( 19, ANY )]),

283+ ( 19, ANY ),

284+ ( 20, ANY )]),

284285 ("tutorial", "Tutorial examples",

285286 [ ( 1, ANY ),

286287 ( 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