<div dir="ltr"><div><span style="font-family:monospace,monospace">(Message re-sent)<br></span></div><div><span style="font-family:monospace,monospace">Hi everyone. I'm not so skillful with GADTs and DataKinds, so I assume this mailing list is appropriate to post on.</span></div><div><span style="font-family:monospace,monospace"></span></div><div class="gmail_quote"><div dir="ltr"><div><span style="font-family:monospace,monospace"><br></span></div><div><span style="font-family:monospace,monospace">Basically, I wanted to do GADT like this<code> (involving GHC.TypeNats):</code></span></div><div><pre class="m_669783419619177487gmail-lang-hs m_669783419619177487gmail-prettyprint m_669783419619177487gmail-prettyprinted"><code><span class="m_669783419619177487gmail-kwd">data</span><span class="m_669783419619177487gmail-pln"> Symmetric </span><span class="m_669783419619177487gmail-pun">(</span><span class="m_669783419619177487gmail-pln">n </span><span class="m_669783419619177487gmail-pun">::</span><span class="m_669783419619177487gmail-pln"> Nat</span><span class="m_669783419619177487gmail-pun">)</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-kwd">where</span><span class="m_669783419619177487gmail-pln">
    S1 </span><span class="m_669783419619177487gmail-pun">::</span><span class="m_669783419619177487gmail-pln"> Symmetric </span><span class="m_669783419619177487gmail-lit">1</span><span class="m_669783419619177487gmail-pln">
    </span><span class="m_669783419619177487gmail-pun">(:.)</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-pun">::</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-pun">(</span><span class="m_669783419619177487gmail-pln">KnownNat n</span><span class="m_669783419619177487gmail-pun">,</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-lit">2</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-pun"><=</span><span class="m_669783419619177487gmail-pln"> n</span><span class="m_669783419619177487gmail-pun">)</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-pun">=></span><span class="m_669783419619177487gmail-pln"> Cyclic n </span><span class="m_669783419619177487gmail-pun">-></span><span class="m_669783419619177487gmail-pln"> Symmetric </span><span class="m_669783419619177487gmail-pun">(</span><span class="m_669783419619177487gmail-pln">n</span><span class="m_669783419619177487gmail-pun">-</span><span class="m_669783419619177487gmail-lit">1</span><span class="m_669783419619177487gmail-pun">)</span><span class="m_669783419619177487gmail-pln"> </span><span class="m_669783419619177487gmail-pun">-></span><span class="m_669783419619177487gmail-pln"> Symmetric n</span></code></pre><span style="font-family:monospace,monospace"><code></code></span></div><div><span style="font-family:monospace,monospace"><code>But I had some issues with this. The full question is here (on Stack Overflow):<br></code></span></div><div><span style="font-family:monospace,monospace"><code><br></code></span></div><div dir="ltr"><span style="font-family:monospace,monospace"><a href="https://stackoverflow.com/q/54000646/4540658" target="_blank">https://stackoverflow.com/q/54000646/4540658</a></span></div><div dir="ltr"><span style="font-family:monospace,monospace"><br></span></div><div><span style="font-family:monospace,monospace">Sincerely,</span></div><div><span style="font-family:monospace,monospace">Dannyu NDos<br></span></div><span style="font-family:monospace,monospace"></span></div>
</div></div>