From e2f7d777bb7e4c176e01e1c4f8184f115253dee0 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Mon, 15 Feb 2016 15:51:50 +0000 Subject: A tiny, outright bug in tcDataFamInstDecl This bug was revealed by Trac #11362. It turns out that in my patch for Trac #11148 (namely 1160dc5), I failed to turn one occurrence of tvs' into full_tvs. Sigh. This is tricky stuff and it cost me several hours to page it back in and figure out what was happening. The result was a CoAxiom whose lhs had rhs had different kinds. Eeek! Anyway it's fixed. I also added an ASSERT, in FamInst.newFamInst, that trips on such bogus CoAxioms. --- testsuite/tests/polykinds/T6137.hs | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'testsuite/tests/polykinds') 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 -- cgit v1.2.1