Suggested pattern signature doesn't account for provided constraints

[sheaf]

It seems that the suggested pattern signature is not always correct in the presence of provided constraints. For instance:

{-# LANGUAGE PatternSynonyms #-}
import GHC.TypeNats

pattern MySomeNat a = SomeNat a

HLS suggests the pattern signature

pattern MySomeNat :: KnownNat n => Proxy n -> SomeNat

which is incorrect, as KnownNat n is not a required constraint (that is needed in order to write down the pattern synonym) but a provided one (which becomes available once pattern matching succeeds).

The pattern signature that HLS should suggest is the following:

pattern MySomeNat :: () => KnownNat n => Proxy n -> SomeNat

which uses the peculiar pattern signature syntax wherein the first set of constraints denotes those that are required, and the second the provided ones.

Another example:

class MyClass (n :: Nat)

pattern MySomeNat1 :: MyClass n => KnownNat n => Proxy n -> SomeNat
pattern MySomeNat1 a = SomeNat a

pattern MySomeNat2 a = MySomeNat1 a

HLS suggests the pattern signature:

pattern MySomeNat2 :: (MyClass n, KnownNat n) => Proxy n -> SomeNat

Not understanding that

pattern MySomeNat2 :: MyClass n => KnownNat n => Proxy n -> SomeNat

means something different.

It seems like there is some logic that rewrites a constraint involving multiple constraint arrows. For instance, if one writes:

{-# LANGUAGE NoMonomorphismRestriction #-}

x :: () => Num a => Ord a => Bounded a => a
x = 1

y = x

Then HLS suggests the following type for y:

y :: (Num a, Ord a, Bounded a) => a

This is obviously fine in this case, but the same rewriting is invalid for pattern signatures.

Version: Haskell Language Server 1.2.0 with GHC 9.0.

[peterwicksstringfield]

Duplicate of #1951; should be fixed by #1952.

This is from a unit test in that PR. I think this covers the use case you have in mind?

ghcide/test/Main.hs

data T1 a where
   MkT1 :: (Show b) => a -> b -> T1 a

pattern MkT1' b = MkT1 42 b

-- And we test that we get this type suggested
-- pattern MkT1' :: (Eq a, Num a) => Show b => b -> T1 a"

Hmm, can you confirm something for me? I think the types here are correct:

data T1 a where
   MkT1 :: (Show b) => a -> b -> T1 a

pattern MkT1' :: (Eq a, Num a) => Show b => b -> T1 a
pattern MkT1' b = MkT1 42 b

y :: (Eq a, Num a, Show b) => b -> T1 a
y x = MkT1' x

y uses MkT1' as an expression and so calling y requires Show b.

[jneira]

@sheaf thanks for report the issue, will close as duplicate if you use case match the test posted above

[sheaf]

Excellent, thanks for your work @peterwicksstringfield. Your solution does indeed cover the situation in the OP.

To answer your other question, in your second example, the type signature you give for y is precisely the one I'd expect GHC to infer. (Technically we don't need the Eq a instance to use MkT1 as a constructor, but we don't have a way of specifying that information when writing a pattern signature).

[peterwicksstringfield]

@sheaf, thanks! Glad we are on the same page.