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.

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