newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newKindVar, newKindVars,
+ mkTcTyVarName,
newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
isFilledMetaTyVar, isFlexiMetaTyVar,
--------------------------------
-- Creating new evidence variables
newEvVar, newCoVar, newEvVars,
- newWantedCoVar, writeWantedCoVar, readWantedCoVar,
- newIP, newDict, newSelfDict, isSelfDict,
+ newIP, newDict, newSilentGiven, isSilentEvVar,
- newWantedEvVar, newWantedEvVars,
- newKindConstraint,
+ newWantedEvVar, newWantedEvVars,
newTcEvBinds, addTcEvBind,
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
- tcInstType, tcInstSigType,
- tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars,
+ tcInstTyVars, tcInstSigTyVars,
+ tcInstType,
+ tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+ tcSkolDFunType, tcSuperSkolTyVars,
--------------------------------
-- Checking type validity
--------------------------------
-- Zonking
zonkType, mkZonkTcTyVar, zonkTcPredType,
- zonkTcTypeCarefully,
+ zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKindToKind, zonkTcKind,
- zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+ zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
+ zonkWC, zonkWantedEvVars,
zonkTcTypeAndSubst,
tcGetGlobalTyVars,
+
readKindVar, writeKindVar
) where
import TypeRep
import TcType
import Type
-import Coercion
import Class
import TyCon
import Var
import SrcLoc
import Outputable
import FastString
+import Unique( Unique )
import Bag
import Control.Monad
-import Data.List ( (\\) )
+import Data.List ( (\\) )
\end{code}
newEvVars theta = mapM newEvVar theta
newWantedEvVar :: TcPredType -> TcM EvVar
-newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
+newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
newWantedEvVar (ClassP cls tys) = newDict cls tys
newWantedEvVar (IParam ip ty) = newIP ip ty
newWantedEvVars :: TcThetaType -> TcM [EvVar]
newWantedEvVars theta = mapM newWantedEvVar theta
-newWantedCoVar :: TcType -> TcType -> TcM CoVar
-newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
-
--- We used to create a mutable co-var
-{-
--- A wanted coercion variable is a MetaTyVar
--- that can be filled in with its binding
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; let name = mkSysTvName uniq (fsLit "c")
- kind = mkPredTy (EqPred ty1 ty2)
- ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
--}
-
--------------
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
newCoVar :: TcType -> TcType -> TcM CoVar
newCoVar ty1 ty2
- = do { name <- newName (mkTyVarOccFS (fsLit "co"))
+ = do { name <- newName (mkVarOccFS (fsLit "co"))
; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
newIP :: IPName Name -> TcType -> TcM IpId
; return (mkInternalName uniq occ loc) }
-----------------
-newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
--- Create a new wanted CoVar that constrains the type
--- to have the specified kind
-newKindConstraint ty kind
- = do { ty_k <- newFlexiTyVarTy kind
- ; co_var <- newWantedCoVar ty ty_k
- ; return (co_var, ty_k) }
-
------------------
-newSelfDict :: Class -> [TcType] -> TcM DictId
--- Make a dictionary for "self". It behaves just like a normal DictId
--- except that it responds True to isSelfDict
+newSilentGiven :: PredType -> TcM EvVar
+-- Make a dictionary for a "silent" given dictionary
+-- Behaves just like any EvVar except that it responds True to isSilentDict
-- This is used only to suppress confusing error reports
-newSelfDict cls tys
+newSilentGiven (ClassP cls tys)
= do { uniq <- newUnique
- ; let name = mkSystemName uniq selfDictOcc
+ ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+newSilentGiven (EqPred ty1 ty2)
+ = do { uniq <- newUnique
+ ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
+ ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+newSilentGiven pred@(IParam {})
+ = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
-selfDictOcc :: OccName
-selfDictOcc = mkVarOcc "self"
-
-isSelfDict :: EvVar -> Bool
-isSelfDict v = isSystemName (Var.varName v)
+isSilentEvVar :: EvVar -> Bool
+isSilentEvVar v = isSystemName (Var.varName v)
-- Notice that all *other* evidence variables get Internal Names
\end{code}
; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
-- Either the tyvars are freshly made, by inst_tyvars,
- -- or (in the call from tcSkolSigType) any nested foralls
- -- have different binders. Either way, zipTopTvSubst is ok
+ -- or any nested foralls have different binders.
+ -- Either way, zipTopTvSubst is ok
; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
; return (tyvars', theta, tau) }
-mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
-mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
-
-tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type signature with skolem constants, but
-- do *not* give them fresh names, because we want the name to
-- be in the type environment: it is lexically scoped.
-tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
-tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
-- Make skolem constants, but do *not* give them new names, as above
-tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
- | tv <- tyvars ]
+-- Moreover, make them "super skolems"; see comments with superSkolemTv
+tcSuperSkolTyVars tyvars
+ = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
+ | tv <- tyvars ]
-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
-- Instantiate the tyvar, using
-- * the occ-name and kind of the supplied tyvar,
-- * the unique from the monad,
-- * the location either from the tyvar (skol_info = SigSkol)
--- or from the monad (otehrwise)
-tcInstSkolTyVar skol_info tyvar
+-- or from the monad (otherwise)
+tcInstSkolTyVar overlappable tyvar
= do { uniq <- newUnique
- ; loc <- case skol_info of
- SigSkol {} -> return (getSrcSpan old_name)
- _ -> getSrcSpanM
+ ; loc <- getSrcSpanM
; let new_name = mkInternalName uniq occ loc
- ; return (mkSkolTyVar new_name kind skol_info) }
+ ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
where
old_name = tyVarName tyvar
occ = nameOccName old_name
kind = tyVarKind tyvar
-tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Get the location from the monad
-tcInstSkolTyVars info tyvars
- = mapM (tcInstSkolTyVar info) tyvars
+tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
+
+tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
-
-tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigType use_skols name ty
- | use_skols
- = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
- | otherwise
- = tcInstType tcInstSigTyVars ty
+tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
-- Make meta SigTv type variables for patten-bound scoped type varaibles
-- We use SigTvs for them, so that they can't unify with arbitrary types
-tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
- -- ToDo: the "function binding site is bogus
+tcInstSigTyVars = mapM tcInstSigTyVar
+
+tcInstSigTyVar :: TyVar -> TcM TcTyVar
+tcInstSigTyVar tyvar
+ = do { uniq <- newMetaUnique
+ ; ref <- newMutVar Flexi
+ ; let name = setNameUnique (tyVarName tyvar) uniq
+ -- Use the same OccName so that the tidy-er
+ -- doesn't rename 'a' to 'a0' etc
+ kind = tyVarKind tyvar
+ ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
\end{code}
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newMetaTyVar meta_info kind
- = do { uniq <- newUnique
+ = do { uniq <- newMetaUnique
; ref <- newMutVar Flexi
- ; let name = mkSysTvName uniq fs
- fs = case meta_info of
- TauTv -> fsLit "t"
- SigTv _ -> fsLit "a"
+ ; let name = mkTcTyVarName uniq s
+ s = case meta_info of
+ TauTv -> fsLit "t"
+ TcsTv -> fsLit "u"
+ SigTv -> fsLit "a"
; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
-instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
--- Make a new meta tyvar whose Name and Kind
--- come from an existing TyVar
-instMetaTyVar meta_info tyvar
- = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; let name = setNameUnique (tyVarName tyvar) uniq
- kind = tyVarKind tyvar
- ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
+mkTcTyVarName :: Unique -> FastString -> Name
+-- Make sure that fresh TcTyVar names finish with a digit
+-- leaving the un-cluttered names free for user names
+mkTcTyVarName uniq str = mkSysTvName uniq str
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
-readWantedCoVar :: CoVar -> TcM MetaDetails
-readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
- readMutVar (metaTvRef covar)
-
-
-
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
= WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
return ()
-writeWantedCoVar :: CoVar -> Coercion -> TcM ()
-writeWantedCoVar cv co = writeMetaTyVar cv co
-
--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
-- Here the tyvar is for error checking only;
| otherwise
= do { meta_details <- readMutVar ref;
- ; WARN( not (isFlexi meta_details),
- hang (text "Double update of meta tyvar")
+ ; ASSERT2( isFlexi meta_details,
+ hang (text "Double update of meta tyvar")
2 (ppr tyvar $$ ppr meta_details) )
traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
-tcInstTyVar :: TyVar -> TcM TcTyVar
--- Instantiate with a META type variable
-tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
-
tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- Instantiate with META type variables
tcInstTyVars tyvars
-- Since the tyvars are freshly made,
-- they cannot possibly be captured by
-- any existing for-alls. Hence zipTopTvSubst
+
+tcInstTyVar :: TyVar -> TcM TcTyVar
+-- Make a new unification variable tyvar whose Name and Kind
+-- come from an existing TyVar
+tcInstTyVar tyvar
+ = do { uniq <- newMetaUnique
+ ; ref <- newMutVar Flexi
+ ; let name = mkSystemName uniq (getOccName tyvar)
+ kind = tyVarKind tyvar
+ ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
\end{code}
zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
----------------- Types
-
zonkTcTypeCarefully :: TcType -> TcM TcType
-- Do not zonk type variables free in the environment
zonkTcTypeCarefully ty
| otherwise
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
- FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
+ SkolemTv {} -> return (TyVarTy tv)
+ RuntimeUnk {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
Flexi -> return (TyVarTy tv)
Indirect ty -> zonkType (zonk_tv env_tvs) ty }
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
- FlatSkol ty -> zonkTcType ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
- Flexi -> return (TyVarTy tv)
+ SkolemTv {} -> return (TyVarTy tv)
+ RuntimeUnk {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkTcType ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
Indirect ty -> zonkTcType ty }
zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
where
zonk_tv tv
= case tcTyVarDetails tv of
- SkolemTv {} -> return (TyVarTy tv)
- FlatSkol ty -> zonkType zonk_tv ty
- MetaTv _ ref -> do { cts <- readMutVar ref
- ; case cts of
+ SkolemTv {} -> return (TyVarTy tv)
+ RuntimeUnk {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType zonk_tv ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
Flexi -> zonk_flexi tv
Indirect ty -> zonkType zonk_tv ty }
zonk_flexi tv
zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
--- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
---
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
--
-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
- | ASSERT2( isTcTyVar tv, ppr tv )
- isSkolemTyVar tv
- = do { kind <- zonkTcType (tyVarKind tv)
- ; return $ setTyVarKind tv kind
- }
+ = ASSERT2( isTcTyVar tv, ppr tv )
+ case tcTyVarDetails tv of
+ SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen?
+ do { kind <- zonkTcType (tyVarKind tv)
+ ; return $ setTyVarKind tv kind }
-- It might be a skolem type variable,
-- for example from a user type signature
- | otherwise -- It's a meta-type-variable
- = do { details <- readMetaTyVar tv
-
- -- Create the new, frozen, skolem type variable
- -- We zonk to a skolem, not to a regular TcVar
- -- See Note [Zonking to Skolem]
+ MetaTv _ _ref ->
+#ifdef DEBUG
+ -- [Sept 04] Check for non-empty.
+ -- See note [Silly Type Synonym]
+ (readMutVar _ref >>= \cts ->
+ case cts of
+ Flexi -> return ()
+ Indirect ty -> WARN( True, ppr tv $$ ppr ty )
+ return ()) >>
+#endif
+ skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+ _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
+
+skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
+-- We have a Meta tyvar with a ref-cell inside it
+-- Skolemise it, including giving it a new Name, so that
+-- we are totally out of Meta-tyvar-land
+-- We create a skolem TyVar, not a regular TyVar
+-- See Note [Zonking to Skolem]
+skolemiseUnboundMetaTyVar tv details
+ = ASSERT2( isMetaTyVar tv, ppr tv )
+ do { span <- getSrcSpanM -- Get the location from "here"
+ -- ie where we are generalising
+ ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land
; let final_kind = defaultKind (tyVarKind tv)
- final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
-
- -- Bind the meta tyvar to the new tyvar
- ; case details of
- Indirect ty -> WARN( True, ppr tv $$ ppr ty )
- return ()
- -- [Sept 04] I don't think this should happen
- -- See note [Silly Type Synonym]
-
- Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-
- -- Return the new tyvar
+ final_name = mkInternalName uniq (getOccName tv) span
+ final_tv = mkTcTyVar final_name final_kind details
+ ; writeMetaTyVar tv (mkTyVarTy final_tv)
; return final_tv }
\end{code}
\begin{code}
zonkImplication :: Implication -> TcM Implication
-zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given
- , ic_wanted = wanted })
- = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs
- ; given' <- mapM zonkEvVar given
- ; wanted' <- mapBagM zonkWanted wanted
- ; return (implic { ic_untch = env_tvs', ic_given = given'
- , ic_wanted = wanted' }) }
+zonkImplication implic@(Implic { ic_given = given
+ , ic_wanted = wanted
+ , ic_loc = loc })
+ = do { -- No need to zonk the skolems
+ ; given' <- mapM zonkEvVar given
+ ; loc' <- zonkGivenLoc loc
+ ; wanted' <- zonkWC wanted
+ ; return (implic { ic_given = given'
+ , ic_wanted = wanted'
+ , ic_loc = loc' }) }
zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
; return (setVarType var ty') }
-zonkWanted :: WantedConstraint -> TcM WantedConstraint
-zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
-zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
+zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
+zonkFlavoredEvVar (EvVarX ev fl)
+ = do { ev' <- zonkEvVar ev
+ ; fl' <- zonkFlavor fl
+ ; return (EvVarX ev' fl') }
+
+zonkWC :: WantedConstraints -> TcM WantedConstraints
+zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+ = do { flat' <- zonkWantedEvVars flat
+ ; implic' <- mapBagM zonkImplication implic
+ ; insol' <- mapBagM zonkFlavoredEvVar insol
+ ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
+
+zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
+zonkWantedEvVars = mapBagM zonkWantedEvVar
zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
-zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
+zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
+
+zonkFlavor :: CtFlavor -> TcM CtFlavor
+zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
+zonkFlavor fl = return fl
+
+zonkGivenLoc :: GivenLoc -> TcM GivenLoc
+-- GivenLocs may have unification variables inside them!
+zonkGivenLoc (CtLoc skol_info span ctxt)
+ = do { skol_info' <- zonkSkolemInfo skol_info
+ ; return (CtLoc skol_info' span ctxt) }
+
+zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
+zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
+ ; return (SigSkol cx ty') }
+zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
+ ; return (InferSkol ntys') }
+ where
+ do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
+zonkSkolemInfo skol_info = return skol_info
\end{code}
-
Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
-zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
- -- see zonkTcType, and zonkTcTypeToType
- -> TcType
- -> TcM Type
+zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
+ -> TcType -> TcM Type
zonkType zonk_tc_tyvar ty
= go ty
where
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
- | otherwise = liftM TyVarTy $
- zonkTyVar zonk_tc_tyvar tyvar
+ | otherwise = return (TyVarTy tyvar)
-- Ordinary (non Tc) tyvars occur inside quantified types
go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
ty' <- go ty
- tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+ tyvar' <- return tyvar
return (ForAllTy tyvar' ty')
go_pred (ClassP c tys) = do tys' <- mapM go tys
ty2' <- go ty2
return (EqPred ty1' ty2')
-mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
-> TcTyVar -> TcM TcType
mkZonkTcTyVar unbound_var_fn tyvar
= ASSERT( isTcTyVar tyvar )
case tcTyVarDetails tyvar of
SkolemTv {} -> return (TyVarTy tyvar)
+ RuntimeUnk {} -> return (TyVarTy tyvar)
FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> unbound_var_fn tyvar
Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
-
--- Zonk the kind of a non-TC tyvar in case it is a coercion variable
--- (their kind contains types).
-zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
- -> TyVar -> TcM TyVar
-zonkTyVar zonk_tc_tyvar tv
- | isCoVar tv
- = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
- ; return $ setTyVarKind tv kind }
- | otherwise = return tv
\end{code}
ForSigCtxt _ -> gen_rank 1
SpecInstCtxt -> gen_rank 1
- ThBrackCtxt -> gen_rank 1
+ ThBrackCtxt -> gen_rank 1
+ GenSigCtxt -> panic "checkValidType"
+ -- Can't happen; GenSigCtxt not used for *user* sigs
actual_kind = typeKind ty
warnTc (notNull dups) (dupPredWarn dups)
mapM_ (check_pred_ty dflags ctxt) theta
where
- (_,dups) = removeDups tcCmpPred theta
+ (_,dups) = removeDups cmpPred theta
-------------------------
check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
-check_pred_ty dflags _ pred@(EqPred ty1 ty2)
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
= do { -- Equational constraints are valid in all contexts if type
-- families are permitted
; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+ ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
+ (eqSuperClassErr pred)
-- Check the form of the argument types
; checkValidMonoType ty1
ambigErr :: PredType -> SDoc
ambigErr pred
- = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
+ = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred),
nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
ptext (sLit "must be reachable from the type after the '=>'"))]
\end{code}
= vcat [ptext (sLit "In the context:") <+> pprTheta theta,
ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
+eqSuperClassErr :: PredType -> SDoc
+eqSuperClassErr pred
+ = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
+ 2 (ppr pred)
+
badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
-badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
-eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
- $$
- parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred
+eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred
+ $$
+ parens (ptext (sLit "Use -XTypeFamilies to permit this"))
predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
- nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
dupPredWarn :: [[PredType]] -> SDoc
-dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups)
arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
arityErr kind name n m
We can also have instances for functions: @instance Foo (a -> b) ...@.
\begin{code}
-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-checkValidInstHead ty -- Should be a source type
- = case tcSplitPredTy_maybe ty of {
- Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
- Just pred ->
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+ = do { dflags <- getDOpts
- case getClassPredTys_maybe pred of {
- Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
- Just (clas,tys) -> do
-
- dflags <- getDOpts
- check_inst_head dflags clas tys
- return (clas, tys)
- }}
-
-check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
-check_inst_head dflags clas tys
- = do { -- If GlasgowExts then check at least one isn't a type variable
+ -- If GlasgowExts then check at least one isn't a type variable
; checkTc (xopt Opt_TypeSynonymInstances dflags ||
all tcInstHeadTyNotSynonym tys)
- (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+ (instTypeErr pp_pred head_type_synonym_msg)
; checkTc (xopt Opt_FlexibleInstances dflags ||
all tcInstHeadTyAppAllTyVars tys)
- (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+ (instTypeErr pp_pred head_type_args_tyvars_msg)
; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
isSingleton tys)
- (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+ (instTypeErr pp_pred head_one_type_msg)
-- May not contain type family applications
; mapM_ checkTyFamFreeness tys
}
where
+ pp_pred = pprClassPred clas tys
head_type_synonym_msg = parens (
text "All instance types must be of the form (T t1 ... tn)" $$
text "where T is not a synonym." $$
head_type_args_tyvars_msg = parens (vcat [
text "All instance types must be of the form (T a1 ... an)",
- text "where a1 ... an are type *variables*,",
+ text "where a1 ... an are *distinct type variables*,",
text "and each type variable appears at most once in the instance head.",
text "Use -XFlexibleInstances if you want to disable this."])
%************************************************************************
\begin{code}
-checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
- -> TcM (Class, [TcType])
-checkValidInstance hs_type tyvars theta tau
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
+ -> Class -> [TcType] -> TcM ()
+checkValidInstance hs_type tyvars theta clas inst_tys
= setSrcSpan (getLoc hs_type) $
- do { (clas, inst_tys) <- setSrcSpan head_loc $
- checkValidInstHead tau
-
- ; undecidable_ok <- xoptM Opt_UndecidableInstances
-
- ; checkValidTheta InstThetaCtxt theta
+ do { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
+ ; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- Check that instance inference will terminate (if we care)
-- For Haskell 98 this will already have been done by checkValidTheta,
-- but as we may be using other extensions we need to check.
- ; unless undecidable_ok $
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
+ ; unless undecidable_ok $
mapM_ addErrTc (checkInstTermination inst_tys theta)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
-
- ; return (clas, inst_tys)
- }
+ }
where
msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
undecidableMsg])
- -- The location of the "head" of the instance
+ -- The location of the "head" of the instance
head_loc = case hs_type of
L _ (HsForAllTy _ _ _ (L loc _)) -> loc
L loc _ -> loc
predUndecErr :: PredType -> SDoc -> SDoc
predUndecErr pred msg = sep [msg,
- nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)]
nomoreMsg, smallerMsg, undecidableMsg :: SDoc
nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
projects / ghc-hetmet.git / blobdiff