Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / typecheck / should_fail / T12648.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE FunctionalDependencies #-}
5 {-# LANGUAGE GADTs #-}
6 {-# LANGUAGE MultiParamTypeClasses #-}
7 {-# LANGUAGE PolyKinds #-}
8 {-# LANGUAGE RankNTypes #-}
9 {-# LANGUAGE ScopedTypeVariables #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE TypeOperators #-}
12 {-# LANGUAGE UndecidableInstances #-}
13 {-# LANGUAGE UndecidableSuperClasses #-}
14 module T12648 where
15
16 import Data.Kind (Type, Constraint)
17 import Unsafe.Coerce (unsafeCoerce)
18
19 type family Skolem (p :: k -> Constraint) :: k
20 type family Forall (p :: k -> Constraint) :: Constraint
21 type instance Forall p = Forall_ p
22 class p (Skolem p) => Forall_ (p :: k -> Constraint)
23 instance p (Skolem p) => Forall_ (p :: k -> Constraint)
24
25 inst :: forall p a. Forall p :- p a
26 inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p))
27
28 data Dict :: Constraint -> Type where
29 Dict :: a => Dict a
30
31 newtype a :- b = Sub (a => Dict b)
32
33 infixl 1 \\ -- required comment
34
35 (\\) :: a => (b => r) -> (a :- b) -> r
36 r \\ Sub Dict = r
37
38 class (Applicative b, Applicative m, Monad b, Monad m) => MonadBase b m | m -> b
39
40 instance MonadBase IO IO -- where liftBase = id
41
42 class MonadBase b m => MonadBaseControl b m | m -> b where
43 type StM m a :: Type
44 liftBaseWith :: (RunInBase m b -> b a) -> m a
45
46 type RunInBase m b = forall a. m a -> b (StM m a)
47
48 instance MonadBaseControl IO IO where
49 type StM IO a = a
50 liftBaseWith f = f id
51 {-# INLINABLE liftBaseWith #-}
52
53 class (StM m a ~ a) => IdenticalBase m a
54 instance (StM m a ~ a) => IdenticalBase m a
55
56 newtype UnliftBase b m = UnliftBase { unliftBase :: forall a. m a -> b a }
57
58 mkUnliftBase :: forall m a b. (Forall (IdenticalBase m), Monad b)
59 => (forall c. m c -> b (StM m c)) -> m a -> b a
60 mkUnliftBase r act = r act \\ (inst :: Forall (IdenticalBase m) :- IdenticalBase m a)
61
62 class (MonadBaseControl b m, Forall (IdenticalBase m)) => MonadBaseUnlift b m | m -> b
63 instance (MonadBaseControl b m, Forall (IdenticalBase m)) => MonadBaseUnlift b m
64
65 askUnliftBase :: forall b m. (MonadBaseUnlift b m) => m (UnliftBase b m)
66 askUnliftBase = liftBaseWith unlifter
67 where
68 unlifter :: (forall c. m c -> b (StM m c)) -> b (UnliftBase b m)
69 unlifter r = return $ UnliftBase (mkUnliftBase r)
70
71 f :: (MonadBaseUnlift m IO) => m a
72 f = do
73
74 _ <- askUnliftBase
75
76 return ()