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

git.iko.soy/Idris-dev

on master help sign in

Fix rules for checking Borrowed types

75783a6Edwin Brady12 years ago

idris.cabal+3

compare with master

unifiedsplit

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

510 test/unique001/run

511 test/unique001/*.idr

512 test/unique001/expected

513+ test/unique002/run

514+ test/unique002/*.idr

515+ test/unique002/expected

513

516

514source-repository head

517source-repository head

515 type: git

518 type: git

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

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

258 chkBinders env (Bind n b t)

259 = do chkBinderName env n b

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

261+ chkBinders env (binderTy b)

262+ case b of

263+ Let t v -> chkBinders env v

264+ _ -> return ()

261 chkBinders env t = return ()

265 chkBinders env t = return ()

262

266

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

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

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

275 UType AllTypes -> do ns <- get

279 UType AllTypes -> do ns <- get

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

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

277 _ -> return ()

281 _ -> return ()

278− chkBinders env (binderTy b)

279− case b of

280− Let t v -> chkBinders env v

281− _ -> return ()

282

283 chkName n

284 = do ns <- get