import TcType ( TcTyVar, SkolemInfo(SigSkol),
TcTauType, TcSigmaType,
mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType,
- mkForAllTy, isUnLiftedType, tcGetTyVar_maybe,
+ mkForAllTy, isUnLiftedType, tcGetTyVar,
mkTyVarTys, tidyOpenTyVar, tidyOpenType )
import Kind ( argTypeKind )
import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv )
%* *
%************************************************************************
-Type signatures are tricky. Consider
-
- x :: [a]
- y :: b
- (x,y,z) = ([y,z], z, head x)
-
-Here, x and y have type sigs, which go into the environment. We used to
-instantiate their types with skolem constants, and push those types into
-the RHS, so we'd typecheck the RHS with type
- ( [a*], b*, c )
-where a*, b* are skolem constants, and c is an ordinary meta type varible.
-
-The trouble is that the occurrences of z in the RHS force a* and b* to
-be the *same*, so we can't make them into skolem constants that don't unify
-with each other. Alas.
-
-Current solution: don't use skolems at all. Instead, instantiate the type
-signatures with ordinary meta type variables, and check at the end that
-each group has remained distinct.
-
+Type signatures are tricky. See Note [Signature skolems] in TcType
\begin{code}
tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
tcTySig (L span (Sig (L _ name) ty))
= setSrcSpan span $
do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
- ; let rigid_info = SigSkol name
- poly_id = mkLocalId name sigma_ty
+ ; (tvs, theta, tau) <- tcInstSigType name sigma_ty
+ ; loc <- getInstLoc (SigOrigin (SigSkol name))
+
+ ; let poly_id = mkLocalId name sigma_ty
-- The scoped names are the ones explicitly mentioned
-- in the HsForAll. (There may be more in sigma_ty, because
L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
other -> []
- ; (tvs, theta, tau) <- tcInstSigType sigma_ty
- ; loc <- getInstLoc (SigOrigin rigid_info)
; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
sig_tvs = tvs, sig_theta = theta, sig_tau = tau,
sig_loc = loc }) }
; return zonked_tvs }
where
zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
- ; case tcGetTyVar_maybe ty of
- Just tv' -> return tv'
- Nothing -> bomb_out sig_tv "a type" ty }
+ ; return (tcGetTyVar "checkDistinctTyVars" ty) }
+ -- 'ty' is bound to be a type variable, because SigSkolTvs
+ -- can only be unified with type variables
check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
-- The TyVarEnv maps each zonked type variable back to its
-- corresponding user-written signature type variable
check_dup acc (sig_tv, zonked_tv)
= case lookupVarEnv acc zonked_tv of
- Just sig_tv' -> bomb_out sig_tv "another quantified type variable"
- (mkTyVarTy sig_tv')
+ Just sig_tv' -> bomb_out sig_tv sig_tv'
Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
- bomb_out sig_tv doc ty
- = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv)
- <+> ptext SLIT("is unified with") <+> text doc <+> ppr tidy_ty)
+ bomb_out sig_tv1 sig_tv2
+ = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1)
+ <+> ptext SLIT("is unified with another quantified type variable")
+ <+> ppr tidy_tv2)
where
- (env1, tidy_tv) = tidyOpenTyVar emptyTidyEnv sig_tv
- (_env2, tidy_ty) = tidyOpenType env1 ty
+ (env1, tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
+ (_env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2
\end{code}
Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
- arityErr, isRigidType,
+ arityErr,
--------------------------------
-- Zonking
newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
-isRigidType :: TcType -> TcM Bool
--- Check that the type is rigid, *taking the type refinement into account*
--- In other words if a rigid type variable tv is refined to a wobbly type,
--- the answer should be False
--- ToDo: can this happen?
-isRigidType ty
- = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
- ; return (and rigids) }
- where
- is_rigid tv = do { details <- lookupTcTyVar tv
- ; case details of
- RigidTv -> return True
- IndirectTv True ty -> isRigidType ty
- other -> return False
- }
-
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Nothing
-- they cannot possibly be captured by
-- any existing for-alls. Hence zipTopTvSubst
-tcInstTyVar tyvar -- Use the OccName of the tyvar we are instantiating
- -- but make a System Name, so that it's updated in
- -- preference to a tcInstSigTyVar
+tcInstTyVar tyvar -- Freshen the Name of the tyvar
= do { uniq <- newUnique
- ; newMetaTyVar (mkSystemName uniq (getOccName tyvar))
+ ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
(tyVarKind tyvar) Flexi }
tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
---------------------------------------------
-tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh meta type variables, but
--- ones which have the same Name as the original type
--- variable. This is used for type signatures, where we must
--- instantiate with meta type variables, but we'd like to avoid
--- instantiating them were possible; and the unifier unifies
--- tyvars with System Names by preference
+tcInstSigType :: Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.
--
+-- Tne new type variables have the sane Name as the original.
-- We don't need a fresh unique, because the renamer has made them
-- unique, and it's better not to do so because we extend the envt
-- with them as scoped type variables, and we'd like to avoid spurious
-- 's = s' bindings in error messages
-tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
+tcInstSigType id_name ty = tc_inst_type (tcInstSigTyVars id_name) ty
-tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSigTyVars tyvars
+tcInstSigTyVars :: Name -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name tyvars
= mapM new_tv tyvars
where
- new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
+ new_tv tv = do { ref <- newMutVar Flexi ;
+ ; return (mkTcTyVar (tyVarName tv) (tyVarKind tv)
+ (SigSkolTv id_name ref)) }
---------------------------------------------
\begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call
- = FlexiTv
- | RigidTv
+ = DoneTv TcTyVarDetails
| IndirectTv Bool TcType
-- True => This is a non-wobbly type refinement,
-- gotten from GADT match unification
-- This function is the ONLY PLACE that we consult the
-- type refinement carried by the monad
lookupTcTyVar tyvar
- = case tcTyVarDetails tyvar of
+ = let
+ details = tcTyVarDetails tyvar
+ in
+ case details of
+ MetaTv ref -> lookup_wobbly details ref
+
SkolemTv _ -> do { type_reft <- getTypeRefinement
; case lookupVarEnv type_reft tyvar of
Just ty -> return (IndirectTv True ty)
- Nothing -> return RigidTv
- }
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
+ Nothing -> return (DoneTv details)
}
+ -- For SigSkolTvs try the refinement, and, failing that
+ -- see if it's been unified to anything. It's a combination
+ -- of SkolemTv and MetaTv
+ SigSkolTv _ ref -> do { type_reft <- getTypeRefinement
+ ; case lookupVarEnv type_reft tyvar of
+ Just ty -> return (IndirectTv True ty)
+ Nothing -> lookup_wobbly details ref
+ }
+
-- Look up a meta type variable, conditionally consulting
-- the current type refinement
condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
condLookupTcTyVar use_refinement tyvar
| use_refinement = lookupTcTyVar tyvar
| otherwise
- = case tcTyVarDetails tyvar of
- SkolemTv _ -> return RigidTv
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
- }
+ = case details of
+ MetaTv ref -> lookup_wobbly details ref
+ SkolemTv _ -> return (DoneTv details)
+ SigSkolTv _ ref -> lookup_wobbly details ref
+ where
+ details = tcTyVarDetails tyvar
+
+lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
+lookup_wobbly details ref
+ = do { meta_details <- readMutVar ref
+ ; case meta_details of
+ Indirect ty -> return (IndirectTv False ty)
+ Flexi -> return (DoneTv details)
+ }
{-
-- gaw 2004 We aren't shorting anything out anymore, at least for now
-- If b is true, the variable was refined, and therefore it is okay
-- to continue refining inside. Otherwise it was wobbly and we should
-- not refine further inside.
- IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
- FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
- RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
+ IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+ DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable
+ DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
\end{code}
tcLookupClass, tcLookupDataCon, tcLookupId )
import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
- SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprSkolemTyVar,
+ SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprTcTyVar,
TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
import VarEnv ( mkVarEnv ) -- ugly
lazyPatErr pat tvs
= failWithTc $
hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
- 2 (vcat (map get tvs))
- where
- get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv
+ 2 (vcat (map pprTcTyVar tvs))
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
import Packages ( PackageId )
import Type ( Type, TvSubstEnv, pprParendType, pprTyThingCategory )
import TcType ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo,
- TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes )
+ TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes, pprSkolInfo )
import InstEnv ( DFunId, InstEnv )
import IOEnv
import RdrName ( GlobalRdrEnv, LocalRdrEnv )
\begin{code}
pprInstLoc :: InstLoc -> SDoc
-pprInstLoc (InstLoc (SigOrigin info) locn _)
- = text "arising from" <+> ppr info -- I don't think this happens much, if at all
pprInstLoc (InstLoc orig locn _)
= hsep [text "arising from", pp_orig orig, text "at", ppr locn]
where
pp_orig (LiteralOrigin lit) = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
pp_orig (ArithSeqOrigin seq) = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
pp_orig (PArrSeqOrigin seq) = hsep [ptext SLIT("the parallel array sequence"), quotes (ppr seq)]
- pp_orig InstSigOrigin = ptext SLIT("instantiating a type signature")
- pp_orig InstScOrigin = ptext SLIT("the superclasses of an instance declaration")
+ pp_orig InstSigOrigin = ptext SLIT("instantiating a type signature")
+ pp_orig InstScOrigin = ptext SLIT("the superclasses of an instance declaration")
pp_orig DerivOrigin = ptext SLIT("the 'deriving' clause of a data type declaration")
pp_orig DefaultOrigin = ptext SLIT("a 'default' declaration")
- pp_orig DoOrigin = ptext SLIT("a do statement")
- pp_orig ProcOrigin = ptext SLIT("a proc expression")
- pp_orig (SigOrigin info) = ppr info
+ pp_orig DoOrigin = ptext SLIT("a do statement")
+ pp_orig ProcOrigin = ptext SLIT("a proc expression")
+ pp_orig (SigOrigin info) = pprSkolInfo info
\end{code}
--------------------------------
-- MetaDetails
Expected(..), TcRef, TcTyVarDetails(..),
- MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
- isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
- isFlexi, isIndirect,
+ MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+ isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+ isFlexi, isIndirect,
--------------------------------
-- Builders
It's knot-tied back to Var.lhs. There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+ x :: [a]
+ y :: b
+ (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment. We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+ ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other. Alas.
+
+On the other hand, we *must* use skolems for signature type variables,
+becuase GADT type refinement refines skolems only.
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures. But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.
+
+
\begin{code}
type TcTyVar = TyVar -- Used only during type inference
-- A TyVarDetails is inside a TyVar
data TcTyVarDetails
- = SkolemTv SkolemInfo -- A skolem constant
- | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+ = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+ | SkolemTv SkolemInfo -- A skolem constant
+ | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
+ -- see Note [Signature skolems]
+ -- The MetaDetails, if filled in, will
+ -- always be another SigSkolTv
data SkolemInfo
= SigSkol Name -- Bound at a type signature
-- Tidy the type inside a GenSkol, preparatory to printing it
tidySkolemTyVar env tv
= ASSERT( isSkolemTyVar tv )
- (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
+ (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
where
- (env1, info1) = case skolemTvInfo tv of
- GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+ (env1, info1) = case tcTyVarDetails tv of
+ SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
where
(env1, tvs1) = tidyOpenTyVars env tvs
(env2, ty1) = tidyOpenType env1 ty
info -> (env, info)
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
- = ASSERT( isSkolemTyVar tv )
- quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
- ppr (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
- ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
- ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
- ppr (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
- ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
- ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
- <+> quotes (ppr (mkForAllTys tvs ty)),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+ = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+ where
+ ppr_details (MetaTv _) = ptext SLIT("is a meta type variable")
+ ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+ ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info
+
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type")
+ <+> quotes (ppr (mkForAllTys tvs ty)),
+ nest 2 (ptext SLIT("at") <+> ppr loc)]
instance Outputable MetaDetails where
ppr Flexi = ptext SLIT("Flexi")
isSkolemTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> True
- MetaTv _ -> False
+ SkolemTv _ -> True
+ SigSkolTv _ _ -> True
+ MetaTv _ -> False
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
isMetaTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv _ -> False
MetaTv _ -> True
-
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv
- = ASSERT( isTcTyVar tv )
- case tcTyVarDetails tv of
- SkolemTv info -> info
+ other -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- MetaTv ref -> ref
+ MetaTv ref -> ref
+ other -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
import TcRnMonad -- TcType, amongst others
import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
- TcTyVarSet, TcThetaType, Expected(..),
+ TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
SkolemInfo( GenSkol ), MetaDetails(..),
- pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
+ pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
isSubKind, pprKind, splitKindFunTys )
import Inst ( newDicts, instToId, tcInstCall )
import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
- putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
+ tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
readKindVar, writeKindVar )
import TcSimplify ( tcSimplifyCheck )
case details of
IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
| otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
- FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2
- RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2
-
- -- Expand synonyms; ignore FTVs
-uFlexiVar :: Bool -> TcTyVar ->
- Bool -> -- Allow refinements to ty2
- TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Flexi
-uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
- = uFlexiVar swapped tv1 r2 ps_ty2 ty2
-
-uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
+ DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+----------------
+uDoneVar :: Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> Bool -- Allow refinements to ty2
+ -> TcTauType -> TcTauType -- Type 2
+ -> TcM ()
+-- Invariant: tyvar 1 is not unified with anything
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
+ = -- Expand synonyms; ignore FTVs
+ uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
-- Same type variable => no-op
| tv1 == tv2
= returnM ()
-- Distinct type variables
| otherwise
- = condLookupTcTyVar r2 tv2 `thenM` \ details ->
- case details of
- IndirectTv b ty2' -> uFlexiVar swapped tv1 b ty2' ty2'
- FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1)
- | otherwise -> updateFlexi swapped tv1 ty2
- RigidTv -> updateFlexi swapped tv1 ty2
- -- Note that updateFlexi does a sub-kind check
+ = do { lookup2 <- condLookupTcTyVar r2 tv2
+ ; case lookup2 of
+ IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2'
+ DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2
+ }
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
+ = case details1 of
+ MetaTv ref1 -> do { -- Do the occurs check, and check that we are not
+ -- unifying a type variable with a polytype
+ -- Returns a zonked type ready for the update
+ ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
+ ; updateMeta swapped tv1 ref1 ty2 }
+
+ skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
+
+
+----------------
+uDoneVars :: Bool -- Args are swapped
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 1
+ -> TcTyVar -> TcTyVarDetails -- Tyvar 2
+ -> TcM ()
+-- Invarant: the type variables are distinct,
+-- and are not already unified with anything
+
+uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
+ = case details2 of
+ MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ -- Note that updateMeta does a sub-kind check
-- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
where
k1 = tyVarKind tv1
-- so we can choose which to do.
nicer_to_update_tv2 = isSystemName (varName tv2)
- -- Try to update sys-y type variables in preference to sig-y ones
-
- -- First one is flexi, second one isn't a type variable
-uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2
- = -- Do the occurs check, and check that we are not
- -- unifying a type variable with a polytype
- -- Returns a zonked type ready for the update
- do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
- ; updateFlexi swapped tv1 ty2 }
-
--- Ready to update tv1, which is flexi; occurs check is done
-updateFlexi swapped tv1 ty2
- = do { checkKinds swapped tv1 ty2
- ; putMetaTyVar tv1 ty2 }
-
-
-uRigidVar :: Bool -> TcTyVar
- -> Bool -> -- Allow refinements to ty2
- TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Rigid
-uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
- = uRigidVar swapped tv1 r2 ps_ty2 ty2
+ -- Try to update sys-y type variables in preference to ones
+ -- gotten (say) by instantiating a polymorphic function with
+ -- a user-written type sig
+
+uDoneVars swapped tv1 (SkolemTv _) tv2 details2
+ = case details2 of
+ MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
- -- The both-type-variable case
-uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
- -- Same type variable => no-op
- | tv1 == tv2
- = returnM ()
+uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
+ = case details2 of
+ MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+ SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+ other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
- -- Distinct type variables
- | otherwise
- = condLookupTcTyVar r2 tv2 `thenM` \ details ->
- case details of
- IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2'
- FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1)
- RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2)
-
- -- Second one isn't a type variable
-uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2
- = unifyMisMatch (TyVarTy tv1) ps_ty2
+----------------
+updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+updateMeta swapped tv1 ref1 ty2
+ = do { checkKinds swapped tv1 ty2
+ ; writeMutVar ref1 (Indirect ty2) }
\end{code}
\begin{code}
-- unlifted type: e.g. (id 3#) is illegal
= addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
unifyKindMisMatch k1 k2
-
where
(k1,k2) | swapped = (tk2,tk1)
| otherwise = (tk1,tk2)
; case tidy_ty of
TyVarTy tv
| isSkolemTyVar tv -> return (env2, pp_rigid tv',
- pprSkolemTyVar tv')
+ pprTcTyVar tv')
| otherwise -> return simple_result
where
(env2, tv') = tidySkolemTyVar env1 tv