- normaliseOneInst isWanted fun
- dict@(Dict {tci_pred = pred,
- tci_loc = loc})
- = do { traceTc $ text "genericNormaliseInst <-" <+> ppr dict
- ; (coi, pred') <- fun pred
-
- ; case coi of
- IdCo ->
- do { traceTc $ text "genericNormaliseInst ->" <+> ppr dict
- ; return (dict, emptyBag)
- }
- -- don't use pred' in this case; otherwise, we get
- -- more unfolded closed type synonyms in error messages
- ACo co ->
- do { -- an inst for the new pred
- ; dict' <- newDictBndr loc pred'
- -- relate the old inst to the new one
- -- target_dict = source_dict `cast` st_co
- ; let (target_dict, source_dict, st_co)
- | isWanted = (dict, dict', mkSymCoercion co)
- | otherwise = (dict', dict, co)
- -- we have
- -- co :: dict ~ dict'
- -- hence, if isWanted
- -- dict = dict' `cast` sym co
- -- else
- -- dict' = dict `cast` co
- expr = HsVar $ instToId source_dict
- cast_expr = HsWrap (WpCo st_co) expr
- rhs = L (instLocSpan loc) cast_expr
- binds = instToDictBind target_dict rhs
- -- return the new inst
- ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
- ; return (dict', binds)
- }
- }
-
- -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
- normaliseOneInst _isWanted _fun inst
- = do { inst' <- zonkInst inst
- ; return (inst', emptyBag)
- }
+ -- NB: we don't have to transitively chase the relation as the substitution
+ -- process applied before generating the bindings was exhaustive
+ getEscapingSkolems
+ = do { tybinds_rel <- getTcTyVarBindsRelation
+ ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
+ }
+ where
+ isFree (tv, _) = tv `elemVarSet` freeFlexibles
+
+ -- co :: alpha ~ t or co :: a ~ alpha
+ instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+ = do { flexi_tv1 <- isFlexible tv1
+ ; maybe_flexi_tv2 <- isFlexibleTy ty2
+ ; case (flexi_tv1, maybe_flexi_tv2) of
+ (True, Just tv2)
+ | isSigTyVar tv1 && isSigTyVar tv2
+ -> -- co :: alpha ~ beta, where both a SigTvs
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (True, Nothing)
+ | Just tv2 <- tcGetTyVar_maybe ty2
+ , isSigTyVar tv1
+ , isSkolemTyVar tv2
+ -> -- co :: alpha ~ a, where alpha is a SigTv
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (True, _)
+ | not (isSigTyVar tv1)
+ -> -- co :: alpha ~ t, where alpha is not a SigTv
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (False, Just tv2)
+ | isSigTyVar tv2
+ , isSkolemTyVar tv1
+ -> -- co :: a ~ alpha, where alpha is a SigTv
+ doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+ | not (isSigTyVar tv2)
+ -> -- co :: a ~ alpha, where alpha is not a SigTv
+ -- ('a' may be filled)
+ doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+ _ -> return $ Just eq
+ }
+ instVarEq eq = return $ Just eq
+
+ -- co :: F args ~ alpha,
+ -- and we are either in checking mode or alpha is a skolem flexible that
+ -- doesn't escape
+ instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
+ rwi_right = ty2, rwi_co = co})
+ | Just tv2 <- tcGetTyVar_maybe ty2
+ , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
+ = do { flexi_tv2 <- isFlexible tv2
+ ; if flexi_tv2
+ then
+ doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
+ else
+ return $ Just eq
+ }
+ instFamEq _ eq = return $ Just eq
+
+ -- tv is a meta var, but not a SigTV and not filled
+ isFlexible tv
+ | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
+ | otherwise = return False
+
+ -- type is a tv that is a meta var, but not a SigTV and not filled
+ isFlexibleTy ty
+ | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
+ ; if flexi then return $ Just tv
+ else return Nothing
+ }
+ | otherwise = return Nothing
+
+ doInst _swapped _tv _ty (Right ty) _eq
+ = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
+ doInst swapped tv ty (Left cotv) eq
+ = do { lookupTV <- lookupTcTyVar tv
+ ; bMeta swapped tv lookupTV ty cotv
+ }
+ where
+ -- Try to create a binding for a meta variable. There is *no* need to
+ -- consider reorienting the underlying equality; `checkOrientation'
+ -- makes sure that we get variable-variable equalities only in the
+ -- appropriate orientation.
+ --
+ bMeta :: Bool -- is this a swapped equality?
+ -> TcTyVar -- tyvar to instantiate
+ -> LookupTyVarResult -- lookup result of that tyvar
+ -> TcType -- to to instantiate tyvar with
+ -> TcTyVar -- coercion tyvar of current equality
+ -> TcM (Maybe RewriteInst) -- returns the original equality if
+ -- the tyvar could not be instantiated,
+ -- and hence, the equality must be kept
+
+ -- meta variable has been filled already
+ -- => this should never happen due to the use of `isFlexible' above
+ bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
+ = pprPanic "TcTyFuns.bMeta" $
+ ptext (sLit "flexible") <+> ppr tv <+>
+ ptext (sLit "already filled with") <+> ppr fill_ty <+>
+ ptext (sLit "meant to fill with") <+> ppr ty
+
+ -- type variable meets type variable
+ -- => `checkOrientation' already ensures that it is fine to instantiate
+ -- tv1 with tv2, but chase tv2's instantiations if necessary, so that
+ -- we eventually can perform a kinds check in bMetaInst
+ -- NB: tv's instantiations won't alter the orientation in which we
+ -- want to instantiate as they either constitute a family
+ -- application or are themselves due to a properly oriented
+ -- instantiation
+ bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
+ = do { lookupTV2 <- lookupTcTyVar tv2
+ ; case lookupTV2 of
+ IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
+ DoneTv _ -> bMetaInst swapped tv1 ty cotv
+ }
+
+ -- updatable meta variable meets non-variable type
+ -- => occurs check, monotype check, and kinds match check, then bind
+ bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
+ = bMetaInst swapped tv non_tv_ty cotv
+
+ bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
+
+ -- We know `tv' can be instantiated; check that `ty' is alright for
+ -- instantiating `tv' with and then record a binding; we return the
+ -- original equality if it is cyclic through a synonym family
+ bMetaInst swapped tv ty cotv
+ = do { -- occurs + monotype check
+ ; mb_ty' <- checkTauTvUpdate tv ty
+
+ ; case mb_ty' of
+ Nothing ->
+ -- there may be a family in non_tv_ty due to an unzonked,
+ -- but updated skolem for a local equality
+ -- (cf `wantedToLocal')
+ return $ Just eq
+ Just ty' ->
+ do { checkKinds swapped tv ty'
+ ; bindMetaTyVar tv ty' -- bind meta var
+ ; bindMetaTyVar cotv ty' -- bind co var
+ ; return Nothing
+ }
+ }