after stripping
ScopeInfo
  current = Optimised-open
  context = []
  modules
    scope
    scope Optimised-open
      private
        names
          P --> [Optimised-open._.P]
      public
        names
          A --> [Optimised-open.A]
        modules
          M₁ --> [Optimised-open.M₁]
    scope Optimised-open.M₁
      public
        names
          P --> [Optimised-open.M₁.P]
          X --> [Optimised-open.M₁.X]
    scope Optimised-open._
      public
        names
          P --> [Optimised-open._.P]
after stripping
ScopeInfo
  current = Optimised-open.M₂
  context = []
  modules
    scope
    scope Optimised-open
      private
        names
          P --> [Optimised-open._.P]
      public
        names
          A --> [Optimised-open.A]
          a --> [Optimised-open.a]
          p --> [Optimised-open.p]
        modules
          M₁ --> [Optimised-open.M₁]
    scope Optimised-open.M₁
      public
        names
          P --> [Optimised-open.M₁.P]
          X --> [Optimised-open.M₁.X]
    scope Optimised-open._
      public
        names
          P --> [Optimised-open._.P]
    scope Optimised-open.M₂
      public
        names
          P′ --> [Optimised-open.M₂._.P]
    scope Optimised-open.M₂._
      public
        names
          P′ --> [Optimised-open.M₂._.P]
Optimised-open.agda:35,9-10
(A → Set) !=< A of type Set₁
when checking that the expression P has type A
