Cannot unify with non-toplevel 'forall'

[iacore]

Example 1

poly : IO a -> IO a
poly = id

hole_to_fill : IO (forall a . IO a -> IO a)
hole_to_fill = pure poly

1/1: Building implicit-unify (implicit-unify.idr)
Error: While processing right hand side of hole_to_fill. Can't find an implementation for Applicative ?f.

implicit-unify:7:16--7:25
 3 | 
 4 | poly : (forall a . IO a -> IO a)
 5 | 
 6 | hole_to_fill : IO (forall a . IO a -> IO a)
 7 | hole_to_fill = pure poly
                    ^^^^^^^^^

Workaround : pure {f=IO} poly

Example 2

poly : (forall a . IO a -> IO a)

hole_to_fill : IO (forall a . IO a -> IO a)
hole_to_fill = do
   putStrLn "something"
   pure {f=IO} poly

1/1: Building implicit-unify (implicit-unify.idr)
Error: While processing right hand side of hole_to_fill. When unifying:
    IO (IO ?a -> IO ?a)
and:
    IO (IO a -> IO a)
Mismatch between: IO ?a -> IO ?a and IO a -> IO a.

implicit-unify:8:4--8:24
 4 | poly : (forall a . IO a -> IO a)
 5 | 
 6 | hole_to_fill : IO (forall a . IO a -> IO a)
 7 | hole_to_fill = do
 8 |    putStrLn "something"
        ^^^^^^^^^^^^^^^^^^^^

Workaround : name pure {f=IO} poly as separate term. Example:

export
createRng : (seed: Int) -> IO (forall a . Random Int a -> IO a)
createRng seed = do
   seed' <- newIORef $ nextseed seed
   let -- workaround idris2 bug
      erased0 : IO (forall a . Random Int a -> IO a)
      erased0 = pure {f=IO} $ nextNumber seed'
   erased0