75783a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix rules for checking Borrowed types

Need to ensure that the scope of a let binding doesn't refer to names used in the let bound value, otherwise we might update or destroy before reading!

commit75783a6e289b58f99dcc6b933c10f5098c5d30eb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Aug 2014, 01:29 (12 years ago) parentddf9779

2 files changed+7−4

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Core/Typecheck.hs+4−4

idris.cabal+3

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

510510 test/unique001/run

511511 test/unique001/*.idr

512512 test/unique001/expected

513+ test/unique002/run

514+ test/unique002/*.idr

515+ test/unique002/expected

513516

514517source-repository head

515518 type: git

src/Idris/Core/Typecheck.hs+4−4

@@ -258,6 +258,10 @@ checkUnique borrowed ctxt env tm

258258 chkBinders env (Bind n b t)

259259 = do chkBinderName env n b

260260 chkBinders ((n, b) : env) t

261+ chkBinders env (binderTy b)

262+ case b of

263+ Let t v -> chkBinders env v

264+ _ -> return ()

261265 chkBinders env t = return ()

262266

263267 chkBinderName :: Env -> Name -> Binder Term ->

@@ -275,10 +279,6 @@ checkUnique borrowed ctxt env tm

275279 UType AllTypes -> do ns <- get

276280 put ((n, (Once, AllTypes)) : ns)

277281 _ -> return ()

278− chkBinders env (binderTy b)

279− case b of

280− Let t v -> chkBinders env v

281− _ -> return ()

282282

283283 chkName n

284284 = do ns <- get