Hi,

Motivating example: I have an open sum type (Variant, or V) which can be used to store values of different types:

x,y :: V '[String,Int]
x = V "test"
y = V @Int 10

f :: V '[String,Int] -> String
f = \case
   V s            -> "Found string: " ++ s
   V (i :: Int)   -> "Found int: " ++ show (i+10)

V is a pattern synonym defined like this (you don't need to understand the details):

pattern V :: forall c cs. (c :< cs) => c -> Variant cs
pattern V x <- (fromVariant -> Just x)
   where V x = toVariant x

Where the (:<) constraint checks that we are not doing anything wrong:

z :: V '[String,Int]
z = V @Float 10

Test.hs:15:5: error:
    • `Float' is not a member of '[String, Int]
    • In the expression: V @Float 10
      In an equation for ‘z’: z = V @Float 10

f :: V '[String,Int] -> String
f = \case
   ...
   V (i :: Float) -> "Found float: " ++ show i

Test.hs:20:4: error:
    • `Float' is not a member of '[String, Int]
    • In the pattern: V (i :: Float)
      In a case alternative: V (i :: Float) -> "Found float: " ++ show i

So far so good, it works well. Now the issues:

1) The case-expression in "f" is reported as non-exhaustive

2) We have to disambiguate the type of "10" in the definition of "y" and in the match "(V (i :: Int))"

Both of these issues are caused by the fact that even with the (c :< cs) constraint, GHC doesn't know/use the fact that the type "c" is really one of the types in "cs".

Would it make sense to add the following built-in "isOneOf" constraint:

∈ :: k -> [k] ->Constraint

pattern V :: forall c cs. (c :< cs, c ∈ cs) => c -> Variant cs

1) GHC could infer pattern completeness information when the V pattern is used depending on the type list "cs"

2) GHC might use the "c ∈ cs" constraint in the last resort to infer "c" if it remains ambiguous: try to type-check with c~c' forall c' in cs and if there is only one valid and unambiguous c', then infer c~c'.

Has it already been considered? I don't know how hard it would be to implement nor if it is sound to add something like this. 1 seems simpler/safer than 2, though (it is similar to a new kind of COMPLETE pragma), and it would already be great! Any thoughts?

Best regards,
Sylvain