-- Canonical constraints
CanonicalCts, emptyCCan, andCCan, andCCans,
- singleCCan, extendCCans, isEmptyCCan,
+ singleCCan, extendCCans, isEmptyCCan, isEqCCan,
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals,
mkWantedConstraints, deCanonicaliseWanted,
makeGivens, makeSolved,
- CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
+ CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve,
combineCtLoc, mkGivenFlavor,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
import TcRnTypes
-import Control.Monad
import Data.IORef
\end{code}
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
-- * tv not in tvs(xi) (occurs check)
- -- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
- -- a skolem, then typeKind xi = typeKind tv
+ -- * If constraint is given then typeKind xi == typeKind tv
+ -- See Note [Spontaneous solving and kind compatibility]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar,
-- Invariant: * isSynFamilyTyCon cc_fun
-- * cc_rhs is not a touchable unification variable
-- See Note [No touchables as FunEq RHS]
- -- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+ -- * If constraint is given then
+ -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
isEmptyCCan :: CanonicalCts -> Bool
isEmptyCCan = isEmptyBag
+
+isEqCCan :: CanonicalCt -> Bool
+isEqCCan (CTyEqCan {}) = True
+isEqCCan (CFunEqCan {}) = True
+isEqCCan _ = False
+
\end{code}
%************************************************************************
isDerived (Derived {}) = True
isDerived _ = False
+canSolve :: CtFlavor -> CtFlavor -> Bool
+-- canSolve ctid1 ctid2
+-- The constraint ctid1 can be used to solve ctid2
+-- "to solve" means a reaction where the active parts of the two constraints match.
+-- active(F xis ~ xi) = F xis
+-- active(tv ~ xi) = tv
+-- active(D xis) = D xis
+-- active(IP nm ty) = nm
+-----------------------------------------
+canSolve (Given {}) _ = True
+canSolve (Derived {}) (Wanted {}) = True
+canSolve (Derived {}) (Derived {}) = True
+canSolve (Wanted {}) (Wanted {}) = True
+canSolve _ _ = False
+
canRewrite :: CtFlavor -> CtFlavor -> Bool
-- canRewrite ctid1 ctid2
--- The constraint ctid1 can be used to rewrite ctid2
-canRewrite (Given {}) _ = True
-canRewrite (Derived {}) (Wanted {}) = True
-canRewrite (Derived {}) (Derived {}) = True
-canRewrite (Wanted {}) (Wanted {}) = True
-canRewrite _ _ = False
+-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
+canRewrite = canSolve
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted
pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
isTouchableMetaTyVar :: TcTyVar -> TcS Bool
--- is touchable variable!
isTouchableMetaTyVar tv
- | isMetaTyVar tv = do { untch <- getUntouchables
- ; return (inTouchableRange untch tv) }
- | otherwise = return False
+ = case tcTyVarDetails tv of
+ MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables]
+ MetaTv {} -> do { untch <- getUntouchables
+ ; return (inTouchableRange untch tv) }
+ _ -> return False
+\end{code}
+
+Note [Touchable meta type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Meta type variables allocated *by the constraint solver itself* are always
+touchable. Example:
+ instance C a b => D [a] where...
+if we use this instance declaration we "make up" a fresh meta type
+variable for 'b', which we must later guess. (Perhaps C has a
+functional dependency.) But since we aren't in the constraint *generator*
+we can't allocate a Unique in the touchable range for this implication
+constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable.
+\begin{code}
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
- where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
- newFlattenSkolemTyVar ty
- = wrapTcS $ do { uniq <- TcM.newUnique
- ; let name = mkSysTvName uniq (fsLit "f")
- ; return $
- mkTcTyVar name (typeKind ty) (FlatSkol ty)
- }
+
+newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
+newFlattenSkolemTyVar ty
+ = wrapTcS $ do { uniq <- TcM.newUnique
+ ; let name = mkSysTvName uniq (fsLit "f")
+ ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
-instDFunTypes mb_inst_tys =
- let inst_tv :: Either TyVar TcType -> TcS Type
- inst_tv (Left tv) = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
- inst_tv (Right ty) = return ty
- in mapM inst_tv mb_inst_tys
-
+instDFunTypes mb_inst_tys
+ = mapM inst_tv mb_inst_tys
+ where
+ inst_tv :: Either TyVar TcType -> TcS Type
+ inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv
+ inst_tv (Right ty) = return ty
instDFunConstraints :: TcThetaType -> TcS [EvVar]
instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
+newFlexiTcS :: TyVar -> TcS TcTyVar
+-- Make a TcsTv meta tyvar; it is always touchable,
+-- but we are supposed to guess its instantiation
+-- See Note [Touchable meta type variables]
+newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
-- Superclasses and recursive dictionaries
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
where
to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
to_work_item ((qtvs, pairs), _, _)
- = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
- ; mapM (do_one tenv) pairs }
+ = do { let tvs = varSetElems qtvs
+ ; tvs' <- mapM newFlexiTcS tvs
+ ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+ ; mapM (do_one subst) pairs }
- do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
- sty2 = substTy tenv ty2
+ do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1
+ sty2 = substTy subst ty2
; ev <- newWantedCoVar sty1 sty2
; return (WantedEvVar ev loc) }