-- Canonical constraints
CanonicalCts, emptyCCan, andCCan, andCCans,
- singleCCan, extendCCans, isEmptyCCan,
- CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals,
+ singleCCan, extendCCans, isEmptyCCan, isCTyEqCan,
+ isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
+
+ CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
mkWantedConstraints, deCanonicaliseWanted,
- makeGivens, makeSolved,
+ makeGivens, makeSolvedByInst,
+
+ CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst,
+ isGivenCt, isWantedCt,
- CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
+ DerivedOrig (..),
+ canRewrite, canSolve,
combineCtLoc, mkGivenFlavor,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
- tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS,
+ tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
-- Creation of evidence variables
isGoodRecEv,
+ zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad
+ compatKind,
+
+
isTouchableMetaTyVar,
+ isTouchableMetaTyVar_InRange,
getDefaultInfo, getDynFlags,
| CIPCan { -- ?x::tau
-- See note [Canonical implicit parameter constraints].
cc_id :: EvVar,
- cc_flavor :: CtFlavor,
+ cc_flavor :: CtFlavor,
cc_ip_nm :: IPName Name,
cc_ip_ty :: TcTauType
}
| 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 `compatKind` typeKind tv
+ -- See Note [Spontaneous solving and kind compatibility]
+ -- * If 'xi' is a flatten skolem then 'tv' can only be:
+ -- - a flatten skolem or a unification variable
+ -- i.e. equalities prefer flatten skolems in their LHS
+ -- See Note [Loopy Spontaneous Solving, Example 4]
+ -- Also related to [Flatten Skolem Equivalence Classes]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
- cc_tyvar :: TcTyVar,
- cc_rhs :: Xi
+ cc_tyvar :: TcTyVar,
+ cc_rhs :: Xi
}
| CFunEqCan { -- F xis ~ xi
-- 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) `compatKind` typeKind cc_rhs
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
}
+compatKind :: Kind -> Kind -> Bool
+compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
+
makeGivens :: CanonicalCts -> CanonicalCts
makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
-- The UnkSkol doesn't matter because these givens are
-- not contradictory (else we'd have rejected them already)
-makeSolved :: CanonicalCt -> CanonicalCt
+makeSolvedByInst :: CanonicalCt -> CanonicalCt
-- Record that a constraint is now solved
-- Wanted -> Derived
-- Given, Derived -> no-op
-makeSolved ct
- | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc }
+makeSolvedByInst ct
+ | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
| otherwise = ct
mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCanonical (CIPCan { cc_ip_ty = ty }) = tyVarsOfType ty
+tyVarsOfCDict :: CanonicalCt -> TcTyVarSet
+tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
+tyVarsOfCDict _ct = emptyVarSet
+
+tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet
+tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
+
tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
Hence the invariant.
+The invariant is
+
Note [Canonical implicit parameter constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type in a canonical implicit parameter constraint doesn't need to
isEmptyCCan :: CanonicalCts -> Bool
isEmptyCCan = isEmptyBag
+
+isCTyEqCan :: CanonicalCt -> Bool
+isCTyEqCan (CTyEqCan {}) = True
+isCTyEqCan (CFunEqCan {}) = False
+isCTyEqCan _ = False
+
+isCDictCan_Maybe :: CanonicalCt -> Maybe Class
+isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
+isCDictCan_Maybe _ = Nothing
+
+isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
+isCIPCan_Maybe (CIPCan {cc_ip_nm = nm }) = Just nm
+isCIPCan_Maybe _ = Nothing
+
+isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
+isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
+isCFunEqCan_Maybe _ = Nothing
+
\end{code}
%************************************************************************
\begin{code}
data CtFlavor
= Given GivenLoc -- We have evidence for this constraint in TcEvBinds
- | Derived WantedLoc -- We have evidence for this constraint in TcEvBinds;
+ | Derived WantedLoc DerivedOrig
+ -- We have evidence for this constraint in TcEvBinds;
-- *however* this evidence can contain wanteds, so
-- it's valid only provisionally to the solution of
-- these wanteds
| Wanted WantedLoc -- We have no evidence bindings for this constraint.
+data DerivedOrig = DerSC | DerInst
+-- Deriveds are either superclasses of other wanteds or deriveds, or partially
+-- solved wanteds from instances.
+
instance Outputable CtFlavor where
- ppr (Given _) = ptext (sLit "[Given]")
- ppr (Wanted _) = ptext (sLit "[Wanted]")
- ppr (Derived _) = ptext (sLit "[Derived]")
+ ppr (Given _) = ptext (sLit "[Given]")
+ ppr (Wanted _) = ptext (sLit "[Wanted]")
+ ppr (Derived {}) = ptext (sLit "[Derived]")
isWanted :: CtFlavor -> Bool
isWanted (Wanted {}) = True
isDerived (Derived {}) = True
isDerived _ = False
+isDerivedSC :: CtFlavor -> Bool
+isDerivedSC (Derived _ DerSC) = True
+isDerivedSC _ = False
+
+isDerivedByInst :: CtFlavor -> Bool
+isDerivedByInst (Derived _ DerInst) = True
+isDerivedByInst _ = False
+
+isWantedCt :: CanonicalCt -> Bool
+isWantedCt ct = isWanted (cc_flavor ct)
+isGivenCt :: CanonicalCt -> Bool
+isGivenCt ct = isGiven (cc_flavor ct)
+
+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
-combineCtLoc (Wanted loc) _ = loc
-combineCtLoc _ (Wanted loc) = loc
-combineCtLoc (Derived loc) _ = loc
-combineCtLoc _ (Derived loc) = loc
+combineCtLoc (Wanted loc) _ = loc
+combineCtLoc _ (Wanted loc) = loc
+combineCtLoc (Derived loc _) _ = loc
+combineCtLoc _ (Derived loc _) = loc
combineCtLoc _ _ = panic "combineCtLoc: both given"
mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
-mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
-mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
+mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk)
+mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
+mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk)
\end{code}
in
thing_inside nest_env
+recoverTcS :: TcS a -> TcS a -> TcS a
+recoverTcS (TcS recovery_code) (TcS thing_inside)
+ = TcS $ \ env ->
+ TcM.recoverM (recovery_code env) (thing_inside env)
+
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
ctxtUnderImplic SimplRuleLhs = SimplCheck
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
+ = do { untch <- getUntouchables
+ ; return $ isTouchableMetaTyVar_InRange untch tv }
+isTouchableMetaTyVar_InRange :: Untouchables -> TcTyVar -> Bool
+isTouchableMetaTyVar_InRange untch tv
+ = case tcTyVarDetails tv of
+ MetaTv TcsTv _ -> True -- See Note [Touchable meta type variables]
+ MetaTv {} -> inTouchableRange untch tv
+ _ -> 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
+
+newFlexiTcS :: TyVar -> TcS TcTyVar
+-- Like TcM.instMetaTyVar but the variable that is created is always
+-- touchable; we are supposed to guess its instantiation.
+-- See Note [Touchable meta type variables]
+newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
+
+newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type)
+-- Create new wanted CoVar that constrains the type to have the specified kind.
+newKindConstraint tv knd
+ = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd
+ ; let ty_k = mkTyVarTy tv_k
+ ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
+ ; return (co_var, ty_k) }
+
+newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
+newFlexiTcSHelper tvname tvkind
+ = wrapTcS $
+ do { uniq <- TcM.newUnique
+ ; ref <- TcM.newMutVar Flexi
+ ; let name = setNameUnique tvname uniq
+ kind = tvkind
+ ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
+
-- Superclasses and recursive dictionaries
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
newWantedCoVar :: TcType -> TcType -> TcS EvVar
newWantedCoVar ty1 ty2 = wrapTcS $ TcM.newWantedCoVar ty1 ty2
-newKindConstraint :: TcType -> Kind -> TcS (CoVar, TcType)
-newKindConstraint ty kind = wrapTcS $ TcM.newKindConstraint ty kind
newCoVar :: TcType -> TcType -> TcS EvVar
newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2
}
+zonkTcTypeTcS :: TcType -> TcS TcType
+-- Zonk through the TyBinds of the Tcs Monad
+zonkTcTypeTcS ty
+ = do { subst <- getTcSTyBindsMap >>= return . varEnvElts
+ ; let (dom,rng) = unzip subst
+ apply_once = substTyWith dom rng
+ ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ]
+ ; return (substTyWith dom rng_idemp ty) }
+
+
+
+
+
+
-- Functional dependencies, instantiation of equations
-------------------------------------------------------
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) }