# Type constraint: isOneOf

Tue Jul 31 14:59:26 UTC 2018

```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...