- where
- -- Kinds should be guaranteed ok at this point
- update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
- update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
-
- kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
- unifyKindMisMatch k1 k2
-
- k1 = tyVarKind tv1
- k2 = tyVarKind tv2
- k1_sub_k2 = k1 `isSubKind` k2
- k2_sub_k1 = k2 `isSubKind` k1
-
- nicer_to_update_tv1 = isSystemName (Var.varName tv1)
- -- Try to update sys-y type variables in preference to ones
- -- gotten (say) by instantiating a polymorphic function with
- -- a user-written type sig
-
- uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{Normalisation of Insts}
-%* *
-%************************************************************************
-
-Normalises a set of dictionaries relative to a set of given equalities (which
-are interpreted as rewrite rules). We only consider given equalities of the
-form
-
- F ts ~ t or a ~ t
-
-where F is a type family.
-
-\begin{code}
-substEqInDictInsts :: [Inst] -- given equalities (used as rewrite rules)
- -> [Inst] -- dictinaries to be normalised
- -> TcM ([Inst], TcDictBinds)
-substEqInDictInsts eqInsts dictInsts
- = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
- ; dictInsts' <-
- foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
- ; traceTc (text "substEqInDictInst ->" <+> ppr dictInsts')
- ; return dictInsts'
- }
- where
- -- (1) Given equality of form 'F ts ~ t' or 'a ~ t': use for rewriting
- rewriteWithOneEquality (dictInsts, dictBinds)
- eqInst@(EqInst {tci_left = pattern,
- tci_right = target})
- | isOpenSynTyConApp pattern || isTyVarTy pattern
- = do { (dictInsts', moreDictBinds) <-
- genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
- ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
- }
- where
- applyThisEq = tcGenericNormaliseFamInstPred (return . matchResult)
-
- -- rewrite in case of an exact match
- matchResult ty | tcEqType pattern ty = Just (target, eqInstType eqInst)
- | otherwise = Nothing
-
- -- (2) Given equality has the wrong form: ignore
- rewriteWithOneEquality (dictInsts, dictBinds) _not_a_rewrite_rule
- = return (dictInsts, dictBinds)
-\end{code}
-
-
-Take a bunch of Insts (not EqInsts), and normalise them wrt the top-level
-type-function equations, where
-
- (norm_insts, binds) = normaliseInsts is_wanted insts
-
-If 'is_wanted'
- = True, (binds + norm_insts) defines insts (wanteds)
- = False, (binds + insts) defines norm_insts (givens)
-
-Ie, in the case of normalising wanted dictionaries, we use the normalised
-dictionaries to define the originally wanted ones. However, in the case of
-given dictionaries, we use the originally given ones to define the normalised
-ones.
-
-\begin{code}
-normaliseInsts :: Bool -- True <=> wanted insts
- -> [Inst] -- wanted or given insts
- -> TcM ([Inst], TcDictBinds) -- normalised insts and bindings
-normaliseInsts isWanted insts
- = genericNormaliseInsts isWanted tcNormaliseFamInstPred insts
-
-genericNormaliseInsts :: Bool -- True <=> wanted insts
- -> (TcPredType -> TcM (CoercionI, TcPredType))
- -- how to normalise
- -> [Inst] -- wanted or given insts
- -> TcM ([Inst], TcDictBinds) -- normalised insts & binds
-genericNormaliseInsts isWanted fun insts
- = do { (insts', binds) <- mapAndUnzipM (normaliseOneInst isWanted fun) insts
- ; return (insts', unionManyBags binds)
- }
- where
- 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)
- }