2 Jan
2019
2 Jan
'19
3:38 a.m.
Hi everyone. I'm not so skillful with GADTs and DataKinds, so I assume this mailing list is appropriate to post on. Basically, I wanted to do GADT like this (involving GHC.TypeNats): data Symmetric (n :: Nat) where S1 :: Symmetric 1 (:.) :: (KnownNat n, 2 <= n) => Cyclic n -> Symmetric (n-1) -> Symmetric n But I had some issues with this. The full question is here (on Stack Overflow): https://stackoverflow.com/q/54000646/4540658 Sincerely, Dannyu NDos