X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=1a618228ebe9d85954f376bba70bd717653a64c8;hb=6493f9d3305d5af08ad92c8f32b8b6410404eb46;hp=23cc9e21760724b982b42322863af6001fe1b13b;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 23cc9e2..1a61822 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -32,14 +32,14 @@ import TcMType ( lookupTcTyVar, LookupTyVarResult(..), tcInstSkolType, newKindVar, newMetaTyVar, tcInstBoxy, newBoxyTyVar, newBoxyTyVarTys, readFilledBox, readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, - tcInstSkolTyVars, + tcInstSkolTyVars, tcInstTyVar, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) import TcEnv ( tcGetGlobalTyVars, findGlobals ) import TcIface ( checkWiredInTyCon ) import TcRnMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcTyVar, TcTauType, +import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, BoxySigmaType, BoxyRhoType, BoxyType, TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..), SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar, @@ -53,7 +53,8 @@ import TcType ( TcKind, TcType, TcTyVar, TcTauType, TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst, lookupTyVar, extendTvSubst ) import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, - openTypeKind, liftedTypeKind, mkArrowKind, defaultKind, + openTypeKind, liftedTypeKind, unliftedTypeKind, + mkArrowKind, defaultKind, isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, isSubKind, pprKind, splitKindFunTys ) import TysPrim ( alphaTy, betaTy ) @@ -477,8 +478,8 @@ boxyLub orig_ty1 orig_ty2 = TyConApp tc1 (zipWith boxyLub ts1 ts2) go (TyVarTy tv1) ty2 -- This is the whole point; - | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box - = ty2 + | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box + = orig_ty2 -- Look inside type synonyms, but only if the naive version fails go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 @@ -995,10 +996,14 @@ uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2 = -- Expand synonyms; ignore FTVs uUnfilledVar False swapped tv1 details1 nb2 ps_ty2 ty2' -uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2) - -- Same type variable => no-op - | tv1 == tv2 - = returnM () +uUnfilledVar outer swapped tv1 details1 nb2 ps_ty2 (TyVarTy tv2) + | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case) + = case details1 of + MetaTv BoxTv ref1 -- A boxy type variable meets itself; + -- this is box-meets-box, so fill in with a tau-type + -> do { tau_tv <- tcInstTyVar tv1 + ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) } + other -> returnM () -- No-op -- Distinct type variables | otherwise @@ -1024,10 +1029,26 @@ uMetaVar :: Bool -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable +uMetaVar swapped tv1 BoxTv ref1 nb2 ps_ty2 non_var_ty2 + = -- tv1 is a BoxTv. So we must unbox ty2, to ensure + -- that any boxes in ty2 are filled with monotypes + -- + -- It should not be the case that tv1 occurs in ty2 + -- (i.e. no occurs check should be needed), but if perchance + -- it does, the unbox operation will fill it, and the DEBUG + -- checks for that. + do { final_ty <- unBox ps_ty2 +#ifdef DEBUG + ; meta_details <- readMutVar ref1 + ; case meta_details of + Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) + return () -- This really should *not* happen + Flexi -> return () +#endif + ; checkUpdateMeta swapped tv1 ref1 final_ty } + uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2 - = do { final_ty <- case info1 of - BoxTv -> unBox ps_ty2 -- No occurs check - other -> checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check + = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check ; checkUpdateMeta swapped tv1 ref1 final_ty } ---------------- @@ -1079,13 +1100,18 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2) update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1) - box_meets_box | k1_sub_k2 = fill_with k1 - | k2_sub_k1 = fill_with k2 + box_meets_box | k1_sub_k2 = if k2_sub_k1 && nicer_to_update_tv1 + then fill_from tv2 + else fill_from tv1 + | k2_sub_k1 = fill_from tv2 | otherwise = kind_err - fill_with kind = do { tau_ty <- newFlexiTyVarTy kind - ; updateMeta tv1 ref1 tau_ty - ; updateMeta tv2 ref2 tau_ty } + -- Update *both* tyvars with a TauTv whose name and kind + -- are gotten from tv (avoid losing nice names is poss) + fill_from tv = do { tv' <- tcInstTyVar tv + ; let tau_ty = mkTyVarTy tv' + ; updateMeta tv1 ref1 tau_ty + ; updateMeta tv2 ref2 tau_ty } kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $ unifyKindMisMatch k1 k2 @@ -1181,9 +1207,7 @@ checkTauTvUpdate orig_tv orig_ty ; case cts of Indirect ty -> go ty Flexi -> case box of - BoxTv -> do { tau <- newFlexiTyVarTy (tyVarKind tv) - ; writeMutVar ref (Indirect tau) - ; return tau } + BoxTv -> fillBoxWithTau tv ref other -> return (TyVarTy tv) } @@ -1201,6 +1225,19 @@ checkTauTvUpdate orig_tv orig_ty (tcView (TyConApp tc tys))) -- Try again, expanding the synonym } + +fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType +-- (fillBoxWithTau tv ref) fills ref with a freshly allocated +-- tau-type meta-variable, whose print-name is the same as tv +-- Choosing the same name is good: when we instantiate a function +-- we allocate boxy tyvars with the same print-name as the quantified +-- tyvar; and then we often fill the box with a tau-tyvar, and again +-- we want to choose the same name. +fillBoxWithTau tv ref + = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget + ; let tau = mkTyVarTy tv' -- name of the type variable + ; writeMutVar ref (Indirect tau) + ; return tau } \end{code} Note [Type synonyms and the occur check] @@ -1271,13 +1308,11 @@ unBox (TyVarTy tv) , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible = do { cts <- readMutVar ref -- under nested quantifiers ; case cts of + Flexi -> fillBoxWithTau tv ref Indirect ty -> do { non_boxy_ty <- unBox ty ; if isTauTy non_boxy_ty then return non_boxy_ty else notMonoType non_boxy_ty } - Flexi -> do { tau <- newFlexiTyVarTy (tyVarKind tv) - ; writeMutVar ref (Indirect tau) - ; return tau } } | otherwise -- Skolems, and meta-tau-variables = return (TyVarTy tv) @@ -1490,6 +1525,7 @@ kindSimpleKind orig_swapped orig_kind go True OpenTypeKind = return liftedTypeKind go True ArgTypeKind = return liftedTypeKind go sw LiftedTypeKind = return liftedTypeKind + go sw UnliftedTypeKind = return unliftedTypeKind go sw k@(KindVar _) = return k -- KindVars are always simple go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:") <+> ppr orig_swapped <+> ppr orig_kind)