Lower precedence for {-# UNPACK #-}
[ghc.git] / testsuite / tests / typecheck / should_fail / T14350.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeApplications #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# LANGUAGE PolyKinds, DataKinds #-}
9 {-# LANGUAGE TypeOperators #-}
10 module T14350 where
11
12 import Data.Kind
13
14 data Proxy a = Proxy
15 data family Sing (a :: k)
16
17 data SomeSing k where
18 SomeSing :: Sing (a :: k) -> SomeSing k
19
20 class SingKind k where
21 type Demote k :: Type
22 fromSing :: Sing (a :: k) -> Demote k
23 toSing :: Demote k -> SomeSing k
24
25 data instance Sing (x :: Proxy k) where
26 SProxy :: Sing 'Proxy
27
28 instance SingKind (Proxy k) where
29 type Demote (Proxy k) = Proxy k
30 fromSing SProxy = Proxy
31 toSing Proxy = SomeSing SProxy
32
33 data TyFun :: Type -> Type -> Type
34 type a ~> b = TyFun a b -> Type
35 infixr 0 ~>
36
37 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
38 type a @@ b = Apply a b
39 infixl 9 @@
40
41 newtype instance Sing (f :: k1 ~> k2) =
42 SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
43
44 instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
45 type Demote (k1 ~> k2) = Demote k1 -> Demote k2
46 fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
47 toSing = undefined
48
49 dcomp :: forall (a :: Type)
50 (b :: a ~> Type)
51 (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
52 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
53 (g :: forall (x :: a). Proxy x ~> b @@ x)
54 (x :: a).
55 Sing f
56 -> Sing g
57 -> Sing x
58 -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
59 dcomp f g x = applySing f Proxy Proxy