X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=8f25f7e1fa4d9203a2a9c05a394911c34d42dfd2;hp=b870b86ed7f0abea72842a746d4ebab544bdccd2;hb=0dc2b9de4dd4681aa11dfa5419c931a51b274fa6;hpb=daa3fb945909feb28d7623aa2a075663d31076f0 diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index b870b86..8f25f7e 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,7 +1,7 @@ \begin{code} module TcCanonical( mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, - canEq + canEq, canEqLeafTyVarLeft ) where #include "HsVersions.h" @@ -248,16 +248,23 @@ canEq fl cv ty1 ty2 -- If one side is a variable, orient and flatten, -- WITHOUT expanding type synonyms, so that we tend to --- substitute a~Age rather than a~Int when type Age=Ing -canEq fl cv (TyVarTy tv1) ty2 = canEqLeaf fl cv (VarCls tv1) (classify ty2) -canEq fl cv ty1 (TyVarTy tv2) = canEqLeaf fl cv (classify ty1) (VarCls tv2) +-- substitute a ~ Age rather than a ~ Int when @type Age = Int@ +canEq fl cv ty1@(TyVarTy {}) ty2 + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (classify ty1) (classify ty2) } +canEq fl cv ty1 ty2@(TyVarTy {}) + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (classify ty1) (classify ty2) } + -- NB: don't use VarCls directly because tv1 or tv2 may be scolems! canEq fl cv (TyConApp fn tys) ty2 | isSynFamilyTyCon fn, length tys == tyConArity fn - = canEqLeaf fl cv (FunCls fn tys) (classify ty2) + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) } canEq fl cv ty1 (TyConApp fn tys) | isSynFamilyTyCon fn, length tys == tyConArity fn - = canEqLeaf fl cv (classify ty1) (FunCls fn tys) + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) } canEq fl cv s1 s2 | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, @@ -490,17 +497,23 @@ inert set is an idempotent subustitution... \begin{code} data TypeClassifier - = VarCls TcTyVar -- Type variable - | FunCls TyCon [Type] -- Type function, exactly saturated - | OtherCls TcType -- Neither of the above + = FskCls TcTyVar -- ^ Flatten skolem + | VarCls TcTyVar -- ^ Non-flatten-skolem variable + | FunCls TyCon [Type] -- ^ Type function, exactly saturated + | OtherCls TcType -- ^ Neither of the above unClassify :: TypeClassifier -> TcType -unClassify (VarCls tv) = TyVarTy tv -unClassify (FunCls fn tys) = TyConApp fn tys -unClassify (OtherCls ty) = ty +unClassify (VarCls tv) = TyVarTy tv +unClassify (FskCls tv) = TyVarTy tv +unClassify (FunCls fn tys) = TyConApp fn tys +unClassify (OtherCls ty) = ty classify :: TcType -> TypeClassifier -classify (TyVarTy tv) = VarCls tv + +classify (TyVarTy tv) + | isTcTyVar tv, + FlatSkol {} <- tcTyVarDetails tv = FskCls tv + | otherwise = VarCls tv classify (TyConApp tc tys) | isSynFamilyTyCon tc , tyConArity tc == length tys = FunCls tc tys @@ -512,43 +525,43 @@ classify ty | Just ty' <- tcView ty = OtherCls ty -- See note [Canonical ordering for equality constraints]. -reOrient :: TypeClassifier -> TypeClassifier -> Bool +reOrient :: Untouchables -> TypeClassifier -> TypeClassifier -> Bool -- (t1 `reOrient` t2) responds True -- iff we should flip to (t2~t1) -- We try to say False if possible, to minimise evidence generation -- -- Postcondition: After re-orienting, first arg is not OTherCls -reOrient (OtherCls {}) (FunCls {}) = True -reOrient (OtherCls {}) (VarCls {}) = True -reOrient (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun +reOrient _untch (OtherCls {}) (FunCls {}) = True +reOrient _untch (OtherCls {}) (FskCls {}) = True +reOrient _untch (OtherCls {}) (VarCls {}) = True +reOrient _untch (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun -reOrient (FunCls {}) (VarCls tv2) = isMetaTyVar tv2 +reOrient _untch (FunCls {}) (VarCls tv2) = isMetaTyVar tv2 -- See Note [No touchables as FunEq RHS] in TcSMonad - -- For convenience we enforce the stronger invariant that no - -- meta type variable is the RHS of a function equality -reOrient (FunCls {}) _ = False -- Fun/Other on rhs +reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs +reOrient _untch (VarCls tv1) (FunCls {}) = not $ isMetaTyVar tv1 + -- Put function on the left, *except* if the RHS becomes + -- a meta-tyvar; see invariant on CFunEqCan + -- and Note [No touchables as FunEq RHS] -reOrient (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1) -reOrient (VarCls {}) (OtherCls {}) = False +reOrient _untch (VarCls tv1) (FskCls {}) = not $ isMetaTyVar tv1 + -- Put flatten-skolems on the left if possible: + -- see Note [Loopy Spontaneous Solving, Example 4] in TcInteract -reOrient (VarCls tv1) (VarCls tv2) = False -{- --- Variables-variables are oriented according to their kind --- so that the following property has the best chance of --- holding: tv ~ xi --- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv --- a skolem, then typeKind xi = typeKind tv +reOrient _untch (VarCls {}) (OtherCls {}) = False +reOrient _untch (VarCls {}) (VarCls {}) = False - | k1 `eqKind` k2 = False - | otherwise = k1 `isSubKind` k2 - where - k1 = tyVarKind tv1 - k2 = tyVarKind tv2 --} +reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2 + -- See Note [Loopy Spontaneous Solving, Example 4] in TcInteract + +reOrient _untch (FskCls {}) (FskCls {}) = False +reOrient _untch (FskCls {}) (FunCls {}) = True +reOrient _untch (FskCls {}) (OtherCls {}) = False ------------------ -canEqLeaf :: CtFlavor -> CoVar +canEqLeaf :: Untouchables + -> CtFlavor -> CoVar -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts -- Canonicalizing "leaf" equality constraints which cannot be -- decomposed further (ie one of the types is a variable or @@ -557,8 +570,8 @@ canEqLeaf :: CtFlavor -> CoVar -- Preconditions: -- * one of the two arguments is not OtherCls -- * the two types are not equal (looking through synonyms) -canEqLeaf fl cv cls1 cls2 - | cls1 `reOrient` cls2 +canEqLeaf untch fl cv cls1 cls2 + | cls1 `re_orient` cls2 = do { cv' <- if isWanted fl then do { cv' <- newWantedCoVar s2 s1 ; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') @@ -569,6 +582,7 @@ canEqLeaf fl cv cls1 cls2 | otherwise = canEqLeafOriented fl cv cls1 s2 where + re_orient = reOrient untch s1 = unClassify cls1 s2 = unClassify cls2 @@ -579,9 +593,8 @@ canEqLeafOriented :: CtFlavor -> CoVar canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 | let k1 = kindAppResult (tyConKind fn) tys, let k2 = typeKind s2, - isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CFunEqCan - = do { kindErrorTcS fl (unClassify cls1) s2 - ; return emptyCCan } + isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan + = kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) ) do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments @@ -593,12 +606,21 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 , cc_rhs = xi2 } ; return $ ccs1 `andCCan` ccs2 `extendCCans` final_cc } --- Otherwise, we have a variable on the left, so we flatten the RHS --- and then do an occurs check. +-- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft +canEqLeafOriented fl cv (FskCls tv) s2 + = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2 + ; return $ ccs `extendCCans` cc } canEqLeafOriented fl cv (VarCls tv) s2 - | isGiven fl && not (k1 `eqKind` k2) -- Establish the kind invariant for CTyEqCan - = do { kindErrorTcS fl (mkTyVarTy tv) s2 - ; return emptyCCan } + = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2 + ; return $ ccs `extendCCans` cc } +canEqLeafOriented _ cv (OtherCls ty1) ty2 + = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2) + +canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS (CanonicalCt, CanonicalCts) +-- Establish invariants of CTyEqCans +canEqLeafTyVarLeft fl cv tv s2 + | isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan + = kindErrorTcS fl (mkTyVarTy tv) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = do { (xi2,ccs2) <- flatten fl s2 -- flatten RHS @@ -610,14 +632,11 @@ canEqLeafOriented fl cv (VarCls tv) s2 , cc_tyvar = tv , cc_rhs = xi2' } - ; return $ ccs2 `extendCCans` final_cc } + ; return $ (final_cc, ccs2) } where k1 = tyVarKind tv k2 = typeKind s2 -canEqLeafOriented _ cv (OtherCls ty1) ty2 - = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2) - -- See Note [Type synonyms and canonicalization]. -- Check whether the given variable occurs in the given type. We may -- have needed to do some type synonym unfolding in order to get rid