Type applications in patterns should also work for universal type variables

Consider

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}

module Lib where

import Data.Void

data SMaybe a
  = SNothing
  | SJust !a
  deriving Read

foo :: Read a => (SMaybe a -> r) -> String -> r
foo f s = f (read s)

bar :: _
bar = foo (\(SNothing @Void) -> 42 :: Int) "SNothing"

This compiles and infers bar :: Int on HEAD. Nice!

But it doesn't seem to work in the presence of a type index:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

module Lib where

data SBool (b :: Bool) where
  STrue :: forall b. (b ~ 'True) => SBool b
  SFalse :: forall b. (b ~ 'False) => SBool b

class Blah b where
  blah :: SBool b

instance Blah 'True where
  blah = STrue

foo :: Blah b => (SBool b -> Int) -> Int
foo f = f blah

bar = foo (\(STrue @True) -> 42)

Error:

test.hs:24:7: error:
    • Ambiguous type variable ‘b0’ arising from a use of ‘foo’
      prevents the constraint ‘(Blah b0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘b0’ should be.
      These potential instance exist:
        instance Blah 'True -- Defined at test.hs:18:10
    • In the expression: foo (\ (STrue @True) -> 42)
      In an equation for ‘bar’: bar = foo (\ (STrue @True) -> 42)
   |
24 | bar = foo (\(STrue @True) -> 42)
   |       ^^^

Here, I expect the specification of @True in the STrue pattern to refine the universal type variable b of the SBool constructor, so that the type of the match is inferred to be SBool 'True. This means I have to write STrue :: SBool 'True.

I believe what happens is that the type variable b of STrue counts as an existential type variable. What a shame. I had hoped that https://dl.acm.org/doi/pdf/10.1145/3242744.3242753 somehow got rid of this distinction.

I feel like I want a bidirectional flow of information (@True informing the match type, the provided constraints of STrue informing any type variables in the match), like unification, instead of just matching the existentially bound var b against the type application in the pattern True and check whether that constraint (b ~ True) is satisfiable.

This was all inspired by https://mail.haskell.org/pipermail/ghc-devs/2021-March/019703.html.