blob: 05579f9f09b3e2a38bdc73a298330f782f0af4e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Escape where
data ExpGADT t where
ExpInt :: Int -> ExpGADT Int
data Hidden = forall t . Hidden (ExpGADT t) (ExpGADT t)
hval = Hidden (ExpInt 0) (ExpInt 1)
-- With the type sig this is ok, but without it maybe
-- should be rejected because the result type is wobbly
-- weird1 :: ExpGADT Int
--
-- And indeed it is rejected by GHC 7.8 because OutsideIn
-- doesn't unify under an equality constraint.
weird1 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a
-- Hidden t (ExpInt (co :: t ~ Int) _ :: ExpGADT t) (a :: ExpGADT t)
weird2 :: ExpGADT Int
weird2 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a
|
