type signature code lens required vs provided constraints

[peterwicksstringfield]

The TypeLens plugin tries to produce code lenses suggesting type signatures for pattern synonyms like:

pattern Some x = Just x

But it's not doing the right thing to get the type. See ghcide/src/Development/IDE/Plugin/TypeLenses.hs line 283.

            ty = fromJust $ lookupTypeEnv (tcg_type_env gblEnv) name >>= safeTyThingType

safeTyThingType returns Nothing for unidirectional pattern synonyms. It is trying to get the type of the "builder" function. But a unidirectional pattern synonym doesn't have one. So this causes the type lens plugin to crash:

pattern Some x <- Just x

E.g.:

LSP logs stderr:

Module "/home/peter/Notes/2021june21_pattern_synonyms/a" is loaded by Cradle: Cradle {cradleRootDir = "/home/peter/Notes/2021june21_pattern_synonyms", cradleOptsProg = CradleAction: Cabal}
Run entered for haskell-language-server-wrapper(haskell-language-server-wrapper) Version 0.4.0.0, Git revision 0a18edde24923251a148cbbc0ae993a6aac83b9c (dirty) x86_64 ghc-8.10.1
Current directory: /home/peter/Notes/2021june21_pattern_synonyms
Operating system: linux
Arguments: ["--lsp","-d","-l","/tmp/hls.log"]
Cradle directory: /home/peter/Notes/2021june21_pattern_synonyms
Cradle type: Cabal

Tool versions found on the $PATH
cabal:		3.4.0.0
stack:		2.5.1
ghc:		8.10.5


Consulting the cradle to get project GHC version...
Project GHC version: 8.10.5
haskell-language-server exe candidates: ["haskell-language-server-8.10.5","haskell-language-server-8.10","haskell-language-server"]
Launching haskell-language-server exe at:/home/peter/.ghcup/bin/haskell-language-server-8.10.5
haskell-language-server version: 1.2.0.0 (GHC: 8.10.5) (PATH: /home/peter/.ghcup/bin/haskell-language-server-8.10.5~1.2.0) (GIT hash: be2071e985cb417f984ab00a1aad76dee02d6d0b)
Starting (haskell-language-server)LSP server...
  with arguments: GhcideArguments {argsCommand = LSP, argsCwd = Nothing, argsShakeProfiling = Nothing, argsTesting = False, argsExamplePlugin = False, argsDebugOn = True, argsLogFile = Just "/tmp/hls.log", argsThreads = 0, argsProjectGhcVersion = False}
  with plugins: [PluginId "pragmas",PluginId "floskell",PluginId "fourmolu",PluginId "tactics",PluginId "ormolu",PluginId "stylish-haskell",PluginId "retrie",PluginId "brittany",PluginId "class",PluginId "haddockComments",PluginId "eval",PluginId "importLens",PluginId "refineImports",PluginId "moduleName",PluginId "hlint",PluginId "splice",PluginId "ghcide-hover-and-symbols",PluginId "ghcide-code-actions-imports-exports",PluginId "ghcide-code-actions-type-signatures",PluginId "ghcide-code-actions-bindings",PluginId "ghcide-code-actions-fill-holes",PluginId "ghcide-completions",PluginId "ghcide-type-lenses",PluginId "ghcide-core"]
  in directory: /home/peter/Notes/2021june21_pattern_synonyms
 Starting LSP server...
If you are seeing this in a terminal, you probably should have run WITHOUT the --lsp option!
Started LSP server in 0.00s
setInitialDynFlags cradle: Cradle {cradleRootDir = "/home/peter/Notes/2021june21_pattern_synonyms", cradleOptsProg = CradleAction: Cabal}
Output from setting up the cradle Cradle {cradleRootDir = "/home/peter/Notes/2021june21_pattern_synonyms", cradleOptsProg = CradleAction: Cabal}
> Build profile: -w ghc-8.10.5 -O1
> In order, the following will be built (use -v for more details):
>  - 2021june21-pattern-synonyms-0.1.0.0 (exe:2021june21-pattern-synonyms) (first run)
> Preprocessing executable '2021june21-pattern-synonyms' for 2021june21-pattern-synonyms-0.1.0.0..
haskell-language-server-8.10.5: Maybe.fromJust: Nothing
CallStack (from HasCallStack):
  error, called at libraries/base/Data/Maybe.hs:148:21 in base:Data.Maybe
  fromJust, called at src/Development/IDE/Plugin/TypeLenses.hs:283:18 in ghcide-1.4.0.0-inplace:Development.IDE.Plugin.TypeLenses

But even for pattern synonyms that do have builders, that's still not the type we want. Consider this next example from the GHC docs:

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html#typing-of-pattern-synonyms

data T a where
  MkT :: (Show b) => a -> b -> T a

f0 :: (Num a, Eq a) => T a -> String
f0 (MkT 42 x) = show x

pattern ExNumPat1 :: (Num a, Eq a) => (Show b) => b -> T a
pattern ExNumPat1 x = MkT 42 x

f1 :: (Eq a, Num a) => T a -> String
f1 (ExNumPat1 x) = show x

-- pattern ExNumPat2 :: (Eq a, Num a, Show b) => b -> T a
pattern ExNumPat2 x = MkT 42 x

The code-lens plugin suggests

pattern ExNumPat2 :: (Eq a, Num a, Show b) => b -> T a

as the type signature for ExNumPat2. This is the wrong type, and it will not typecheck. The right type is the one shown on ExNumPat1.

For pattern synonyms, the first (Num a, Eq a) => is the constraints required to use the pattern. The second (Show b) => is the constraints provided in the body of the match. My understanding is that this means that pattern synonyms types can't actually fit in the datatype Type.

The "matchers" associated with type synonyms have types of their own, but we don't want those either.

Here are some comparisons:

pattern Some a = Just a
pattern Some :: a -> Maybe a
builder :: a -> Maybe a
matcher :: Maybe a -> (a -> r) -> (ghc-prim-0.6.1:GHC.Prim.Void# -> r) -> r

pattern Some a <- Just a
pattern Some :: a -> Maybe a,
--builder ::
matcher :: Maybe a -> (a -> r) -> (ghc-prim-0.6.1:GHC.Prim.Void# -> r) -> r

pattern MkT1' b = MkT1 42 b
pattern MkT1' :: (Eq a, Num a) => Show b => b -> T1 a
builder :: (Eq a, Num a, Show b) => b -> T1 a
matcher :: (Eq a, Num a) => T1 a -> (forall b. Show b => b -> r) -> (ghc-prim-0.6.1:GHC.Prim.Void# -> r) -> r

Your environment

peter@gtower:~/Notes/2021june20_pattern_synonyms$ haskell-language-server-wrapper --probe-tools
haskell-language-server version: 1.2.0.0 (GHC: 8.10.4) (PATH: /home/peter/.ghcup/bin/haskell-language-server-wrapper-1.2.0) (GIT hash: be2071e985cb417f984ab00a1aad76dee02d6d0b)
Tool versions found on the $PATH
cabal:		3.4.0.0
stack:		2.7.1
ghc:		8.10.5

Ubuntu

emacs