Custom Tactic Block won't work with GHC 9.0

[konn]

Your environment

Which OS do you use: macOS Monterey 12.4

Which LSP client (editor/plugin) do you use: VSCode 1.67.2
GHC: 9.0.2

Describe your project (alternative: link to the project): a simple project with GHC 9.0.2 consisting of the single file:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

module Lib where

data Type1 = A | B
  deriving (Show)

data SType1 (t :: Type1) where
  SA :: SType1 'A
  SB :: SType1 'B

type Eql :: Type1 -> Type1 -> Bool
type family Eql l r where
  Eql 'A 'A = 'True
  Eql 'A 'B = 'False
  Eql 'B 'A = 'False
  Eql 'B 'B = 'True

data SBool (b :: Bool) where
  STrue :: SBool 'True
  SFalse :: SBool 'False

sEql :: SType1 l -> SType1 r -> SBool (Eql l r)
sEql = _

Steps to reproduce

1. Invoke Wingman: use custom tactic block code action at the _ on the RHS of sEql.2.
2. Hover on [wingman||] or open diagnostics.

Expected behaviour

Goals and assumptions must be shown in the diagnostics in [wingman||].
Also, there must be code action Run custom tactic.

Actual behaviour

All of the above are missing and there is Use custom tactic block code action even after one invokes the same code action.

Include debug information

lsp.log

[isovector]

Try enabling the DEBUG flag used by Wingman.Debug (I'm not sure how to enable it, sorry --- maybe just recompile with the debugging stuff in that module not commented out). The log from that will be much more helpful :)

[michaelpj]

Did you figure this one out in the end?