c710867 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better unification errors when name is out of scope

In particular, a unification problem which cannot be solved because it uses a variable not in scope where the metavariable is bound. Fixes #342

commitc710867ebc8450ebd62cd469dbdd308a56243ce6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Jul 2013, 19:53 (13 years ago) parent02367f9

3 files changed+56−10

compare with master

unifiedsplit

src/Core/TT.hs+11 src/Core/Unify.hs+39−10 src/Idris/Delaborate.hs+6

src/Core/TT.hs+11

@@ -60,6 +60,7 @@ data Err = Msg String

6060 -- unification succeed

6161 | InfiniteUnify Name Term [(Name, Type)]

6262 | CantConvert Term Term [(Name, Type)]

63+ | UnifyScope Name Name Term [(Name, Type)]

6364 | CantInferType String

6465 | NonFunctionType Term Term

6566 | CantIntroduce Term

@@ -86,6 +87,7 @@ instance Sized Err where

8687 size (CantUnify _ left right err _ score) = size left + size right + size err

8788 size (InfiniteUnify _ right _) = size right

8889 size (CantConvert left right _) = size left + size right

90+ size (UnifyScope _ _ right _) = size right

8991 size (NoSuchVariable name) = size name

9092 size (NoTypeDecl name) = size name

9193 size (NotInjective l c r) = size l + size c + size r

@@ -590,6 +592,15 @@ instantiate e = subst 0 where

590592 subst i (Proj x idx) = Proj (subst i x) idx

591593 subst i t = t

592594

595+substV :: TT n -> TT n -> TT n

596+substV x tm = dropV 0 (instantiate x tm) where

597+ dropV i (V x) | x > i = V (x - 1)

598+ | otherwise = V x

599+ dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

600+ dropV i (App f a) = App (dropV i f) (dropV i a)

601+ dropV i (Proj x idx) = Proj (dropV i x) idx

602+ dropV i t = t

603+

593604explicitNames :: TT n -> TT n

594605explicitNames (Bind x b sc) = let b' = fmap explicitNames b in

595606 Bind x b'

src/Core/Unify.hs+39−10

@@ -48,10 +48,10 @@ match_unify ctxt env topx topy dont holes =

4848 where

4949 un names (P _ x _) tm

5050 | holeIn env x || x `elem` holes

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

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

5252 un names tm (P _ y _)

5353 | holeIn env y || y `elem` holes

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

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

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

5656 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

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

@@ -93,11 +93,19 @@ match_unify ctxt env topx topy dont holes =

9393 sc 1

9494 combine bnames as (ns' ++ bs)

9595

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

97− checkCycle (x, tm)

98− | not (x `elem` freeNames tm) = return [(x, tm)]

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

97+ checkCycle ns (x, tm)

98+ | not (x `elem` freeNames tm) = checkScope ns (x, tm)

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

100100

101+ checkScope ns (x, tm) =

102+ case boundVs (envPos x 0 env) tm of

103+ [] -> return [(x, tm)]

104+ (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))

105+ (inst ns tm) (errEnv env))

106+ where inst [] tm = tm

107+ inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

108+

101109notTrivial (x, P _ x' _) = x /= x'

102110notTrivial _ = True

103111

@@ -195,7 +203,7 @@ unify ctxt env topx topy dont holes =

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

196204 then unifyTmpFail xtm tm

197205 else do sc 1

198− checkCycle (x, tm)

206+ checkCycle bnames (x, tm)

199207 | not (injective xtm) && injective tm = unifyFail xtm tm

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

201209 | holeIn env y || y `elem` holes

@@ -206,7 +214,7 @@ unify ctxt env topx topy dont holes =

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

207215 then unifyTmpFail tm ytm

208216 else do sc 1

209− checkCycle (y, tm)

217+ checkCycle bnames (y, tm)

210218 | not (injective ytm) && injective tm = unifyFail ytm tm

211219 un' fn bnames (V i) (P _ x _)

212220 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

@@ -398,11 +406,18 @@ unify ctxt env topx topy dont holes =

398406 put (UI s ((binderTy x, binderTy y, env, err) : f))

399407 return [] -- lift $ tfail err

400408

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

402− checkCycle (x, tm)

403− | not (x `elem` freeNames tm) = return [(x, tm)]

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

410+ checkCycle ns (x, tm)

411+ | not (x `elem` freeNames tm) = checkScope ns (x, tm)

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

405413

414+ checkScope ns (x, tm) =

415+ case boundVs (envPos x 0 env) tm of

416+ [] -> return [(x, tm)]

417+ (i:_) -> lift $ tfail (UnifyScope x (fst (ns!!i))

418+ (inst ns tm) (errEnv env))

419+ where inst [] tm = tm

420+ inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

406421

407422 combineArgs bnames args = ca [] args where

408423 ca acc [] = return acc

@@ -419,6 +434,20 @@ unify ctxt env topx topy dont holes =

419434 sc 1

420435 combine bnames as (ns' ++ bs)

421436

437+boundVs :: Int -> Term -> [Int]

438+boundVs i (V j) | j <= i = []

439+ | otherwise = [j]

440+boundVs i (Bind n b sc) = boundVs (i + 1) sc

441+boundVs i (App f x) = let fs = boundVs i f

442+ xs = boundVs i x in

443+ nub (fs ++ xs)

444+boundVs i _ = []

445+

446+envPos x i [] = 0

447+envPos x i ((y, _) : ys) | x == y = i

448+ | otherwise = envPos x (i + 1) ys

449+

450+

422451-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

423452-- more work may help.

424453-- FIXME: Depending on how overloading gets used, this may cause problems. Better

src/Idris/Delaborate.hs+6

@@ -112,6 +112,12 @@ pshow i (CantConvert x y env)

112112 "Can't convert " ++ showImp imps (delab i x) ++ " with "

113113 ++ showImp imps (delab i y) ++

114114 if (opt_errContext (idris_options i)) then showSc i env else ""

115+pshow i (UnifyScope n out tm env)

116+ = let imps = opt_showimp (idris_options i) in

117+ "Can't unify " ++ show n ++ " with "

118+ ++ showImp imps (delab i tm) ++ " as " ++ show out ++

119+ " is not in scope" ++

120+ if (opt_errContext (idris_options i)) then showSc i env else ""

115121pshow i (CantInferType t)

116122 = "Can't infer type for " ++ t

117123pshow i (NonFunctionType f ty)