Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T11362.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE GADTs #-}
6
7 module T11362 where
8 -- this file when compiled with -dunique-increment=-1 made GHC crash
9
10 data Sum a b = L a | R b
11
12 data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
13 LL :: a i -> Sum1 a b (L i)
14 RR :: b i -> Sum1 a b (R i)
15
16 data Code i o = F (Code (Sum i o) o)
17
18 -- An interpretation for `Code` using a data family works:
19 data family In (f :: Code i o) :: (i -> *) -> (o -> *)
20
21 data instance In (F f) r o where
22 MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o
23
24 -- Requires polymorphic recursion
25 data In' (f :: Code i o) :: (i -> *) -> o -> * where
26 MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t