git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2116 from lenary/relax-io-types

Type Signatures use IO' l where they can instead of IO

commitb8a3f7e224265584596968d0181aa13e68a46788 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 9 Apr 2015, 16:18 (12 years ago) parentbfd93a22a883b9
2 files changed+4−2
compare with master
unifiedsplit
libs/prelude/IO.idr+3−1 libs/prelude/Prelude.idr+1−1
libs/prelude/IO.idr+3−1
@@ -152,13 +152,15 @@ FFI_C = MkFFI C_Types String String
152152IO : Type -> Type
153153IO = IO' FFI_C
154154
155+-- Cannot be relaxed as is used by type providers and they expect IO a
156+-- in the first argument.
155157run__provider : IO a -> PrimIO a
156158run__provider (MkIO f) = f (TheWorld prim__TheWorld)
157159
158160prim_fork : PrimIO () -> PrimIO Ptr
159161prim_fork x = prim_io_return prim__vm -- compiled specially
160162
161−fork : IO () -> IO Ptr
163+fork : IO' l () -> IO' l Ptr
162164fork (MkIO f) = MkIO (\w => prim_io_bind
163165 (prim_fork (prim_io_bind (f w)
164166 (\ x => prim_io_return x)))
libs/prelude/Prelude.idr+1−1
@@ -526,7 +526,7 @@ validFile (FHandle h) = do x <- nullPtr h
526526||| @ test the condition of the loop
527527||| @ body the loop body
528528partial -- obviously
529−while : (test : IO Bool) -> (body : IO ()) -> IO ()
529+while : (test : IO' l Bool) -> (body : IO' l ()) -> IO' l ()
530530while t b = do v <- t
531531 if v then do b
532532 while t b