Overlapping instances via Nat-kind

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Overlapping instances via Nat-kind

Dannyu NDos
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):


Sincerely,
Dannyu NDos

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Fwd: Overlapping instances via Nat-kind

Dannyu NDos
(Message re-sent)
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):


Sincerely,
Dannyu NDos

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Overlapping instances via Nat-kind

Dannyu NDos
This question has been answered on Stack Overflow.

2019년 1월 2일 (수) 오후 5:48, Dannyu NDos <[hidden email]>님이 작성:
(Message re-sent)
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):


Sincerely,
Dannyu NDos

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners