From: simonpj Date: Tue, 1 Mar 2005 21:40:54 +0000 (+0000) Subject: [project @ 2005-03-01 21:40:40 by simonpj] X-Git-Tag: Initial_conversion_from_CVS_complete~1000 X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=ff818166a0a06e77becad9e28ed116f3b7f5cc8b [project @ 2005-03-01 21:40:40 by simonpj] Type signatures and skolem constants (again) Merge to STABLE This commit lays to rest the vexed question of skolem constants and type signatures. My fix last week made type-signature variables into ordinary meta type variables, because they can be unified together (see Note [Signature skolems] in TcType). But that was wrong becuase GADTs will only refine skolems. So this commit extends TcTyVarDetails with a new constructors, SigSkolTv, which is a skolem (like SkolemTv) but is unifiable (like MetaTv). It's a bit of a hack, but the code came out quite nicely. Now the GADT tests work. --- diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index a16cddc..c4e1b92 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -39,7 +39,7 @@ import TcMType ( newTyFlexiVarTy, zonkQuantifiedTyVar, 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 ) @@ -561,26 +561,7 @@ getMonoBindInfo tc_binds %* * %************************************************************************ -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] @@ -612,8 +593,10 @@ tcTySig :: 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 @@ -622,8 +605,6 @@ tcTySig (L span (Sig (L _ name) ty)) 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 }) } @@ -721,26 +702,26 @@ checkDistinctTyVars sig_tvs ; 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} diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index f363026..46968f5 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -29,7 +29,7 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, - arityErr, isRigidType, + arityErr, -------------------------------- -- Zonking @@ -122,22 +122,6 @@ newTyFlexiVarTy kind 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 @@ -177,11 +161,9 @@ tcInstTyVars tyvars -- 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) @@ -192,25 +174,24 @@ tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty --------------------------------------------- -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)) } --------------------------------------------- @@ -299,8 +280,7 @@ We return Nothing iff the original box was unbound. \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 @@ -311,31 +291,47 @@ lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult -- 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 @@ -563,9 +559,9 @@ zonkTyVar unbound_var_fn rflag tyvar -- 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} diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index 9261ecb..208af13 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -25,7 +25,7 @@ import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, 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 @@ -634,9 +634,7 @@ badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat 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 diff --git a/ghc/compiler/typecheck/TcRnTypes.lhs b/ghc/compiler/typecheck/TcRnTypes.lhs index a89ebf3..33190e7 100644 --- a/ghc/compiler/typecheck/TcRnTypes.lhs +++ b/ghc/compiler/typecheck/TcRnTypes.lhs @@ -50,7 +50,7 @@ import HscTypes ( FixityEnv, 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 ) @@ -779,8 +779,6 @@ data InstOrigin \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 @@ -791,11 +789,11 @@ pprInstLoc (InstLoc orig locn _) 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} diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index ce31dd5..b9ff393 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -23,9 +23,9 @@ module TcType ( -------------------------------- -- 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 @@ -247,13 +247,45 @@ checking. It's attached to mutable type variables only. 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 @@ -282,30 +314,34 @@ tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) -- 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") @@ -319,8 +355,9 @@ isImmutableTyVar tv 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 ) @@ -331,20 +368,15 @@ isExistentialTyVar tv -- Existential type variable, bound by a pattern 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 diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 395df1e..85f4eb9 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -34,9 +34,9 @@ import TypeRep ( Type(..), PredType(..), TyNote(..) ) 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, @@ -48,7 +48,7 @@ import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, 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 ) @@ -827,31 +827,57 @@ uVar swapped r1 tv1 r2 ps_ty2 ty2 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 @@ -863,46 +889,27 @@ uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2) -- 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} @@ -919,7 +926,6 @@ checkKinds swapped tv1 ty2 -- 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) @@ -1186,7 +1192,7 @@ ppr_ty env ty ; 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