[Haskell-beginners] Structural restrictions in type constructor

[Imants Cekusins]

On 23 June 2015 at 14:54, Kostiantyn Rybnikov <k-bx at k-bx.com> wrote:
> Hi Matt. I don't know how bad is this, but here's what I came up with.
...

this modified for IO version accepts any input, including that which
should have caused error:

or did I do something wrong?


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module PairsMatchedKR where

import GHC.TypeLits

data TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    x1 <- getLine
    x2 <- getLine
    x3 <- getLine
    x4 <- getLine

    print (MyP (tvi x1, tvi x2) (tvi x3, tvi x4))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)


tvi:: String -> TypeValInt (n::Nat)
tvi = TypeValInt . read