`__IMPOSSIBLE__` error in SSet but not in Set

[FernandoChu]

It seems to be a problem of eta for functions with SSet? I'm not sure. Here's the smallest example I could reduce this to:

{-# OPTIONS --two-level #-}

open import Agda.Primitive

variable A B C : SSet

_∘_ :
  (B → C) → (A → B) → A → C
(g ∘ f) a = g (f a)

id : A → A
id = λ x → x

record Σ (A : SSet) (B : A → SSet) : SSet where
  constructor _,_
  field
    pr1 : A
    pr2 : B pr1

_×_ : (A : SSet) (B : SSet) → SSet
_×_ A B = Σ A (λ _ → B)

data _≡_ (x : A) : A → SSet where
  refl : x ≡ x

_~_ :
  (f g : A → B) →
  SSet lzero
_~_ {A = A} f g = ∀ x → f x ≡ g x

is-equiv : (A → B) → SSet
is-equiv {A = A} {B} f = Σ (B → A) (λ g → (f ∘ g) ~ id) × Σ (B → A) (λ g → (g ∘ f) ~ id)

is-invertible :
  (A → B) → SSet
is-invertible {A = A} {B} f = Σ (B → A) (λ g → ((f ∘ g) ~ id) × ((g ∘ f) ~ id))

module _
   (is-equiv-is-invertible :
      {A : SSet} {B : SSet} {f : A → B} →
      is-invertible f → is-equiv f)
  where

  error :
    is-equiv (id {A → A})
  error = is-equiv-is-invertible ((λ g x → g x) , ((λ x → refl) , (λ x → refl)))
  -- error = is-equiv-is-invertible ((λ g → g) , ((λ x → refl) , (λ x → refl)))
  -- error = is-equiv-is-invertible (id , ((λ x → refl) , (λ x → refl)))

Typechecking this gives

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Constraints.hs:71:11 in Agda-2.6.4.1-LhffR1rONOS7mo6mRdcwS3:Agda.TypeChecking.Constraints

Some comments:

• It typechecks fine with any of the two commented lines.
• It typechecks fine if instead of using sigma types we use records for everything.
• Defining is-equiv-is-invertible doesn't help.
• It typechecks fine if instead of using SSet we use Set.

[FernandoChu]

Wrong repository, sorry.