Accommodate Derived constraints in two places (fix Trac #8129, #8134)
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 17 Sep 2013 19:55:14 +0000 (20:55 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 18 Sep 2013 12:06:36 +0000 (13:06 +0100)
If we have
   class (F a ~ b) => C a b
then we can produce *derived* CFunEqCans.  These were not being
treated properly in two places:

a) in TcMType.zonkFlats (Trac #8134)
b) in TcSMonad.prepareInertsForImplications (Trac #8129)

This patch fixes both.

compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs

index aa8aa64..93e2f99 100644 (file)
@@ -806,12 +806,12 @@ zonkFlats binds_var untch cts
       , not (isSigTyVar tv) || isTyVarTy ty_lhs     -- Never unify a SigTyVar with a non-tyvar
       , typeKind ty_lhs `tcIsSubKind` tyVarKind tv  -- c.f. TcInteract.trySpontaneousEqOneWay
       , not (tv `elemVarSet` tyVarsOfType ty_lhs)   -- Do not construct an infinite type
-      = ASSERT2( isWantedCt orig_ct, ppr orig_ct )
-        ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
+      = ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
         do { writeMetaTyVar tv ty_lhs
            ; let evterm = EvCoercion (mkTcReflCo ty_lhs)
                  evvar  = ctev_evar (cc_ev zct)
-           ; addTcEvBind binds_var evvar evterm
+           ; when (isWantedCt orig_ct) $         -- Can be derived (Trac #8129)
+             addTcEvBind binds_var evvar evterm
            ; traceTc "zonkFlats/unflattening" $
              vcat [ text "zct = " <+> ppr zct,
                     text "binds_var = " <+> ppr binds_var ]
index 65a6784..1ab7fae 100644 (file)
@@ -732,19 +732,25 @@ prepareInertsForImplications is
                   , inert_funeqs = FamHeadMap funeqs
                   , inert_dicts  = dicts })
       = IC { inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
-           , inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
+           , inert_funeqs = FamHeadMap (foldTM given_from_wanted funeqs emptyTM)
            , inert_irreds = Bag.filterBag isGivenCt irreds
            , inert_dicts  = keepGivenCMap dicts
            , inert_insols = emptyCts }
 
-    given_from_wanted funeq   -- This is where the magic processing happens 
-      | isGiven ev = funeq    -- for type-function equalities
-                              -- See Note [Preparing inert set for implications]
-      | otherwise  = funeq { cc_ev = given_ev }
+    given_from_wanted :: Ct -> TypeMap Ct -> TypeMap Ct
+    given_from_wanted funeq fhm   -- This is where the magic processing happens 
+                                  -- for type-function equalities
+                                  -- See Note [Preparing inert set for implications]
+      | isWanted ev  = insert_one (funeq { cc_ev = given_ev }) fhm
+      | isGiven ev   = insert_one funeq fhm   
+      | otherwise    = fhm  -- Drop derived constraints
       where
         ev = ctEvidence funeq
         given_ev = CtGiven { ctev_evtm = EvId (ctev_evar ev)
                            , ctev_pred = ctev_pred ev }
+
+    insert_one :: Ct -> TypeMap Ct -> TypeMap Ct
+    insert_one funeq fhm = insertTM (funEqHead funeq) funeq fhm 
 \end{code}
 
 Note [Preparing inert set for implications]
@@ -789,6 +795,8 @@ fundep (alpha~a) and this can float out again and be used to fix
 alpha.  (In general we can't float class constraints out just in case
 (C d blah) might help to solve (C Int a).)  But we ignore this possiblity.
 
+For Derived constraints we don't have evidence, so we do not turn
+them into Givens.  There can *be* deriving CFunEqCans; see Trac #8129.
 
 \begin{code}
 getInertEqs :: TcS (TyVarEnv Ct)