A tiny, outright bug in tcDataFamInstDecl
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 15 Feb 2016 15:51:50 +0000 (15:51 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 15 Feb 2016 16:21:52 +0000 (16:21 +0000)
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.

compiler/typecheck/FamInst.hs
compiler/typecheck/TcClassDcl.hs
compiler/typecheck/TcInstDcls.hs
testsuite/tests/polykinds/T6137.hs

index e4b2cc3..c38f163 100644 (file)
@@ -62,7 +62,10 @@ newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
 -- Freshen the type variables of the FamInst branches
 -- Called from the vectoriser monad too, hence the rather general type
 newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
-  = do { (subst, tvs') <- freshenTyVarBndrs tvs
+  = ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
+    ASSERT2( tyCoVarsOfType  rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
+    ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
+    do { (subst, tvs') <- freshenTyVarBndrs tvs
        ; (subst, cvs') <- freshenCoVarBndrsX subst cvs
        ; return (FamInst { fi_fam      = tyConName fam_tc
                          , fi_flavor   = flavor
@@ -73,6 +76,10 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
                          , fi_rhs      = substTy  subst rhs
                          , fi_axiom    = axiom }) }
   where
+    lhs_kind = typeKind (mkTyConApp fam_tc lhs)
+    rhs_kind = typeKind rhs
+    tcv_set  = mkVarSet (tvs ++ cvs)
+    pp_ax    = pprCoAxiom axiom
     CoAxBranch { cab_tvs = tvs
                , cab_cvs = cvs
                , cab_lhs = lhs
index 40da199..1e84e4c 100644 (file)
@@ -467,8 +467,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
 
        ; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
                                               , pprCoAxiom axiom ])
-       ; fam_inst <- ASSERT( tyCoVarsOfType rhs' `subVarSet` tv_set' )
-                     newFamInst SynFamilyInst axiom
+       ; fam_inst <- newFamInst SynFamilyInst axiom
        ; return [fam_inst] }
 
    -- No defaults ==> generate a warning
index a94c102..fdc9e8d 100644 (file)
@@ -671,7 +671,7 @@ tcDataFamInstDecl mb_clsinfo
                  -- (obtained from the pats) are at the end (Trac #11148)
              orig_res_ty          = mkTyConApp fam_tc pats'
 
-       ; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
+       ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
            do { data_cons <- tcConDecls new_or_data
                                         rec_rep_tc
                                         (full_tvs, orig_res_ty) cons
@@ -684,23 +684,23 @@ tcDataFamInstDecl mb_clsinfo
                                              axiom_name eta_tvs [] fam_tc eta_pats
                                              (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                     parent = DataFamInstTyCon axiom fam_tc pats'
-                    kind   = mkPiTypesPreferFunTy tvs' liftedTypeKind
-
+                    rep_tc_kind = mkPiTypesPreferFunTy full_tvs liftedTypeKind
 
                       -- NB: Use the full_tvs from the pats. See bullet toward
                       -- the end of Note [Data type families] in TyCon
-                    rep_tc   = mkAlgTyCon rep_tc_name kind full_tvs
-                                             (map (const Nominal) full_tvs)
-                                             (fmap unLoc cType) stupid_theta
-                                             tc_rhs parent
-                                             Recursive gadt_syntax
+                    rep_tc   = mkAlgTyCon rep_tc_name
+                                          rep_tc_kind
+                                          full_tvs
+                                          (map (const Nominal) full_tvs)
+                                          (fmap unLoc cType) stupid_theta
+                                          tc_rhs parent
+                                          Recursive gadt_syntax
                  -- We always assume that indexed types are recursive.  Why?
                  -- (1) Due to their open nature, we can never be sure that a
                  -- further instance might not introduce a new recursive
                  -- dependency.  (2) They are always valid loop breakers as
                  -- they involve a coercion.
-              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
-              ; return (rep_tc, fam_inst) }
+              ; return (rep_tc, axiom) }
 
          -- Remember to check validity; no recursion to worry about here
        ; checkValidTyCon rep_tc
@@ -712,6 +712,7 @@ tcDataFamInstDecl mb_clsinfo
                                   , di_preds  = preds
                                   , di_ctxt   = tcMkDataFamInstCtxt decl }
 
+       ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
        ; return (fam_inst, m_deriv_info) } }
   where
     eta_reduce :: [Type] -> ([Type], [TyVar])
index dafe9a2..aac4c1c 100644 (file)
@@ -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