Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / T13910.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TemplateHaskell #-}
7 {-# LANGUAGE Trustworthy #-}
8 {-# LANGUAGE TypeApplications #-}
9 {-# LANGUAGE TypeFamilyDependencies #-}
10 {-# LANGUAGE DataKinds #-}
11 {-# LANGUAGE PolyKinds #-}
12 {-# LANGUAGE TypeOperators #-}
13 module T13910 where
14
15 import Data.Kind
16 import Data.Type.Equality
17
18 data family Sing (a :: k)
19
20 class SingKind k where
21 type Demote k = (r :: Type) | r -> k
22 fromSing :: Sing (a :: k) -> Demote k
23 toSing :: Demote k -> SomeSing k
24
25 data SomeSing k where
26 SomeSing :: Sing (a :: k) -> SomeSing k
27
28 withSomeSing :: forall k r
29 . SingKind k
30 => Demote k
31 -> (forall (a :: k). Sing a -> r)
32 -> r
33 withSomeSing x f =
34 case toSing x of
35 SomeSing x' -> f x'
36
37 data TyFun :: Type -> Type -> Type
38 type a ~> b = TyFun a b -> Type
39 infixr 0 ~>
40
41 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
42 type a @@ b = Apply a b
43 infixl 9 @@
44
45 data FunArrow = (:->) | (:~>)
46
47 class FunType (arr :: FunArrow) where
48 type Fun (k1 :: Type) arr (k2 :: Type) :: Type
49
50 class FunType arr => AppType (arr :: FunArrow) where
51 type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
52
53 type FunApp arr = (FunType arr, AppType arr)
54
55 instance FunType (:->) where
56 type Fun k1 (:->) k2 = k1 -> k2
57
58 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
59
60 instance AppType (:->) where
61 type App k1 (:->) k2 (f :: k1 -> k2) x = f x
62
63 instance FunType (:~>) where
64 type Fun k1 (:~>) k2 = k1 ~> k2
65
66 $(return [])
67
68 instance AppType (:~>) where
69 type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
70
71 infixr 0 -?>
72 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
73
74 data instance Sing (z :: a :~: b) where
75 SRefl :: Sing Refl
76
77 instance SingKind (a :~: b) where
78 type Demote (a :~: b) = a :~: b
79 fromSing SRefl = Refl
80 toSing Refl = SomeSing SRefl
81
82 (~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
83 Sing r
84 -> p @@ Refl
85 -> p @@ r
86 (~>:~:) SRefl pRefl = pRefl
87
88 type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
89 (y :: t) (e :: from :~: y) = App t arr Type p y
90 data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
91 :: forall (y :: t). from :~: y ~> Type
92 type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
93 = WhyReplacePoly arr from p y x
94
95 replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
96 p from
97 -> from :~: to
98 -> p to
99 replace = replacePoly @(:->)
100
101 replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
102 p @@ from
103 -> from :~: to
104 -> p @@ to
105 replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
106
107 replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
108 (p :: (t -?> Type) arr).
109 FunApp arr
110 => App t arr Type p from
111 -> from :~: to
112 -> App t arr Type p to
113 replacePoly from eq =
114 withSomeSing eq $ \(singEq :: Sing r) ->
115 (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
116
117 type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
118 = App t arr Type f a -> App t arr Type f z
119 data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
120 :: t ~> Type
121 type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
122
123 leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
124 (a :: t) (b :: t).
125 FunApp arr
126 => a :~: b
127 -> App t arr Type f a
128 -> App t arr Type f b
129 leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
130
131 leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
132 a :~: b
133 -> f a
134 -> f b
135 leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
136 -- The line above is what you get if you inline the definition of leibnizPoly.
137 -- It causes a panic, however.
138 --
139 -- An equivalent implementation is commented out below, which does *not*
140 -- cause GHC to panic.
141 --
142 -- leibniz = leibnizPoly @(:->)
143
144 leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
145 a :~: b
146 -> f @@ a
147 -> f @@ b
148 leibnizTyFun = leibnizPoly @(:~>) @_ @f