Internal error when opening a module inside a constructor

[omelkonian]

This program (artificially produced by minimizing a larger one):

open import Agda.Builtin.Sigma

dup : ∀ {A : Set} → A → Σ A λ _ → A
dup x = x , x

postulate
  A : Set

module M {x : A} where
  y = x

data X : Set where
  mkX : ∀ {x : A}
    → let
        (_ , _) = dup x
        open M {x}
      in
      X

produces this error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:106:26 in Agda-2.6.2-5d92e0bc62f6513c7aa12fd932a1e27cdc986b039aa0267ec831a1bc44eb00c1:Agda.TypeChecking.Serialise.Instances.Internal

Agda version: 2.6.2

[andreasabel]

There is an unsolved meta surviving up to serialization, triggering the crash:

agda/src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs

Line 106 in 3185db9

icod_ (MetaV a b) = __IMPOSSIBLE__

Could be a duplicate of #5544.

[omelkonian]

Another interesting occurrence with product projections:

open import Data.Product
open import Data.List
open import Agda.Builtin.Equality

postulate A B : Set

module _ (xys : List (A × B)) where
  xs = proj₁ (unzip xys)
  module H (_ : xs ≡ []) where
    i = xs

data X : List A → Set where
  [⊤] : ∀ {xys : List (A × B)}
    → let xs = proj₁ (unzip xys) in
      (eq : xs ≡ [])
    → let open H xys eq in
      X i

  [⊥] : ∀ {xys : List (A × B)}
    → let xs , _ = unzip xys in
      (eq : xs ≡ [])
    → let open H xys eq in
      X i

The [⊤] constructor (which uses proj₁) works fine, but the [⊥] constructor (which uses pattern matching in a let instead) leads to the same internal error.

[UlfNorell]

This did get fixed by the fix to #5544 so looks like the same problem.