Type constraint: isOneOf

[Sylvain Henry]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180731/bb0cc092/attachment.html>