<div dir="ltr"><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.<br></span></div><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="gmail-lang-hs gmail-prettyprint gmail-prettyprinted"><code><span class="gmail-kwd">data</span><span class="gmail-pln"> Symmetric </span><span class="gmail-pun">(</span><span class="gmail-pln">n </span><span class="gmail-pun">::</span><span class="gmail-pln"> Nat</span><span class="gmail-pun">)</span><span class="gmail-pln"> </span><span class="gmail-kwd">where</span><span class="gmail-pln">
    S1 </span><span class="gmail-pun">::</span><span class="gmail-pln"> Symmetric </span><span class="gmail-lit">1</span><span class="gmail-pln">
    </span><span class="gmail-pun">(:.)</span><span class="gmail-pln"> </span><span class="gmail-pun">::</span><span class="gmail-pln"> </span><span class="gmail-pun">(</span><span class="gmail-pln">KnownNat n</span><span class="gmail-pun">,</span><span class="gmail-pln"> </span><span class="gmail-lit">2</span><span class="gmail-pln"> </span><span class="gmail-pun"><=</span><span class="gmail-pln"> n</span><span class="gmail-pun">)</span><span class="gmail-pln"> </span><span class="gmail-pun">=></span><span class="gmail-pln"> Cyclic n </span><span class="gmail-pun">-></span><span class="gmail-pln"> Symmetric </span><span class="gmail-pun">(</span><span class="gmail-pln">n</span><span class="gmail-pun">-</span><span class="gmail-lit">1</span><span class="gmail-pun">)</span><span class="gmail-pln"> </span><span class="gmail-pun">-></span><span class="gmail-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">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>