type-checking false positive with effect type

[ceedubs]

structural type Runner g = Runner (forall a. '{g} a -> {} a)

pureRunner : Runner {}
pureRunner = Runner base.force

-- this compiles, but shouldn't the effect type parameter on Runner be invariant?
runner : Runner {IO}
runner = pureRunner

    ⍟ These new definitions are ok to `add`:
    
      structural type Runner g
      pureRunner : Runner {}
      runner     : Runner {IO}