Fix type-equality in the type checker (fixes Trac #8553)
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 22 Nov 2013 15:48:02 +0000 (15:48 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 22 Nov 2013 15:50:17 +0000 (15:50 +0000)
For horrible reasons (Note [Comparison with OpenTypeKind] in Type), the
function Type.eqType currently equates OOpenKind with *.  This may or may
not be a good idea (it's certainly a revolting one) but it DOES NOT WORK
in the type checker, which *does* need to distinguish OpenKind and *.

Rather than solve the underlying problem (I have some ideas) I just
introduced a new, and very short, simple, straightforward function
TcType.tcEqType to do the job.

compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcGenDeriv.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcTypeNats.hs
compiler/types/Type.lhs

index 916a6cb..90780a7 100644 (file)
@@ -400,10 +400,10 @@ canIrred d old_ev
     -- get an infinite loop
     something_changed old_ty new_ty1 new_ty2
        | EqPred old_ty1 old_ty2 <- classifyPredType old_ty
-       = not (            new_ty1 `eqType`          old_ty1
-              && typeKind new_ty1 `eqKind` typeKind old_ty1
-              &&          new_ty2 `eqType`          old_ty2
-              && typeKind new_ty2 `eqKind` typeKind old_ty2)
+       = not (            new_ty1 `tcEqType`          old_ty1
+              && typeKind new_ty1 `tcEqKind` typeKind old_ty1
+              &&          new_ty2 `tcEqType`          old_ty2
+              && typeKind new_ty2 `tcEqKind` typeKind old_ty2)
        | otherwise
        = True
 
@@ -494,7 +494,7 @@ flatten :: CtLoc -> FlattenMode
 flatten loc f ctxt ty
   | Just ty' <- tcView ty
   = do { (xi, co) <- flatten loc f ctxt ty'
-       ; if eqType xi ty then return (ty,co) else return (xi,co) }
+       ; if tcEqType xi ty then return (ty,co) else return (xi,co) }
        -- Small tweak for better error messages
 
 flatten _ _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
@@ -717,8 +717,8 @@ emitWorkNC loc evs
 canEqNC :: CtLoc -> CtEvidence -> Type -> Type -> TcS StopOrContinue
 
 canEqNC _loc ev ty1 ty2
-  | eqType ty1 ty2      -- Dealing with equality here avoids
-                        -- later spurious occurs checks for a~a
+  | tcEqType ty1 ty2      -- Dealing with equality here avoids
+                          -- later spurious occurs checks for a~a
   = if isWanted ev then
       setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
     else
@@ -1021,7 +1021,7 @@ reOrient (FunCls {}) _      = False             -- Fun/Other on rhs
 reOrient (VarCls {})   (FunCls {})           = True
 reOrient (VarCls {})   (OtherCls {})         = False
 reOrient (VarCls tv1)  (VarCls tv2)
-  | k1 `eqKind` k2      = tv2 `better_than` tv1
+  | k1 `tcEqKind` k2    = tv2 `better_than` tv1
   | k1 `isSubKind` k2   = True  -- Note [Kind orientation for CTyEqCan]
   | otherwise           = False -- in TcRnTypes
   where
index b7a3f31..1bfbb7f 100644 (file)
@@ -1427,8 +1427,8 @@ gen_Data_binds dflags loc tycon
 
         ------------ gcast1/2
     tycon_kind = tyConKind tycon
-    gcast_binds | tycon_kind `eqKind` kind1 = mk_gcast dataCast1_RDR gcast1_RDR
-                | tycon_kind `eqKind` kind2 = mk_gcast dataCast2_RDR gcast2_RDR
+    gcast_binds | tycon_kind `tcEqKind` kind1 = mk_gcast dataCast1_RDR gcast1_RDR
+                | tycon_kind `tcEqKind` kind2 = mk_gcast dataCast2_RDR gcast2_RDR
                 | otherwise                 = emptyBag
     mk_gcast dataCast_RDR gcast_RDR
       = unitBag (mk_easy_FunBind loc dataCast_RDR [nlVarPat f_RDR]
index 48ac7dd..3e434ab 100644 (file)
@@ -332,7 +332,7 @@ interactIrred :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
 
 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
   | let pred = ctEvPred ev_w
-        (matching_irreds, others) = partitionBag (\ct -> ctPred ct `eqType` pred)
+        (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
                                                  (inert_irreds inerts)
   , (ct_i : rest) <- bagToList matching_irreds
   , let ctev_i = ctEvidence ct_i
@@ -399,7 +399,7 @@ interactGivenIP inerts workItem@(CDictCan { cc_class = cls, cc_tyargs = tys@(ip_
 
     -- Pick out any Given constraints for the same implicit parameter
     is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
-       = isGiven ev && ip_str `eqType` ip_str'
+       = isGiven ev && ip_str `tcEqType` ip_str'
     is_this_ip _ = False
 
 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
@@ -497,7 +497,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
        ; return (Nothing, True) }
 
   | (ev_i : _) <- [ ev_i | CFunEqCan { cc_ev = ev_i, cc_rhs = rhs_i } <- matching_inerts
-                         , rhs_i `eqType` rhs    -- Duplicates
+                         , rhs_i `tcEqType` rhs    -- Duplicates
                          , ev_i `canRewriteOrSame` ev ]
   = do { when (isWanted ev) (setEvBind (ctev_evar ev) (ctEvTerm ev_i))
        ; return (Nothing, True) }
@@ -667,7 +667,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs (inert_eqs inerts) tv
                          , ev_i `canRewriteOrSame` ev
-                         , rhs_i `eqType` rhs ]
+                         , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ b
      -- Work item: a ~ b
     do { when (isWanted ev) (setEvBind (ctev_evar ev) (ctEvTerm ev_i))
@@ -678,7 +678,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs
   , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs (inert_eqs inerts) tv_rhs
                          , ev_i `canRewriteOrSame` ev
-                         , rhs_i `eqType` mkTyVarTy tv ]
+                         , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
     do { when (isWanted ev) (setEvBind (ctev_evar ev)
@@ -1356,7 +1356,7 @@ instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
     der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
 
     do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
-       | eqType sty1 sty2
+       | tcEqType sty1 sty2
        = return ievs -- Return no trivial equalities
        | otherwise
        = do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
@@ -1934,7 +1934,7 @@ matchClassInst inerts clas tys loc
 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
 getCoercibleInst :: Bool -> GlobalRdrEnv -> TcType -> TcType -> TcS LookupInstResult
 getCoercibleInst safeMode rdr_env ty1 ty2
-  | ty1 `eqType` ty2
+  | ty1 `tcEqType` ty2
   = do return $ GenInst []
               $ EvCoercible (EvCoercibleRefl ty1)
 
@@ -1983,7 +1983,7 @@ getCoercibleInst safeMode rdr_env ty1 ty2
 
 nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
 nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
-  where ok (r,t1,t2) = r /= Nominal || t1 `eqType` t2
+  where ok (r,t1,t2) = r /= Nominal || t1 `tcEqType` t2
 
 dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
 dataConsInScope rdr_env tc = not hidden_data_cons
@@ -2005,9 +2005,8 @@ markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
 
 requestCoercible :: TcType -> TcType -> TcS MaybeNew
 requestCoercible ty1 ty2 =
-    ASSERT2( typeKind ty1 `eqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
+    ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
     newWantedEvVar (coercibleClass `mkClassPred` [typeKind ty1, ty1, ty2])
-
 \end{code}
 
 Note [Coercible Instances]
index 78f1be8..d4e737d 100644 (file)
@@ -779,7 +779,7 @@ lookupInInertCans (IS { inert_cans = ics }) pty
   where
     exact_match :: Ct -> Maybe CtEvidence -> Maybe CtEvidence
     exact_match ct deflt | let ctev = ctEvidence ct
-                         , ctEvPred ctev `eqType` pty
+                         , ctEvPred ctev `tcEqType` pty
                          = Just ctev
                          | otherwise
                          = deflt
@@ -1231,7 +1231,7 @@ emitInsoluble ct
       | already_there = is
       | otherwise     = is { inert_cans = ics { inert_insols = extendCts old_insols ct } }
       where
-        already_there = not (isWantedCt ct) && anyBag (eqType this_pred . ctPred) old_insols
+        already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
              -- See Note [Do not add duplicate derived insolubles]
 
 getTcSImplicsRef :: TcS (IORef (Bag Implication))
@@ -1671,7 +1671,7 @@ rewriteCtFlavor (CtDerived {}) new_pred _co
 
 rewriteCtFlavor old_ev new_pred co
   | isTcReflCo co -- If just reflexivity then you may re-use the same variable
-  = return (Just (if ctEvPred old_ev `eqType` new_pred
+  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
                   then old_ev
                   else old_ev { ctev_pred = new_pred }))
        -- Even if the coercion is Refl, it might reflect the result of unification alpha := ty
index 57bf399..21f6cb4 100644 (file)
@@ -519,7 +519,7 @@ simplifyRule name lhs_wanted rhs_wanted
 
              quantify_normal ct
                | EqPred t1 t2 <- classifyPredType (ctPred ct)
-               = not (t1 `eqType` t2)
+               = not (t1 `tcEqType` t2)
                | otherwise
                = True
 
index 0ca8e16..a69b676 100644 (file)
@@ -57,7 +57,7 @@ module TcType (
   -- Predicates.
   -- Again, newtypes are opaque
   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
-  pickyEqType, eqKind,
+  pickyEqType, tcEqType, tcEqKind,
   isSigmaTy, isOverloadedTy,
   isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
@@ -999,6 +999,35 @@ tcInstHeadTyAppAllTyVars ty
 \end{code}
 
 \begin{code}
+tcEqKind :: TcKind -> TcKind -> Bool
+tcEqKind = tcEqType
+
+tcEqType :: TcType -> TcType -> Bool
+-- tcEqType is a proper, sensible type-equality function, that does
+-- just what you'd expect The function Type.eqType (currently) has a
+-- grotesque hack that makes OpenKind = *, and that is NOT what we
+-- want in the type checker!  Otherwise, for example, TcCanonical.reOrient
+-- thinks the LHS and RHS have the same kinds, when they don't, and
+-- fails to re-orient.  That in turn caused Trac #8553.
+
+tcEqType ty1 ty2
+  = go init_env ty1 ty2
+  where
+    init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+    go env t1 t2 | Just t1' <- tcView t1 = go env t1' t2
+                 | Just t2' <- tcView t2 = go env t1 t2'
+    go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
+    go _   (LitTy lit1)        (LitTy lit2)      = lit1 == lit2
+    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go (rnBndr2 env tv1 tv2) t1 t2
+    go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
+    go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
+    go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
+    go _ _ _ = False
+
+    gos _   []       []       = True
+    gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
+    gos _ _ _ = False
+
 pickyEqType :: TcType -> TcType -> Bool
 -- Check when two types _look_ the same, _including_ synonyms.
 -- So (pickyEqType String [Char]) returns False
@@ -1007,6 +1036,7 @@ pickyEqType ty1 ty2
   where
     init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
     go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
+    go _   (LitTy lit1)        (LitTy lit2)      = lit1 == lit2
     go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go (rnBndr2 env tv1 tv2) t1 t2
     go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
     go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
index 7c47658..c19164b 100644 (file)
@@ -6,7 +6,7 @@ module TcTypeNats
 
 import Type
 import Pair
-import TcType     ( TcType )
+import TcType     ( TcType, tcEqType )
 import TyCon      ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..)  )
 import Coercion   ( Role(..) )
 import TcRnTypes  ( Xi )
@@ -323,7 +323,7 @@ matchFamLeq [s,t]
   | Just 0 <- mbX = Just (axLeq0L, [t], bool True)
   | Just x <- mbX, Just y <- mbY =
     Just (axLeqDef, [s,t], bool (x <= y))
-  | eqType s t  = Just (axLeqRefl, [s], bool True)
+  | tcEqType s t  = Just (axLeqRefl, [s], bool True)
   where mbX = isNumLitTy s
         mbY = isNumLitTy t
 matchFamLeq _ = Nothing
@@ -423,40 +423,40 @@ Interaction with inerts
 
 interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertAdd [x1,y1] z1 [x2,y2] z2
-  | sameZ && eqType x1 x2         = [ y1 === y2 ]
-  | sameZ && eqType y1 y2         = [ x1 === x2 ]
-  where sameZ = eqType z1 z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 interactInertAdd _ _ _ _ = []
 
 interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertSub [x1,y1] z1 [x2,y2] z2
-  | sameZ && eqType x1 x2         = [ y1 === y2 ]
-  | sameZ && eqType y1 y2         = [ x1 === x2 ]
-  where sameZ = eqType z1 z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 interactInertSub _ _ _ _ = []
 
 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertMul [x1,y1] z1 [x2,y2] z2
-  | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
-  | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
-  where sameZ   = eqType z1 z2
+  | sameZ && known (/= 0) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (/= 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ   = tcEqType z1 z2
 
 interactInertMul _ _ _ _ = []
 
 interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertExp [x1,y1] z1 [x2,y2] z2
-  | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
-  | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
-  where sameZ = eqType z1 z2
+  | sameZ && known (> 1) x1 && tcEqType x1 x2 = [ y1 === y2 ]
+  | sameZ && known (> 0) y1 && tcEqType y1 y2 = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
 
 interactInertExp _ _ _ _ = []
 
 
 interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
 interactInertLeq [x1,y1] z1 [x2,y2] z2
-  | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
-  | bothTrue && eqType y1 x2                 = [ (x1 <== y2) === bool True ]
-  | bothTrue && eqType y2 x1                 = [ (x2 <== y1) === bool True ]
+  | bothTrue && tcEqType x1 y2 && tcEqType y1 x2 = [ x1 === y1 ]
+  | bothTrue && tcEqType y1 x2                 = [ (x1 <== y2) === bool True ]
+  | bothTrue && tcEqType y2 x1                 = [ (x2 <== y1) === bool True ]
   where bothTrue = isJust $ do True <- isBoolLitTy z1
                                True <- isBoolLitTy z2
                                return ()
index 0805337..4ccd020 100644 (file)
@@ -1160,11 +1160,13 @@ seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 
 \begin{code}
 eqKind :: Kind -> Kind -> Bool
+-- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
 eqKind = eqType
 
 eqType :: Type -> Type -> Bool
 -- ^ Type equality on source types. Does not look through @newtypes@ or
 -- 'PredType's, but it does look through type synonyms.
+-- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
 eqType t1 t2 = isEqual $ cmpType t1 t2
 
 eqTypeX :: RnEnv2 -> Type -> Type -> Bool
@@ -1195,6 +1197,7 @@ Now here comes the real worker
 
 \begin{code}
 cmpType :: Type -> Type -> Ordering
+-- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
 cmpType t1 t2 = cmpTypeX rn_env t1 t2
   where
     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))