<div dir="ltr">This question has been answered on Stack Overflow.<br></div><br><div class="gmail_quote"><div dir="ltr">2019년 1월 2일 (수) 오후 5:48, Dannyu NDos <<a href="mailto:ndospark320@gmail.com">ndospark320@gmail.com</a>>님이 작성:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><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="gmail-m_8211933256131520767m_669783419619177487gmail-lang-hs gmail-m_8211933256131520767m_669783419619177487gmail-prettyprint gmail-m_8211933256131520767m_669783419619177487gmail-prettyprinted"><code><span class="gmail-m_8211933256131520767m_669783419619177487gmail-kwd">data</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> Symmetric </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">(</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln">n </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">::</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> Nat</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">)</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-kwd">where</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln">
    S1 </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">::</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> Symmetric </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-lit">1</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln">
    </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">(:.)</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">::</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">(</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln">KnownNat n</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">,</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-lit">2</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun"><=</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> n</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">)</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">=></span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> Cyclic n </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">-></span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> Symmetric </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">(</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln">n</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">-</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-lit">1</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">)</span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pln"> </span><span class="gmail-m_8211933256131520767m_669783419619177487gmail-pun">-></span><span class="gmail-m_8211933256131520767m_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>
</blockquote></div>