-- 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,
+ isGivenCt, isWantedCt, pprFlavorArising,
+
+ isFlexiTcsTv,
- CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
- joinFlavors, mkGivenFlavor,
+ DerivedOrig (..),
+ canRewrite, canSolve,
+ combineCtLoc, mkGivenFlavor, mkWantedFlavor,
+ getWantedLoc,
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
newTcEvBindsTcS,
getInstEnvs, getFamInstEnvs, -- Getting the environments
- getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS,
- getTcEvBindsBag, getTcSContext, getTcSTyBinds,
-
+ getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
+ getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
+ getTcSErrorsBag, FrozenError (..),
+ addErrorTcS,
+ ErrorKind(..),
newFlattenSkolemTy, -- Flatten skolems
- zonkFlattenedType,
instDFunTypes, -- Instantiation
- instDFunConstraints,
+ instDFunConstraints,
+ newFlexiTcSTy,
isGoodRecEv,
+ compatKind,
+
+
+ TcsUntouchables,
isTouchableMetaTyVar,
+ isTouchableMetaTyVar_InRange,
getDefaultInfo, getDynFlags,
import FamInst
import FamInstEnv
-import NameSet ( addOneToNameSet )
-
import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
import TcType
-import Module
import DynFlags
import Coercion
import Name
import Var
+import VarEnv
import Outputable
import Bag
import MonadUtils
| 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]
+ -- * We prefer unification variables on the left *JUST* for efficiency
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 (F xis) `compatKind` typeKind xi
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
= ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
\end{code}
-
-Note [No touchables as FunEq RHS]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Notice that (F xis ~ beta), where beta is an touchable unification
-variable, is not canonical. Why?
- * If (F xis ~ beta) was the only wanted constraint, we'd
- definitely want to spontaneously-unify it
-
- * But suppose we had an earlier wanted (beta ~ Int), and
- have already spontaneously unified it. Then we have an
- identity given (id : beta ~ Int) in the inert set.
-
- * But (F xis ~ beta) does not react with that given (because we
- don't subsitute on the RHS of a function equality). So there's a
- serious danger that we'd spontaneously unify it a second time.
-
-Hence the invariant.
-
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 | DerSelf
+-- Deriveds are either superclasses of other wanteds or deriveds, or partially
+-- solved wanteds from instances, or 'self' dictionaries containing yet wanted
+-- superclasses.
+
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
+pprFlavorArising :: CtFlavor -> SDoc
+pprFlavorArising (Derived wl _) = pprArisingAt wl
+pprFlavorArising (Wanted wl) = pprArisingAt wl
+pprFlavorArising (Given gl) = pprArisingAt gl
+
+getWantedLoc :: CanonicalCt -> WantedLoc
+getWantedLoc ct
+ = ASSERT (isWanted (cc_flavor ct))
+ case cc_flavor ct of
+ Wanted wl -> wl
+ _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
+
+
+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
-
-joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor
-joinFlavors (Wanted loc) _ = Wanted loc
-joinFlavors _ (Wanted loc) = Wanted loc
-joinFlavors (Derived loc) _ = Derived loc
-joinFlavors _ (Derived loc) = Derived loc
-joinFlavors (Given loc) _ = Given loc
+-- 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 _ _ = 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)
+
+mkWantedFlavor :: CtFlavor -> CtFlavor
+mkWantedFlavor (Wanted loc) = Wanted loc
+mkWantedFlavor (Derived loc _) = Wanted loc
+mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
\end{code}
tcs_ev_binds :: EvBindsVar,
-- Evidence bindings
- tcs_ty_binds :: IORef (Bag (TcTyVar, TcType)),
+ tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
-- Global type bindings
- tcs_context :: SimplContext
+ tcs_context :: SimplContext,
+
+ tcs_errors :: IORef (Bag FrozenError),
+ -- Frozen errors that we defer reporting as much as possible, in order to
+ -- make them as informative as possible. See Note [Frozen Errors]
+
+ tcs_untch :: TcsUntouchables
}
+type TcsUntouchables = (Untouchables,TcTyVarSet)
+-- Like the TcM Untouchables,
+-- but records extra TcsTv variables generated during simplification
+-- See Note [Extra TcsTv untouchables] in TcSimplify
+
+data FrozenError
+ = FrozenError ErrorKind CtFlavor TcType TcType
+
+data ErrorKind
+ = MisMatchError | OccCheckError | KindError
+
+instance Outputable FrozenError where
+ ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
+
+\end{code}
+
+Note [Frozen Errors]
+~~~~~~~~~~~~~~~~~~~~
+Some of the errors that we get during canonicalization are best reported when all constraints
+have been simplified as much as possible. For instance, assume that during simplification
+the following constraints arise:
+
+ [Wanted] F alpha ~ uf1
+ [Wanted] beta ~ uf1 beta
+
+When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply
+see a message:
+ 'Can't construct the infinite type beta ~ uf1 beta'
+and the user has no idea what the uf1 variable is.
+
+Instead our plan is that we will NOT fail immediately, but:
+ (1) Record the "frozen" error in the tcs_errors field
+ (2) Isolate the offending constraint from the rest of the inerts
+ (3) Keep on simplifying/canonicalizing
+
+At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to
+report a more informative error:
+ 'Can't construct the infinite type beta ~ F alpha beta'
+\begin{code}
+
data SimplContext
= SimplInfer -- Inferring type of a let-bound thing
| SimplRuleLhs -- Inferring type of a RULE lhs
traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
runTcS :: SimplContext
- -> TcTyVarSet -- Untouchables
+ -> Untouchables -- Untouchables
-> TcS a -- What to run
- -> TcM (a, Bag EvBind)
+ -> TcM (a, Bag FrozenError, Bag EvBind)
runTcS context untouch tcs
- = do { ty_binds_var <- TcM.newTcRef emptyBag
+ = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
+ ; err_ref <- TcM.newTcRef emptyBag
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
- , tcs_context = context }
+ , tcs_context = context
+ , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
+ , tcs_errors = err_ref
+ }
-- Run the computation
- ; res <- TcM.setUntouchables untouch (unTcS tcs env)
-
+ ; res <- unTcS tcs env
-- Perform the type unifications required
; ty_binds <- TcM.readTcRef ty_binds_var
- ; mapBagM_ do_unification ty_binds
+ ; mapM_ do_unification (varEnvElts ty_binds)
-- And return
- ; ev_binds <- TcM.readTcRef evb_ref
- ; return (res, evBindMapBinds ev_binds) }
+ ; frozen_errors <- TcM.readTcRef err_ref
+ ; ev_binds <- TcM.readTcRef evb_ref
+ ; return (res, frozen_errors, evBindMapBinds ev_binds) }
where
do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
-
-nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a
-nestImplicTcS ref untouch tcs
- = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } ->
+
+nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
+nestImplicTcS ref untch (TcS thing_inside)
+ = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
+ tcs_context = ctxt,
+ tcs_errors = err_ref } ->
let
nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
- , tcs_context = ctxtUnderImplic ctxt }
+ , tcs_untch = untch
+ , tcs_context = ctxtUnderImplic ctxt
+ , tcs_errors = err_ref }
in
- TcM.setUntouchables untouch (unTcS tcs nest_env)
+ 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
ctxtUnderImplic ctxt = ctxt
-tryTcS :: TcTyVarSet -> TcS a -> TcS a
+tryTcS :: TcS a -> TcS a
-- Like runTcS, but from within the TcS monad
-- Ignore all the evidence generated, and do not affect caller's evidence!
-tryTcS untch tcs
- = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyBag
+tryTcS tcs
+ = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var <- TcM.newTcEvBinds
+ ; err_ref <- TcM.newTcRef emptyBag
; let env1 = env { tcs_ev_binds = ev_binds_var
- , tcs_ty_binds = ty_binds_var }
- ; TcM.setUntouchables untch (unTcS tcs env1) })
+ , tcs_ty_binds = ty_binds_var
+ , tcs_errors = err_ref }
+ ; unTcS tcs env1 })
-- Update TcEvBinds
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds)
-getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
+getUntouchables :: TcS TcsUntouchables
+getUntouchables = TcS (return . tcs_untch)
+
+getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
getTcSTyBinds = TcS (return . tcs_ty_binds)
+getTcSErrors :: TcS (IORef (Bag FrozenError))
+getTcSErrors = TcS (return . tcs_errors)
+
+getTcSErrorsBag :: TcS (Bag FrozenError)
+getTcSErrorsBag = do { err_ref <- getTcSErrors
+ ; wrapTcS $ TcM.readTcRef err_ref }
+
+getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
+getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef)
+
+
getTcEvBindsBag :: TcS EvBindMap
getTcEvBindsBag
= do { EvBindsVar ev_ref _ <- getTcEvBinds
setWantedTyBind :: TcTyVar -> TcType -> TcS ()
-- Add a type binding
+-- We never do this twice!
setWantedTyBind tv ty
= do { ref <- getTcSTyBinds
; wrapTcS $
do { ty_binds <- TcM.readTcRef ref
- ; TcM.writeTcRef ref (ty_binds `snocBag` (tv,ty)) } }
+#ifdef DEBUG
+ ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
+ vcat [ text "TERRIBLE ERROR: double set of meta type variable"
+ , ppr tv <+> text ":=" <+> ppr ty
+ , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
+#endif
+ ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
setIPBind :: EvVar -> EvTerm -> TcS ()
setIPBind = setEvBind
; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
; return (ctxt, tys, flags) }
+
+
+-- Recording errors in the TcS monad
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
+addErrorTcS frknd fl ty1 ty2
+ = do { err_ref <- getTcSErrors
+ ; wrapTcS $ do
+ { TcM.updTcRef err_ref $ \ errs ->
+ consBag (FrozenError frknd fl ty1 ty2) errs
+
+ -- If there's an error in the *given* constraints,
+ -- stop right now, to avoid a cascade of errors
+ -- in the wanteds
+ ; when (isGiven fl) TcM.failM
+
+ ; return () } }
+
-- Just get some environments needed for instance looking up and matching
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
getGblEnv :: TcS TcGblEnv
getGblEnv = wrapTcS $ TcM.getGblEnv
-getUntouchablesTcS :: TcS TcTyVarSet
-getUntouchablesTcS = wrapTcS $ TcM.getUntouchables
-
-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
isTouchableMetaTyVar :: TcTyVar -> TcS Bool
--- is touchable variable!
-isTouchableMetaTyVar v
- | isMetaTyVar v = wrapTcS $ do { untch <- TcM.isUntouchable v;
- ; return (not untch) }
- | otherwise = return False
+isTouchableMetaTyVar tv
+ = do { untch <- getUntouchables
+ ; return $ isTouchableMetaTyVar_InRange untch tv }
+isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool
+isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
+ = case tcTyVarDetails tv of
+ MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
+ -- See Note [Touchable meta type variables]
+ MetaTv {} -> inTouchableRange untch tv
+ _ -> False
--- 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)
- }
+\end{code}
-zonkFlattenedType :: TcType -> TcS TcType
-zonkFlattenedType ty = wrapTcS (TcM.zonkTcType ty)
+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.
-{--
-tyVarsOfUnflattenedType :: TcType -> TcTyVarSet
--- A version of tyVarsOfType which looks through flatSkols
-tyVarsOfUnflattenedType ty
- = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty)
- where
- do_tv :: TyVar -> TcTyVarSet
- do_tv tv = ASSERT( isTcTyVar tv)
- case tcTyVarDetails tv of
- FlatSkol _ ty -> tyVarsOfUnflattenedType ty
- _ -> unitVarSet tv
---}
+\begin{code}
+-- Flatten skolems
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+newFlattenSkolemTy :: TcType -> TcS TcType
+newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
+newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
+newFlattenSkolemTyVar ty
+ = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
+ ; let name = mkSysTvName uniq (fsLit "f")
+ ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
+ ; traceTcS "New Flatten Skolem Born" $
+ (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
+ ; return tv }
-- 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 <$> instFlexiTcS tv
+ inst_tv (Right ty) = return ty
instDFunConstraints :: TcThetaType -> TcS [EvVar]
instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds
+instFlexiTcS :: 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]
+instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
+
+newFlexiTcSTy :: Kind -> TcS TcType
+newFlexiTcSTy knd
+ = wrapTcS $
+ do { uniq <- TcM.newUnique
+ ; ref <- TcM.newMutVar Flexi
+ ; let name = mkSysTvName uniq (fsLit "uf")
+ ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
+
+isFlexiTcsTv :: TyVar -> Bool
+isFlexiTcsTv tv
+ | not (isTcTyVar tv) = False
+ | MetaTv TcsTv _ <- tcTyVarDetails tv = True
+ | otherwise = False
+
+newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
+-- Create new wanted CoVar that constrains the type to have the specified kind.
+newKindConstraint tv knd
+ = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
+ ; let ty_k = mkTyVarTy tv_k
+ ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
+ ; return co_var }
+
+instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
+instFlexiTcSHelper 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
\begin{code}
-isGoodRecEv :: EvVar -> WantedEvVar -> TcS Bool
+isGoodRecEv :: EvVar -> EvVar -> TcS Bool
-- In a call (isGoodRecEv ev wv), we are considering solving wv
-- using some term that involves ev, such as:
-- by setting wv = ev
-- call (constructor) and -1 for every superclass selection (destructor).
--
-- See Note [Superclasses and recursive dictionaries] in TcInteract
-isGoodRecEv ev_var (WantedEvVar wv _)
+isGoodRecEv ev_var wv
= do { tc_evbinds <- getTcEvBindsBag
; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var
; return $ case mb of
| Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
= chase_ev assocs trg curr_grav (orig:visited) ev_trm
-{- No longer needed: evidence is in the EvBinds
- | isTcTyVar orig && isMetaTyVar orig
- = do { meta_details <- wrapTcS $ TcM.readWantedCoVar orig
- ; case meta_details of
- Flexi -> return Nothing
- Indirect tyco -> chase_ev assocs trg curr_grav
- (orig:visited) (EvCoercion tyco)
- }
--}
- | otherwise = return Nothing
+ | otherwise = return Nothing
chase_ev assocs trg curr_grav visited (EvId v)
= chase_ev_var assocs trg curr_grav visited v
chase_ev assocs trg curr_grav visited (EvCoercion co)
= chase_co assocs trg curr_grav visited co
- chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_vars)
- = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_vars
- ; return (comb_chase_res Nothing chase_results) }
+ chase_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps)
+ = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
+ -- Notice that we chase the ev_deps and not the ev_vars
+ -- See Note [Dependencies in self dictionaries] in TcSimplify
+ ; return (comb_chase_res Nothing chase_results) }
chase_co assocs trg curr_grav visited co
= -- Look for all the coercion variables in the coercion
text "witness" <+> ppr dfun_id
<+> ppr (idType dfun_id) ])
-- Record that this dfun is needed
- ; record_dfun_usage dfun_id
- ; return $ MatchInstSingle (dfun_id, inst_tys)
+ ; return $ MatchInstSingle (dfun_id, inst_tys)
} ;
(matches, unifs) -- More than one matches
-> do { traceTcS "matchClass multiple matches, deferring choice"
}
}
}
- where record_dfun_usage :: Id -> TcS ()
- record_dfun_usage dfun_id
- = do { hsc_env <- getTopEnv
- ; let dfun_name = idName dfun_id
- dfun_mod = ASSERT( isExternalName dfun_name )
- nameModule dfun_name
- ; if isInternalName dfun_name || -- Internal name => defined in this module
- modulePackageId dfun_mod /= thisPackage (hsc_dflags hsc_env)
- then return () -- internal, or in another package
- else do updInstUses dfun_id
- }
-
- updInstUses :: Id -> TcS ()
- updInstUses dfun_id
- = do { tcg_env <- getGblEnv
- ; wrapTcS $ TcM.updMutVar (tcg_inst_uses tcg_env)
- (`addOneToNameSet` idName dfun_id)
- }
-
-matchFam :: TyCon
+
+matchFam :: TyCon
-> [Type]
-> TcS (MatchInstResult (TyCon, [Type]))
matchFam tycon args
-- Functional dependencies, instantiation of equations
-------------------------------------------------------
-mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
+mkWantedFunDepEqns :: WantedLoc
+ -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
-> TcS [WantedEvVar]
mkWantedFunDepEqns _ [] = return []
mkWantedFunDepEqns loc eqns
; return $ concat wevvars }
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_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1
- sty2 = substTy tenv ty2
- ; ev <- newWantedCoVar sty1 sty2
- ; return (WantedEvVar ev loc) }
+ to_work_item ((qtvs, pairs), d1, d2)
+ = do { let tvs = varSetElems qtvs
+ ; tvs' <- mapM instFlexiTcS tvs
+ ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+ loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
+ ; mapM (do_one subst loc') pairs }
+
+ do_one subst loc' (ty1, ty2)
+ = do { let sty1 = substTy subst ty1
+ sty2 = substTy subst ty2
+ ; ev <- newWantedCoVar sty1 sty2
+ ; return (WantedEvVar ev loc') }
pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
pprEquationDoc (eqn, (p1, _), (p2, _))
= vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
+mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
+ = do { pred1' <- TcM.zonkTcPredType pred1
+ ; pred2' <- TcM.zonkTcPredType pred2
+ ; let { pred1'' = tidyPred tidy_env pred1'
+ ; pred2'' = tidyPred tidy_env pred2' }
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
+ nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
+ nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
+ ; return (tidy_env, msg) }
\end{code}
projects / ghc-hetmet.git / blobdiff