c710867 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better unification errors when name is out of scope

c710867Edwin Brady13 years ago

src/Core/TT.hs+11

compare with master

unifiedsplit

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

60 -- unification succeed

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

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

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

63 | CantInferType String

64 | CantInferType String

64 | NonFunctionType Term Term

65 | NonFunctionType Term Term

65 | CantIntroduce Term

66 | CantIntroduce Term

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

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

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

87 size (InfiniteUnify _ right _) = size right

88 size (InfiniteUnify _ right _) = size right

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

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

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

89 size (NoSuchVariable name) = size name

91 size (NoSuchVariable name) = size name

90 size (NoTypeDecl name) = size name

92 size (NoTypeDecl name) = size name

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

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

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

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

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

591 subst i t = t

593 subst i t = t

592

594

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+

593explicitNames :: TT n -> TT n

604explicitNames :: TT n -> TT n

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

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

595 Bind x b'

606 Bind x b'

src/Core/Unify.hs+39−10

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

48 where

49 un names (P _ x _) tm

50 | holeIn env x || x `elem` holes

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

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

52 un names tm (P _ y _)

53 | holeIn env y || y `elem` holes

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

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

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

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

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

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

93 sc 1

94 combine bnames as (ns' ++ bs)

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

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

97− checkCycle (x, tm)

97+ checkCycle ns (x, tm)

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

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

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

100

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+

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

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

102notTrivial _ = True

110notTrivial _ = True

103

111

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

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

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

196 then unifyTmpFail xtm tm

204 then unifyTmpFail xtm tm

197 else do sc 1

205 else do sc 1

198− checkCycle (x, tm)

206+ checkCycle bnames (x, tm)

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

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

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

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

201 | holeIn env y || y `elem` holes

209 | holeIn env y || y `elem` holes

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

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

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

207 then unifyTmpFail tm ytm

215 then unifyTmpFail tm ytm

208 else do sc 1

216 else do sc 1

209− checkCycle (y, tm)

217+ checkCycle bnames (y, tm)

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

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

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

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

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

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

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

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

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

399 return [] -- lift $ tfail err

407 return [] -- lift $ tfail err

400

408

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

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

402− checkCycle (x, tm)

410+ checkCycle ns (x, tm)

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

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

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

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

405

413

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)

406

421

407 combineArgs bnames args = ca [] args where

422 combineArgs bnames args = ca [] args where

408 ca acc [] = return acc

423 ca acc [] = return acc

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

419 sc 1

434 sc 1

420 combine bnames as (ns' ++ bs)

435 combine bnames as (ns' ++ bs)

421

436

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+

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

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

423-- more work may help.

452-- more work may help.

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

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

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

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

114 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 ""

115pshow i (CantInferType t)

121pshow i (CantInferType t)

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

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

117pshow i (NonFunctionType f ty)

123pshow i (NonFunctionType f ty)