Type Providers mean we can't relax the signature of run__provider
commit2a883b99a7688fc694b10619b59b7f83310f0bcb
authorSam Elliott <sam@lenary.co.uk>
dateMon 6 Apr 2015, 15:24 (12 years ago)
parent76ec3fe
libs/prelude/IO.idr+3−1
@@ -152,7 +152,9 @@ FFI_C = MkFFI C_Types String String
152152IO : Type -> Type
153153IO = IO' FFI_C
154154
155−run__provider : IO' l a -> PrimIO a
155+-- Cannot be relaxed as is used by type providers and they expect IO a
156+-- in the first argument.
157+run__provider : IO a -> PrimIO a
156158run__provider (MkIO f) = f (TheWorld prim__TheWorld)
157159
158160prim_fork : PrimIO () -> PrimIO Ptr