Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / polykinds / T11523.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 {-# language UndecidableInstances #-}
18
19 module T11523 where
20
21 import GHC.Types (Constraint, Type)
22 import qualified Prelude
23
24 type Cat i = i -> i -> Type
25
26 newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
27
28 class Vacuous (a :: i)
29 instance Vacuous a
30
31 class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where
32 type Op p :: Cat i
33 type Op p = Y p
34 type Ob p :: i -> Constraint
35 type Ob p = Vacuous
36
37 class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
38 type Dom f :: Cat i
39 type Cod f :: Cat j
40
41 class (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q
42 instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)
43
44 data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)
45
46 instance (Category p, Category q) => Category (Nat p q) where
47 type Ob (Nat p q) = Fun p q
48
49 instance (Category p, Category q) => Functor (Nat p q) where
50 type Dom (Nat p q) = Y (Nat p q)
51 type Cod (Nat p q) = Nat (Nat p q) (->)
52
53 instance (Category p, Category q) => Functor (Nat p q f) where
54 type Dom (Nat p q f) = Nat p q
55 type Cod (Nat p q f) = (->)
56
57 instance Category (->)
58
59 instance Functor ((->) e) where
60 type Dom ((->) e) = (->)
61 type Cod ((->) e) = (->)
62
63 instance Functor (->) where
64 type Dom (->) = Y (->)
65 type Cod (->) = Nat (->) (->)
66
67 instance (Category p, Op p ~ Y p) => Category (Y p) where
68 type Op (Y p) = p
69
70 instance (Category p, Op p ~ Y p) => Functor (Y p a) where
71 type Dom (Y p a) = Y p
72 type Cod (Y p a) = (->)
73
74 instance (Category p, Op p ~ Y p) => Functor (Y p) where
75 type Dom (Y p) = p
76 type Cod (Y p) = Nat (Y p) (->)
77
78
79 {-
80 Given: Category p, Op p ~ Y p
81
82 --> Category p, Op p ~ Y p
83 Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
84
85 --> Category p, Op p ~ Y p
86 Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)
87 Category (Dom p), Category (Cod p)
88 -}