diff options
Diffstat (limited to 'testsuite/tests/polykinds/T6137.hs')
| -rw-r--r-- | testsuite/tests/polykinds/T6137.hs | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/testsuite/tests/polykinds/T6137.hs b/testsuite/tests/polykinds/T6137.hs index dafe9a21e9..aac4c1c8b6 100644 --- a/testsuite/tests/polykinds/T6137.hs +++ b/testsuite/tests/polykinds/T6137.hs @@ -17,9 +17,26 @@ data Code i o = F (Code (Sum i o) o) -- An interpretation for `Code` using a data family works: data family In (f :: Code i o) :: (i -> *) -> (o -> *) -data instance In (F f) r o where - MkIn :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o +data instance In (F f) r x where + MkIn :: In f (Sum1 r (In (F f) r)) x -> In (F f) r x + +{- data R:InioFrx o i f r x where + where MkIn :: forall o i (f :: Code (Sum i o) o) (r :: i -> *) (x :: o). + In (Sum i o) o f (Sum1 o i r (In i o ('F i o f) r)) x + -> R:InioFrx o i f r x + + So R:InioFrx :: forall o i. Code i o -> (i -> *) -> o -> * + + data family In i o (f :: Code i o) (a :: i -> *) (b :: o) + + axiom D:R:InioFrx0 :: + forall o i (f :: Code (Sum i o) o). + In i o ('F i o f) = R:InioFrx o i f + + + D:R:InioFrx0 :: R:InioFrx o i f ~ In i o ('F i o f) +-} -- Requires polymorphic recursion data In' (f :: Code i o) :: (i -> *) -> o -> * where MkIn' :: In' g (Sum1 r (In' (F g) r)) t -> In' (F g) r t |