git.iko.soy/Idris-dev
on master help sign in
Fix borrowed type check

Actually a borrowed type can be used as many times as you like, it's just the names inside the pattern that can't be used without being lent first!

commitddf9779f8769a671aa8cff2669236e85c0626951 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Aug 2014, 00:12 (12 years ago) parentb37dcbe
2 files changed+2−2
compare with master
unifiedsplit
src/Idris/Core/Typecheck.hs+1−1 test/unique001/unique001d.idr+1−1
src/Idris/Core/Typecheck.hs+1−1
@@ -271,7 +271,7 @@ checkUnique borrowed ctxt env tm
271271 then put ((n, (LendOnly, NullType)) : ns)
272272 else put ((n, (Once, UniqueType)) : ns)
273273 UType NullType -> do ns <- get
274− put ((n, (LendOnly, NullType)) : ns)
274+ put ((n, (Many, NullType)) : ns)
275275 UType AllTypes -> do ns <- get
276276 put ((n, (Once, AllTypes)) : ns)
277277 _ -> return ()
test/unique001/unique001d.idr+1−1
@@ -1,3 +1,3 @@
11
22steal : {a : UniqueType} -> Borrowed a -> a
3−steal x = x
3+steal (Read x) = x