<div dir="ltr">Hi all,<br><br>I'm trying to change type-level Nat to Integer as following:<br><div style="margin-left:40px">{-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds #-}<br><br>data Nat = Z | S Nat<br><br>
class NatToInt n where<br>    natToInt :: n -> Int<br><br>instance NatToInt Z where<br>    natToInt _ = 0<br><br>instance NatToInt (S n) where<br>    natToInt = 1 + natToInt (undefined :: n)<br></div><br>I understand why it fails (Z and S have not the right kind).<br>
How to specify that NatToInt is Nat-specific?<br>Moreover, if you have any advanced explanations/links which could give me a deeper understanding on what going on, I'll take them.<br><br>Thanks in advance for your help. <br>
</div>