1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE TypeFamilies #-}
7 module T6137 where
9 data Sum a b = L a | R b
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)
15 data Code i o = F (Code (Sum i o) o)
17 -- An interpretation for `Code` using a data family works:
18 data family In (f :: Code i o) :: (i -> *) -> (o -> *)
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
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
29 So R:InioFrx :: forall o i. Code i o -> (i -> *) -> o -> *
31 data family In i o (f :: Code i o) (a :: i -> *) (b :: o)
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
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