Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T6137.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE GADTs #-}
6
7 module T6137 where
8
9 data Sum a b = L a | R b
10
11 data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
12 LL :: a i -> Sum1 a b (L i)
13 RR :: b i -> Sum1 a b (R i)
14
15 data Code i o = F (Code (Sum i o) o)
16
17 -- An interpretation for `Code` using a data family works:
18 data family In (f :: Code i o) :: (i -> *) -> (o -> *)
19
20 data instance In (F f) r x where
21 MkIn :: In f (Sum1 r (In (F f) r)) x -> In (F f) r x
22
23
24 {- data R:InioFrx o i f r x where
25 where MkIn :: forall o i (f :: Code (Sum i o) o) (r :: i -> *) (x :: o).
26 In (Sum i o) o f (Sum1 o i r (In i o ('F i o f) r)) x
27 -> R:InioFrx o i f r x
28
29 So R:InioFrx :: forall o i. Code i o -> (i -> *) -> o -> *
30
31 data family In i o (f :: Code i o) (a :: i -> *) (b :: o)
32
33 axiom D:R:InioFrx0 ::
34 forall o i (f :: Code (Sum i o) o).
35 In i o ('F i o f) = R:InioFrx o i f
36
37
38 D:R:InioFrx0 :: R:InioFrx o i f ~ In i o ('F i o f)
39 -}
40 -- Requires polymorphic recursion
41 data In' (f :: Code i o) :: (i -> *) -> o -> * where
42 MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t