- 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 $ let name | isWanted
- = "genericNormaliseInst (wanted) ->"
- | otherwise
- = "genericNormaliseInst (given) ->"
- in
- text name <+> ppr dict' <+>
- text "with" <+> ppr binds
- ; return (dict', binds)
- }
- }
-
- -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
- normaliseOneInst _isWanted _fun inst
- = do { inst' <- zonkInst inst
- ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
- ppr inst
- ; return (inst', emptyBag)
- }
+ wanteds = filter (isWantedCo . rwi_co) eqs
+ checkingMode = length eqs > length wanteds || not localsEmpty
+ -- no local equalities or dicts => checking mode
+
+ -- co :: alpha ~ t or co :: a ~ alpha
+ inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+ = do { flexi_tv1 <- isFlexible mayInst tv1
+ ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
+ ; case (flexi_tv1, maybe_flexi_tv2) of
+ (True, _)
+ -> -- co :: alpha ~ t
+ doInst (rwi_swapped eq) tv1 ty2 co eq
+ (False, Just tv2)
+ -> -- co :: a ~ alpha
+ doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+ _ -> return $ Just eq
+ }
+
+ -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
+ inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args,
+ rwi_right = ty2, rwi_co = co})
+ | Just tv2 <- tcGetTyVar_maybe ty2
+ , isMetaTyVar tv2
+ , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
+ -- !!!FIXME: this is too liberal, even if tv2 is in
+ -- skolems we shouldn't instantiate if tvs occurs
+ -- in other equalities that may propagate it into the
+ -- environment
+ = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
+
+ inst _mayInst eq = return $ Just eq
+
+ -- tv is a meta var and not filled
+ isFlexible mayInst tv
+ | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
+ | otherwise = return False
+
+ -- type is a tv that is a meta var and not filled
+ isFlexibleTy mayInst ty
+ | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst 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
+ ; uMeta swapped tv lookupTV ty cotv
+ }
+ where
+ -- Try to fill in 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.
+ --
+ uMeta :: 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
+ -- => keep the equality
+ uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
+ = do { traceTc $
+ ptext (sLit "flexible") <+> ppr tv <+>
+ ptext (sLit "already filled with") <+> ppr fill_ty <+>
+ ptext (sLit "meant to fill with") <+> ppr ty
+ ; return $ Just eq
+ }
+
+ -- signature skolem
+ -- => cannot update (retain the equality)!
+ uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
+ = return $ Just eq
+
+ -- type variable meets type variable
+ -- => `checkOrientation' already ensures that it is fine to instantiate
+ -- tv1 with tv2, but chase tv2's instantiations if necessary
+ -- 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
+ uMeta swapped tv1 details1@(DoneTv (MetaTv _ ref)) ty@(TyVarTy tv2) cotv
+ = do { lookupTV2 <- lookupTcTyVar tv2
+ ; case lookupTV2 of
+ IndirectTv ty' ->
+ uMeta swapped tv1 details1 ty' cotv
+ DoneTv _ ->
+ uMetaInst swapped tv1 ref ty cotv
+ }
+
+ -- updatable meta variable meets non-variable type
+ -- => occurs check, monotype check, and kinds match check, then update
+ uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
+ = uMetaInst swapped tv ref non_tv_ty cotv
+
+ uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
+
+ -- We know `tv' can be instantiated; check that `ty' is alright for
+ -- instantiating `tv' with and then do it; otherwise, return the original
+ -- equality.
+ uMetaInst swapped tv ref 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
+ return $ Just eq
+ Just ty' ->
+ do { checkUpdateMeta swapped tv ref ty' -- update meta var
+ ; writeMetaTyVar cotv ty' -- update co var
+ ; return Nothing
+ }
+ }