after stripping
ScopeInfo
  current = Optimised-open
  context = []
  modules
    scope
      private
        names
          Prop --> [Agda.Primitive.Prop]
          Set --> [Agda.Primitive.Set]
      imports
        [Agda.Primitive]
    scope Agda.Primitive
      public
        names
          _⊔_ --> [Agda.Primitive._⊔_]
          Level --> [Agda.Primitive.Level]
          Prop --> [Agda.Primitive.Prop]
          SSet --> [Agda.Primitive.SSet]
          SSetω --> [Agda.Primitive.SSetω]
          Set --> [Agda.Primitive.Set]
          Setω --> [Agda.Primitive.Setω]
          lsuc --> [Agda.Primitive.lsuc]
          lzero --> [Agda.Primitive.lzero]
    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
      private
        names
          Prop --> [Agda.Primitive.Prop]
          Set --> [Agda.Primitive.Set]
      imports
        [Agda.Primitive]
    scope Agda.Primitive
      public
        names
          _⊔_ --> [Agda.Primitive._⊔_]
          Level --> [Agda.Primitive.Level]
          Prop --> [Agda.Primitive.Prop]
          SSet --> [Agda.Primitive.SSet]
          SSetω --> [Agda.Primitive.SSetω]
          Set --> [Agda.Primitive.Set]
          Setω --> [Agda.Primitive.Setω]
          lsuc --> [Agda.Primitive.lsuc]
          lzero --> [Agda.Primitive.lzero]
    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
when checking that the expression P has type A
