\begin{code}
module TcCanonical(
- mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck
+ mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck,
+ canEq, canEqLeafTyVarLeft
) where
#include "HsVersions.h"
-- 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)
; 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
; 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 }
-- 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]
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:
\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
= 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
-- 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')
| otherwise
= canEqLeafOriented fl cv cls1 s2
where
+ re_orient = reOrient untch
s1 = unClassify cls1
s2 = unClassify cls2
-> 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 )
- = do { kindErrorTcS fl (unClassify cls1) s2
- ; return emptyCCan }
+ | 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
, 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
- = 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
, 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
projects / ghc-hetmet.git / blobdiff