неожиданный результат генерации кода для case по GADT

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module Main where

import Foreign
import Unsafe.Coerce

-- определение домена значений
data M = A | B deriving (Show, Eq)

-- типизированный доменом значений wrapper
-- в реальной программе враппер вокруг указателя
newtype S (a :: M) = S Int

-- экзестенциальный тип, позволяющий показывать, что
-- реальный тип S не известен на момент компиляции
data SomeS = forall a . SomeS (S a)

-- View тип для S, позволяет просматривать структуру
-- внешнего объекта
data V0 :: M -> * where
  V0A :: Int -> V0 A
  V0B :: Double -> V0 B

-- Другой вариант V, с полиморфным конструктором
-- нужен для демонстрации
data V1 :: M -> * where
  V1A :: Int -> V1 A
  V1B :: Double -> V1 B
  V1a :: () -> V1 a

-- создание View
viewV0 :: S a -> V0 a
viewV0 (S i)
  | even i = unsafeCoerce $ V0A 1
  | otherwise = unsafeCoerce $ V0B 2

-- создание View
viewV1 :: S a -> V1 a
viewV1 (S i)
  | even i = unsafeCoerce $ V1A 1
  | otherwise = unsafeCoerce $ V1B 2

-- определение типа S
typeOf :: S a -> M
typeOf (S i) = if even i then A else B

-- Приведение SomeS к определенному типу.
-- тут в общем-то вся проблема т.к. тип неверный и если
-- его подправить, то все хорошо, но мне интересно
-- поведение при полиморфном результате cast
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 ouput at all
  test1 -- A
  test2 -- O_o