blob: 9a2d0f7354ab3b7cc2d0f92bf353dc3bae91e9ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Main where
import Data.Kind (Type)
import Foreign
import Unsafe.Coerce
data M = A | B deriving (Show, Eq)
newtype S (a :: M) = S Int
data SomeS = forall a . SomeS (S a)
data V0 :: M -> Type where
V0A :: Int -> V0 A
V0B :: Double -> V0 B
data V1 :: M -> Type where
V1A :: Int -> V1 A
V1B :: Double -> V1 B
V1a :: () -> V1 a
viewV0 :: S a -> V0 a
viewV0 (S i)
| even i = unsafeCoerce $ V0A 1
| otherwise = unsafeCoerce $ V0B 2
viewV1 :: S a -> V1 a
viewV1 (S i)
| even i = unsafeCoerce $ V1A 1
| otherwise = unsafeCoerce $ V1B 2
typeOf :: S a -> M
typeOf (S i) = if even i then A else B
cast :: M -> SomeS -> S a
cast ty (SomeS s@(S i))
| ty == typeOf s = S i
| otherwise = error "cast"
test0 :: IO ()
test0 =
let s = cast A (SomeS (S 0))
in case viewV0 s of
V0A{} -> putStrLn "test0 - A"
V0B{} -> putStrLn "test0 - B"
test1 :: IO ()
test1 =
let s = cast A (SomeS (S 2)) :: S A
in case viewV0 s of
V0A{} -> putStrLn "test1 - A"
test2 :: IO ()
test2 =
let s = cast A (SomeS (S 4))
in case viewV1 s of
V1A{} -> putStrLn "test2 - A"
V1B{} -> putStrLn "test2 - B"
V1a{} -> putStrLn "test2 - O_o"
main = do
test0 -- no output at all
test1 -- A
test2 -- O_o
|
