<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Hi,</p>
<p>Motivating example: I have an open sum type (Variant, or V) which
can be used to store values of different types:</p>
<p><tt>x,y :: V '[String,Int]</tt><tt><br>
</tt><tt>x = V "test"</tt><tt><br>
</tt><tt>y = V @Int 10</tt></p>
<p><tt>f :: V '[String,Int] -> String</tt><tt><br>
</tt><tt>f = \case</tt><tt><br>
</tt><tt> V s -> "Found string: " ++ s</tt><tt><br>
</tt><tt> V (i :: Int) -> "Found int: " ++ show (i+10)</tt><br>
<br>
</p>
<p><br>
V is a pattern synonym defined like this (you don't need to
understand the details):</p>
<p><tt>pattern V :: forall c cs. (c :< cs) => c -> Variant
cs</tt><tt><br>
</tt><tt>pattern V x <- (fromVariant -> Just x)</tt><tt><br>
</tt><tt> where V x = toVariant x</tt></p>
<p><br>
Where the (:<) constraint checks that we are not doing anything
wrong:</p>
<p><tt>z :: V '[String,Int]</tt><tt><br>
</tt><tt>z = V @Float 10</tt></p>
<p><tt>Test.hs:15:5: error:</tt><tt><br>
</tt><tt> • `Float' is not a member of '[String, Int]</tt><tt><br>
</tt><tt> • In the expression: V @Float 10</tt><tt><br>
</tt><tt> In an equation for ‘z’: z = V @Float 10</tt></p>
<p><tt>f :: V '[String,Int] -> String</tt><tt><br>
</tt><tt>f = \case<br>
...<br>
V (i :: Float) -> "Found float: " ++ show i</tt></p>
<p><tt>Test.hs:20:4: error:</tt><tt><br>
</tt><tt> • `Float' is not a member of '[String, Int]</tt><tt><br>
</tt><tt> • In the pattern: V (i :: Float)</tt><tt><br>
</tt><tt> In a case alternative: V (i :: Float) -> "Found
float: " ++ show i</tt></p>
<p><br>
</p>
<p>So far so good, it works well. Now the issues:<br>
<br>
1) The case-expression in "f" is reported as non-exhaustive</p>
<p>2) We have to disambiguate the type of "10" in the definition of
"y" and in the match "(V (i :: Int))"<br>
</p>
<p><br>
</p>
<p>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".</p>
<p>Would it make sense to add the following built-in "isOneOf"
constraint:<br>
<br>
<span style="font-size: 14px;font-family: verdana, geneva,
sans-serif;">∈ :: k -> [k] ->Constraint</span></p>
<p><tt>pattern V :: forall c cs. (c :< cs, c </tt><tt><span
style="font-size: 14px;font-family: verdana, geneva,
sans-serif;">∈ cs</span>) => c -> Variant cs</tt></p>
<p><tt> </tt><span style="font-size: 14px;">1) GHC could infer
pattern completeness information when the V pattern is used
depending on the type list "cs"<br>
</span></p>
<p><span style="font-size: 14px;">2) GHC might use the "</span><span
style="font-size: 14px;font-family: verdana, geneva,
sans-serif;">c <span style="font-size: 14px;">∈ cs" constraint
in the </span><span style="font-size: 14px;">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'.</span><tt><span style="font-size:
14px;font-family: verdana, geneva, sans-serif;"><br>
</span></tt></span></p>
<p><span style="font-size: 14px;"><span style="font-size: 14px;"><br>
</span></span></p>
<p><span style="font-size: 14px;"><span style="font-size: 14px;">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. </span></span><span
style="font-size: 14px;"><span style="font-size: 14px;"><span
style="font-size: 14px;"><span style="font-size: 14px;">1
seems simpler/safer than 2, though (it is similar to a new
kind of COMPLETE pragma), and it would already be great!</span></span>
Any thoughts?</span></span></p>
<p><span style="font-size: 14px;font-family: verdana, geneva,
sans-serif;"><span style="font-size: 14px;">Best regards,<br>
Sylvain</span><tt><span style="font-size: 14px;font-family:
verdana, geneva, sans-serif;"><br>
</span></tt></span></p>
</body>
</html>