<div dir="ltr">Hello,<div><br></div><div style>the following programs seems to hit either some limitation of GHC or maybe I'm just missing something and it behaves the intended way.</div><div style><br></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px">
<div style><div style><div style><font face="courier new, monospace">{-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds, GADTs #-}</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br>
</font></div></div></div><div style><div style><div style><font face="courier new, monospace">module Test where</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br></font></div>
</div></div><div style><div style><div style><font face="courier new, monospace">import Data.Singletons</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br></font></div></div>
</div>
<div style><div style><div style><font face="courier new, monospace">data TA = CA</font></div></div></div><div style><div style><div style><font face="courier new, monospace">data TB = CB</font></div></div></div><div style>
<div style><div style><font face="courier new, monospace">data TC = CC (Either TA TB)</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br></font></div></div></div><div style><div style>
<div style><font face="courier new, monospace">$(genSingletons [''TA, ''TB, ''TC])</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br></font></div></div>
</div><div style><div style><div style><font face="courier new, monospace">type family Output (x :: TC) :: *</font></div></div></div><div style><div style><div style><font face="courier new, monospace">type instance Output ('CC ('Left 'CA)) = Int</font></div>
</div></div><div style><div style><div style><font face="courier new, monospace">type instance Output ('CC ('Right 'CB)) = String</font></div></div></div><div style><div style><div style><font face="courier new, monospace"><br>
</font></div></div></div><div style><div style><div style><font face="courier new, monospace">f :: Sing (a :: TC) -> Output a</font></div></div></div><div style><div style><div style><font face="courier new, monospace">f (SCC (SLeft SCA)) = 1</font></div>
</div></div><div style><div style><div style><font face="courier new, monospace"><br></font></div></div></div><div style><div style><div style><font face="courier new, monospace">g :: Sing (a :: TC) -> Output a</font></div>
</div></div><div style><div style><div style><font face="courier new, monospace">g (SCC (SLeft _)) = 1</font></div></div></div></blockquote><div style><div><font face="courier new, monospace"><br></font></div>Function f typechecks as expected. Function g fails to typecheck with the following error.</div>
<div style><font face="courier new, monospace"><br></font></div><div style><div><div><font face="courier new, monospace"> Could not deduce (Num (Output ('CC ('Left TA TB n0))))</font></div><div><font face="courier new, monospace"> arising from the literal `1'</font></div>
<div><font face="courier new, monospace"> from the context (a ~ 'CC n, SingRep (Either TA TB) n)</font></div><div><font face="courier new, monospace"> bound by a pattern with constructor</font></div><div><font face="courier new, monospace"> SCC :: forall (a_a37R :: TC) (n_a37S :: Either TA TB).</font></div>
<div><font face="courier new, monospace"> (a_a37R ~ 'CC n_a37S, SingRep (Either TA TB) n_a37S) =></font></div><div><font face="courier new, monospace"> Sing (Either TA TB) n_a37S -> Sing TC a_a37R,</font></div>
<div><font face="courier new, monospace"> in an equation for `g'</font></div><div><font face="courier new, monospace"> at Test.hs:21:4-16</font></div><div><font face="courier new, monospace"> or from (n ~ 'Left TA TB n0,</font></div>
<div><font face="courier new, monospace"> SingRep TA n0,</font></div><div><font face="courier new, monospace"> SingKind TA ('KindParam TA))</font></div><div><font face="courier new, monospace"> bound by a pattern with constructor</font></div>
<div><font face="courier new, monospace"> SLeft :: forall (a0 :: BOX)</font></div><div><font face="courier new, monospace"> (b0 :: BOX)</font></div><div><font face="courier new, monospace"> (a1 :: Either a0 b0)</font></div>
<div><font face="courier new, monospace"> (n0 :: a0).</font></div><div><font face="courier new, monospace"> (a1 ~ 'Left a0 b0 n0, SingRep a0 n0,</font></div><div>
<font face="courier new, monospace"> SingKind a0 ('KindParam a0)) =></font></div><div><font face="courier new, monospace"> Sing a0 n0 -> Sing (Either a0 b0) a1,</font></div>
<div><font face="courier new, monospace"> in an equation for `g'</font></div><div><font face="courier new, monospace"> at Test.hs:21:9-15</font></div><div><font face="courier new, monospace"> Possible fix:</font></div>
<div><font face="courier new, monospace"> add an instance declaration for</font></div><div><font face="courier new, monospace"> (Num (Output ('CC ('Left TA TB n0))))</font></div><div><font face="courier new, monospace"> In the expression: 1</font></div>
<div><font face="courier new, monospace"> In an equation for `g': g (SCC (SLeft _)) = 1</font></div></div><div><br></div><div><br></div><div style>I would expect that<font face="courier new, monospace"> a ~ ('CC ('Left 'CA))</font> in the right hand-side of <span style="font-family:monospace">g (SCC (SLeft _)) = 1</span> since SLeft's argument is necessarily of type STA, whose sole inhabitant is SA.</div>
<div style><br></div><div style>Now I understand (looking at -ddump-slices, the singletons' library paper and the error message) that the definition of SCC and SLeft don't immediately imply what I just wrote above. So my question is: in the right hand-side of <span style="font-family:monospace">g (SCC (SLeft _)) = 1,</span></div>
<div style><ul style><li style>is <font face="courier new, monospace">a ~ ('CC ('Left 'CA)) </font>a consequence of the definitions of SCC, SLeft, ... (in which case GHC could infer it but for some reason can't)</li>
<li style>or are these pattern + definitions not sufficient to prove that <span style="font-family:monospace">a ~ ('CC ('Left 'CA))</span><font face="arial, helvetica, sans-serif"> no matter what?</font></li>
</ul>
</div>Cheers,<br>Paul</div></div>