X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=8f25f7e1fa4d9203a2a9c05a394911c34d42dfd2;hp=e0c85202b90b90c8deff4070617ceae27f001608;hb=0dc2b9de4dd4681aa11dfa5419c931a51b274fa6;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516 diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index e0c8520..8f25f7e 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,6 +1,7 @@ \begin{code} module TcCanonical( - mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck + mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, + canEq, canEqLeafTyVarLeft ) where #include "HsVersions.h" @@ -247,16 +248,48 @@ 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, + Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2 + = do { (v1,v2,v3) <- if isWanted fl then + do { v1 <- newWantedCoVar t1a t2a + ; v2 <- newWantedCoVar t1b t2b + ; v3 <- newWantedCoVar t1c t2c + ; let res_co = mkCoPredCo (mkCoVarCoercion v1) + (mkCoVarCoercion v2) (mkCoVarCoercion v3) + ; setWantedCoBind cv res_co + ; return (v1,v2,v3) } + else let co_orig = mkCoVarCoercion cv + coa = mkCsel1Coercion co_orig + cob = mkCsel2Coercion co_orig + coc = mkCselRCoercion co_orig + in do { v1 <- newGivOrDerCoVar t1a t2a coa + ; v2 <- newGivOrDerCoVar t1b t2b cob + ; v3 <- newGivOrDerCoVar t1c t2c coc + ; return (v1,v2,v3) } + ; cc1 <- canEq fl v1 t1a t2a + ; cc2 <- canEq fl v2 t1b t2b + ; cc3 <- canEq fl v3 t1c t2c + ; return (cc1 `andCCan` cc2 `andCCan` cc3) } + -- Split up an equality between function types into two equalities. canEq fl cv (FunTy s1 t1) (FunTy s2 t2) @@ -275,6 +308,34 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) ; cc2 <- canEq fl resv t1 t2 ; return (cc1 `andCCan` cc2) } +canEq fl cv (PredTy p1) (PredTy p2) = canEqPred p1 p2 + where canEqPred (IParam n1 t1) (IParam n2 t2) + | n1 == n2 + = if isWanted fl then + do { v <- newWantedCoVar t1 t2 + ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) + ; canEq fl v t1 t2 } + else return emptyCCan -- DV: How to decompose given IP coercions? + + canEqPred (ClassP c1 tys1) (ClassP c2 tys2) + | c1 == c2 + = if isWanted fl then + do { vs <- zipWithM newWantedCoVar tys1 tys2 + ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) + ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 + } + else return emptyCCan + -- How to decompose given dictionary (and implicit parameter) coercions? + -- You may think that the following is right: + -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) + -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos + -- But this assumes that the coercion is a type constructor-based + -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose + -- to not decompose these coercions. We have to get back to this + -- when we clean up the Coercion API. + + canEqPred p1 p2 = misMatchErrorTcS fl (mkPredTy p1) (mkPredTy p2) + canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) | isAlgTyCon tc1 && isAlgTyCon tc2 @@ -311,9 +372,10 @@ canEq fl cv ty1 ty2 ; cc2 <- canEq fl cv2 t1 t2 ; return (cc1 `andCCan` cc2) } -canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) - | Wanted {} <- fl - = misMatchErrorTcS fl s1 s2 +canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) + | tcIsForAllTy s1, tcIsForAllTy s2, + Wanted {} <- fl + = misMatchErrorTcS fl s1 s2 | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2) ; return emptyCCan } @@ -321,9 +383,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) -- Finally expand any type synonym applications. canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2' - canEq fl _ ty1 ty2 = misMatchErrorTcS fl ty1 ty2 + + \end{code} Note [Equality between type applications] @@ -341,14 +404,6 @@ in Haskell are always same type from different type arguments. -Note [Kinding] -~~~~~~~~~~~~~~ -The canonicalizer assumes that it's provided with well-kinded equalities -as wanted or given, that is LHS kind and the RHS kind agree, modulo subkinding. - -Both canonicalization and interaction solving must preserve this invariant. -DV: TODO TODO: Check! - Note [Canonical ordering for equality constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Implemented as (<+=) below: @@ -442,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 @@ -464,40 +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 (VarCls tv1) (FunCls {}) = not (isMetaTyVar tv1) -reOrient (VarCls {}) (OtherCls {}) = False - --- Variables-variables are oriented according to their kind --- so that the invariant of CTyEqCan 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 (VarCls tv1) (VarCls tv2) - | k1 `eqKind` k2 = False - | otherwise = k1 `isSubKind` k2 - where - k1 = tyVarKind tv1 - k2 = tyVarKind tv2 +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 _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 _untch (VarCls {}) (OtherCls {}) = False +reOrient _untch (VarCls {}) (VarCls {}) = False + +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 @@ -506,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') @@ -518,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 @@ -526,8 +591,10 @@ canEqLeafOriented :: CtFlavor -> CoVar -> TypeClassifier -> TcType -> TcS CanonicalCts -- First argument is not OtherCls canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 - | not (kindAppResult (tyConKind fn) tys `eqKind` typeKind s2 ) - = kindErrorTcS fl (unClassify cls1) s2 + | let k1 = kindAppResult (tyConKind fn) tys, + let k2 = typeKind s2, + 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 @@ -539,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 - | not (k1 `eqKind` k2 || (isMetaTyVar tv && k2 `isSubKind` k1)) - -- Establish the kind invariant for CTyEqCan - = kindErrorTcS fl (mkTyVarTy tv) s2 + = 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 @@ -556,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