CTest1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Main where

import           Data.Parameterized.Classes
import           Data.Parameterized.Context
import qualified Data.Parameterized.Context.Unsafe as U

data (Show t) => MyMaybe t = MyJust t | MyNothing
instance ShowF MyMaybe
instance Show (MyMaybe t) where show = showF

type TestCtx = U.EmptyCtx '::> Int '::> String '::> Int '::> Bool

mkUMyMaybe :: U.Assignment MyMaybe TestCtx
mkUMyMaybe = U.generate U.knownSize setMyValue

setMyValue :: U.Index TestCtx tp -> MyMaybe tp
setMyValue idx
  | Just Refl <- testEquality (U.lastIndex U.knownSize) idx = MyJust False
  | Just Refl <- testEquality (U.skipIndex $ U.skipIndex $ U.skipIndex U.baseIndex) idx = MyJust 1
  | Just Refl <- testEquality (U.skipIndex $ U.skipIndex $ U.nextIndex U.knownSize) idx = MyJust "two"
  | Just Refl <- testEquality (U.skipIndex $ U.nextIndex U.knownSize) idx = MyJust 3

main = do putStrLn "start"
          putStrLn $ show $ U.sizeInt (U.size mkUMyMaybe)
          putStrLn $ show mkUMyMaybe
          putStrLn "end"