Commit 985663ea authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix type-equality in the type checker (fixes Trac #8553)

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.
parent 7db23406
......@@ -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
......
......@@ -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]
......
......@@ -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]
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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 ()
......
......@@ -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))
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment