Fix #12442.
[ghc.git] / testsuite / tests / dependent / should_compile / T12442.hs
1 -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
2
3 {-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications,
4 GADTs, TypeFamilies, AllowAmbiguousTypes #-}
5
6 module T12442 where
7
8 import Data.Kind
9
10 data family Sing (a :: k)
11 data TyFun :: Type -> Type -> Type
12 type a ~> b = TyFun a b -> Type
13 infixr 0 ~>
14 type family (a :: k1 ~> k2) @@ (b :: k1) :: k2
15
16 data TyCon1 :: (Type -> Type) -> (Type ~> Type)
17 type instance (TyCon1 t) @@ x = t x
18
19 data TyCon2 :: (Type -> Type -> Type) -> (Type ~> Type ~> Type)
20 type instance (TyCon2 t) @@ x = (TyCon1 (t x))
21
22 data TyCon3 :: (Type -> Type -> Type -> Type) -> (Type ~> Type ~> Type ~> Type)
23 type instance (TyCon3 t) @@ x = (TyCon2 (t x))
24
25 type Effect = Type ~> Type ~> Type ~> Type
26
27 data EFFECT :: Type where
28 MkEff :: Type -> Effect -> EFFECT
29
30 data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
31 Here :: EffElem x a (MkEff a x ': xs)
32
33 data instance Sing (elem :: EffElem x a xs) where
34 SHere :: Sing Here
35
36 type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
37 (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
38 UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
39
40 data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type
41
42 effect :: forall e a b t xs prf eff m.
43 Sing (prf :: EffElem e a xs)
44 -> Sing (eff :: e @@ a @@ b @@ t)
45 -> EffM m xs (UpdateResTy b t xs prf eff) t
46 effect = undefined
47
48 data State :: Type -> Type -> Type -> Type where
49 Get :: State a a a
50
51 data instance Sing (e :: State a b c) where
52 SGet :: Sing Get
53
54 type STATE t = MkEff t (TyCon3 State)
55
56 get_ :: forall m x. EffM m '[STATE x] '[STATE x] x
57 get_ = effect @(TyCon3 State) SHere SGet