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,
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 )
= 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
= -- 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
-- 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 }
----------------
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
; 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)
}
(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]
, 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)
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)
projects / ghc-hetmet.git / blobdiff