dafe9a21e9034e1e7b90b5c0dc1632edb9e07189
[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 o where
21 MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
22
23 -- Requires polymorphic recursion
24 data In' (f :: Code i o) :: (i -> *) -> o -> * where
25 MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t