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