Constraint solving does not honour singleton types

[plt-amy]

Making a separate bug so I can keep #6071 a discussion. Here's issue #593, now with the latest trendy thing:

“unit” : _
“unit” = Sub Nat i1 λ ._ → 42

“tt” : “unit”
“tt” = inS 42

data _≡ₛ_ {A : SSet} (a : A) : A → SSet where
  reflₛ : a ≡ₛ a

-- demonstrating definitional eta:
_ : ∀ {x y : “unit”} → x ≡ₛ y
_ = reflₛ

refl : ∀ {l} {A : Set l} {x : A} → PathP (λ i → A) x x
refl {x = x} i = x

bla7 : (F : “unit” → Set) ->
  let X : Set
      X = _
  in (z : “unit”) -> PathP (λ i → Set) X (F z)
bla7 F z = refl

Easy fix: isSingletonType' should return Just (x 1=1) when given Sub A i1 x, blocking on the φ argument.

[plt-amy]

Totally off-topic but it's very humbling to revisit an old issue and see that it's just a tad over half my age.

[jespercockx]

Possibly related: #5837

[jespercockx]

@plt-amy I've assigned you and added the 2.6.3 milestone, but feel free to bump it to another one if you don't have the time now.

[plt-amy]

@jespercockx sounds good; I'm fairly sure the solution I sketched works, but I haven't pushed it yet since I'm banned from Actions, so CI doesn't run on my PRs 😔

I've reached out to support but haven't heard anything back, yet.

[jespercockx]

If you can push your branch to here then I can create the PR for you.