Erase %World for the purpose of newtypes

We never inspect it, so it carries no information - it just needs to be
there as a token to make sure that IO operations run at the right time.
So, IORes can be a newtype now and therefore optimised away.

libs/prelude/PrimIO.idr

@@ -27,6 +27,7 @@ prim_io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
 prim_io_bind fn k w
     = let MkIORes x' w' = fn w in k x' w'
 
+%inline
 export
 io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
 io_bind (MkIO fn)

src/Compiler/CompileExpr.idr

@@ -223,6 +223,7 @@ mutual
                    pure $ natHack res
 
 mutual
+  -- In the below, treat %World, and newtypes, as default cases
   conCases : {auto c : Ref Ctxt Defs} ->
              NameTags -> Name -> List (CaseAlt vars) ->
              Core (List (CConAlt vars))
@@ -243,6 +244,8 @@ mutual
                NameTags -> Name -> List (CaseAlt vars) ->
                Core (List (CConstAlt vars))
   constCases tags n [] = pure []
+  constCases tags n (ConstCase WorldVal sc :: ns)
+      = constCases tags n ns
   constCases tags n (ConstCase x sc :: ns)
       = pure $ MkConstAlt x !(toCExpTree tags n sc) ::
                     !(constCases tags n ns)
@@ -255,6 +258,8 @@ mutual
   getDef fc scr tags n [] = pure Nothing
   getDef fc scr tags n (DefaultCase sc :: ns)
       = pure $ Just !(toCExpTree tags n sc)
+  getDef fc scr tags n (ConstCase WorldVal sc :: ns)
+      = pure $ Just !(toCExpTree tags n sc)
   getDef {vars} fc scr tags n (ConCase x tag args sc :: ns)
       = do defs <- get Ctxt
            case !(lookupDefExact x (gamma defs)) of

src/Compiler/Scheme/Chez.idr

@@ -202,16 +202,11 @@ cCall fc cfn clib args ret
     applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
     applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as
 
-    getVal : String -> String
-    getVal str = "(vector-ref " ++ str ++ "2)"
-
     mkFun : List CFType -> CFType -> String -> String
     mkFun args ret n
         = let argns = mkNs 0 args in
               "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
-              (case ret of
-                    CFIORes _ => getVal (applyLams n argns) ++ ")"
-                    _ => applyLams n argns ++ ")")
+              (applyLams n argns ++ ")")
 
     notWorld : CFType -> Bool
     notWorld CFWorld = False

src/Compiler/Scheme/Common.idr

@@ -234,7 +234,7 @@ toPrim pn = Unknown pn
 
 export
 mkWorld : String -> String
-mkWorld res = schConstructor 0 ["#f", res, "#f"] -- MkIORes
+mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 ["#f", res, "#f"] -- MkIORes
 
 schConstant : (String -> String) -> Constant -> String
 schConstant _ (I x) = show x

src/Compiler/Scheme/Racket.idr

@@ -180,16 +180,11 @@ cCall fc cfn libspec args ret
     applyLams n (Just (a, ty) :: as)
         = applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as
 
-    getVal : CFType -> String -> String
-    getVal ty str = rktToC ty ("(vector-ref " ++ str ++ "2)")
-
     mkFun : List CFType -> CFType -> String -> String
     mkFun args ret n
         = let argns = mkNs 0 args in
               "(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++
-              (case ret of
-                    CFIORes rt => getVal rt (applyLams n argns) ++ ")"
-                    _ => applyLams n argns ++ ")")
+              (applyLams n argns ++ ")")
 
     notWorld : CFType -> Bool
     notWorld CFWorld = False

src/Idris/Elab/Interface.idr

@@ -308,6 +308,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
              log 5 $ "Top level methods: " ++ show fns
              traverse (processDecl [] nest env) fns
              traverse_ (\n => do mn <- inCurrentNS n
+                                 setFlag fc mn Inline
                                  setFlag fc mn TCInline
                                  setFlag fc mn Overloadable) meth_names
 

src/TTImp/ProcessData.idr

@@ -197,6 +197,10 @@ getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat)
 getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc)
     = getRelevantArg defs (1 + i) rel
            !(sc defs (toClosure defaultOpts [] (Erased fc False)))
+-- %World is never inspected, so might as well be deleted from data types
+getRelevantArg defs i rel (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc)
+    = getRelevantArg defs (1 + i) rel
+           !(sc defs (toClosure defaultOpts [] (Erased fc False)))
 getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
     = getRelevantArg defs (1 + i) (Just i)
            !(sc defs (toClosure defaultOpts [] (Erased fc False)))