Update Trac ticket URLs to point to GitLab
[ghc.git] / testsuite / tests / polykinds / T11480b.hs
1 {-# language KindSignatures #-}
2 {-# language PolyKinds #-}
3 {-# language DataKinds #-}
4 {-# language TypeFamilies #-}
5 {-# language RankNTypes #-}
6 {-# language NoImplicitPrelude #-}
7 {-# language FlexibleContexts #-}
8 {-# language MultiParamTypeClasses #-}
9 {-# language GADTs #-}
10 {-# language ConstraintKinds #-}
11 {-# language FlexibleInstances #-}
12 {-# language TypeOperators #-}
13 {-# language ScopedTypeVariables #-}
14 {-# language DefaultSignatures #-}
15 {-# language FunctionalDependencies #-}
16 {-# language UndecidableSuperClasses #-}
17
18 -- This code, supplied by Edward Kmett, uses UndecidableSuperClasses along
19 -- with a bunch of other stuff, so it's a useful stress test.
20 -- See #11480 comment:12.
21
22 module T11480b where
23
24 import Data.Kind (Constraint, Type)
25 import Data.Type.Equality as Equality
26 import Data.Type.Coercion as Coercion
27 import qualified Prelude
28 import Prelude (Either(..))
29
30 newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
31
32 type family Op (p :: i -> j -> Type) :: j -> i -> Type where
33 Op (Y p) = p
34 Op p = Y p
35
36 class Vacuous (p :: i -> i -> Type) (a :: i)
37 instance Vacuous p a
38
39 data Dict (p :: Constraint) where
40 Dict :: p => Dict p
41
42 class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> Type) where
43 type Ob p :: i -> Constraint
44 type Ob p = Vacuous p
45
46 id :: Ob p a => p a a
47 (.) :: p b c -> p a b -> p a c
48
49 source :: p a b -> Dict (Ob p a)
50 default source :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p a)
51 source _ = Dict
52
53 target :: p a b -> Dict (Ob p b)
54 default target :: (Ob p ~ Vacuous p) => p a b -> Dict (Ob p b)
55 target _ = Dict
56
57 op :: p b a -> Op p a b
58 default op :: Op p ~ Y p => p b a -> Op p a b
59 op = Y
60
61 unop :: Op p b a -> p a b
62 default unop :: Op p ~ Y p => Op p b a -> p a b
63 unop = getY
64
65 class (Category p, Category q) =>
66 Functor (p :: i -> i -> Type)
67 (q :: j -> j -> Type)
68 (f :: i -> j) | f -> p q where
69 fmap :: p a b -> q (f a) (f b)
70
71 data Nat (p :: i -> i -> Type)
72 (q :: j -> j -> Type) (f :: i -> j) (g :: i -> j) where
73 Nat :: (Functor p q f, Functor p q g) =>
74 { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g
75
76 instance (Category p, Category q) => Category (Nat p q) where
77 type Ob (Nat p q) = Functor p q
78 id = Nat id1 where
79 id1 :: forall f x. (Functor p q f, Ob p x) => q (f x) (f x)
80 id1 = id \\ (ob :: Ob p x :- Ob q (f x))
81 Nat f . Nat g = Nat (f . g)
82 source Nat{} = Dict
83 target Nat{} = Dict
84
85 ob :: forall p q f a. Functor p q f => Ob p a :- Ob q (f a)
86 ob = Sub (case source (fmap (id :: p a a) :: q (f a) (f a)) of Dict -> Dict)
87
88 instance (Category p, Category q) =>
89 Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where
90 fmap (Y f) = Nat (. f)
91
92 instance (Category p, Category q) => Functor (Nat p q) (->) (Nat p q f) where
93 fmap = (.)
94
95 contramap :: Functor p q f => Op p b a -> q (f a) (f b)
96 contramap = fmap . unop
97
98 instance Category (->) where
99 id = Prelude.id
100 (.) = (Prelude..)
101
102 instance Functor (->) (->) ((->) e) where
103 fmap = (.)
104
105 instance Functor (Y (->)) (Nat (->) (->)) (->) where
106 fmap (Y f) = Nat (. f)
107
108 instance (Category p, Op p ~ Y p) => Category (Y p) where
109 type Ob (Y p) = Ob p
110 id = Y id
111 Y f . Y g = Y (g . f)
112 source (Y f) = target f
113 target (Y f) = source f
114 unop = Y
115 op = getY
116
117 instance (Category p, Op p ~ Y p) => Functor (Y p) (->) (Y p a) where
118 fmap = (.)
119
120 instance (Category p, Op p ~ Y p) => Functor p (Nat (Y p) (->)) (Y p) where
121 fmap f = Nat (. Y f)
122
123 --------------------------------------------------------------------------------
124 -- * Constraints
125 --------------------------------------------------------------------------------
126
127 infixl 1 \\ -- comment required for cpp
128 (\\) :: a => (b => r) -> (a :- b) -> r
129 r \\ Sub Dict = r
130
131 newtype p :- q = Sub (p => Dict q)
132
133 instance Functor (:-) (->) Dict where
134 fmap p Dict = case p of
135 Sub q -> q
136
137 instance Category (:-) where
138 id = Sub Dict
139 f . g = Sub (Dict \\ f \\ g)
140
141 instance Functor (:-) (->) ((:-) e) where
142 fmap = (.)
143
144 instance Functor (Y (:-)) (Nat (:-) (->)) (:-) where
145 fmap (Y f) = Nat (. f)
146
147 --------------------------------------------------------------------------------
148 -- * Common Functors
149 --------------------------------------------------------------------------------
150
151 instance Functor (->) (->) ((,) e) where
152 fmap f ~(a,b) = (a, f b)
153
154 instance Functor (->) (->) (Either e) where
155 fmap _ (Left a) = Left a
156 fmap f (Right b) = Right (f b)
157
158 instance Functor (->) (->) [] where
159 fmap = Prelude.fmap
160
161 instance Functor (->) (->) Prelude.Maybe where
162 fmap = Prelude.fmap
163
164 instance Functor (->) (->) Prelude.IO where
165 fmap = Prelude.fmap
166
167 instance Functor (->) (Nat (->) (->)) (,) where
168 fmap f = Nat (\(a,b) -> (f a, b))
169
170 instance Functor (->) (Nat (->) (->)) Either where
171 fmap f0 = Nat (go f0) where
172 go :: (a -> b) -> Either a c -> Either b c
173 go f (Left a) = Left (f a)
174 go _ (Right b) = Right b
175
176 --------------------------------------------------------------------------------
177 -- * Type Equality
178 --------------------------------------------------------------------------------
179
180 instance Category (:~:) where
181 id = Refl
182 (.) = Prelude.flip Equality.trans
183
184 instance Functor (Y (:~:)) (Nat (:~:) (->)) (:~:) where
185 fmap (Y f) = Nat (. f)
186
187 instance Functor (:~:) (->) ((:~:) e) where
188 fmap = (.)
189
190 --------------------------------------------------------------------------------
191 -- * Type Coercions
192 --------------------------------------------------------------------------------
193
194 instance Category Coercion where
195 id = Coercion
196 (.) = Prelude.flip Coercion.trans
197
198 instance Functor (Y Coercion) (Nat Coercion (->)) Coercion where
199 fmap (Y f) = Nat (. f)
200
201 instance Functor Coercion (->) (Coercion e) where
202 fmap = (.)