+normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
+-- Normalise one equality.
+normEqInst inst
+ = ASSERT( isEqInst inst )
+ do { traceTc $ ptext (sLit "normEqInst of ") <+>
+ pprEqInstCo co <+> text "::" <+>
+ ppr ty1 <+> text "~" <+> ppr ty2
+ ; res <- go ty1 ty2 co
+ ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
+ ; return res
+ }
+ where
+ (ty1, ty2) = eqInstTys inst
+ co = eqInstCoercion inst
+
+ -- look through synonyms
+ go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
+ go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
+
+ -- left-to-right rule with type family head
+ go ty1@(TyConApp con args) ty2 co
+ | isOpenSynTyConApp ty1 -- only if not oversaturated
+ = mkRewriteFam False con args ty2 co
+
+ -- right-to-left rule with type family head
+ go ty1 ty2@(TyConApp con args) co
+ | isOpenSynTyConApp ty2 -- only if not oversaturated
+ = do { co' <- mkSymEqInstCo co (ty2, ty1)
+ ; mkRewriteFam True con args ty1 co'
+ }
+
+ -- no outermost family
+ go ty1 ty2 co
+ = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
+ ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
+ ; let ty12_eqs = ty1_eqs ++ ty2_eqs
+ sym_co2 = mkSymCoercion co2
+ eqTys = (ty1', ty2')
+ ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
+ ; eqs <- checkOrientation ty1' ty2' co' inst
+ ; if isLoopyEquality eqs ty12_eqs'
+ then do { if isWantedCo (tci_co inst)
+ then
+ addErrCtxt (ptext (sLit "Rejecting loopy equality")) $
+ eqInstMisMatch inst
+ else
+ warnDroppingLoopyEquality ty1 ty2
+ ; return ([], emptyVarSet) -- drop the equality
+ }
+ else
+ return (eqs ++ ty12_eqs',
+ ty1_skolems `unionVarSet` ty2_skolems)
+ }
+
+ mkRewriteFam swapped con args ty2 co
+ = do { (args', cargs, args_eqss, args_skolemss)
+ <- mapAndUnzip4M (flattenType inst) args
+ ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
+ ; let co1 = mkTyConApp con cargs
+ sym_co2 = mkSymCoercion co2
+ all_eqs = concat args_eqss ++ ty2_eqs
+ eqTys = (mkTyConApp con args', ty2')
+ ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
+ ; let thisRewriteFam = RewriteFam
+ { rwi_fam = con
+ , rwi_args = args'
+ , rwi_right = ty2'
+ , rwi_co = co'
+ , rwi_loc = tci_loc inst
+ , rwi_name = tci_name inst
+ , rwi_swapped = swapped
+ }
+ ; return $ (thisRewriteFam : all_eqs',
+ unionVarSets (ty2_skolems:args_skolemss))
+ }
+
+ -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
+ -- have a variable equality with 'a' on the lhs as the first equality.
+ -- Then, check whether 'a' occurs in the lhs of any family equality
+ -- generated by flattening.
+ isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
+ = any inRewriteFam eqs
+ where
+ inRewriteFam (RewriteFam {rwi_args = args})
+ = tv `elemVarSet` tyVarsOfTypes args
+ inRewriteFam _ = False
+ isLoopyEquality _ _ = False
+
+normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
+-- Normalise one dictionary or IP constraint.
+normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
+ = do { (args', cargs, args_eqss, args_skolemss)
+ <- mapAndUnzip4M (flattenType inst) args
+ ; let rewriteCo = PredTy $ ClassP clas cargs
+ eqs = concat args_eqss
+ pred' = ClassP clas args'
+ ; if null eqs
+ then -- don't generate a binding if there is nothing to flatten
+ return (inst, [], emptyBag, emptyVarSet)
+ else do {
+ ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
+ ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
+ ; return (inst', eqs', bind, unionVarSets args_skolemss)
+ }}
+normDict _isWanted inst
+ = return (inst, [], emptyBag, emptyVarSet)
+-- !!!TODO: Still need to normalise IP constraints.
+
+checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
+-- Performs the occurs check, decomposition, and proper orientation
+-- (returns a singleton, or an empty list in case of a trivial equality)
+-- NB: We cannot assume that the two types already have outermost type
+-- synonyms expanded due to the recursion in the case of type applications.
+checkOrientation ty1 ty2 co inst
+ = go ty1 ty2
+ where
+ -- look through synonyms
+ go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+ go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+ -- identical types => trivial
+ go ty1 ty2
+ | ty1 `tcEqType` ty2
+ = do { mkIdEqInstCo co ty1
+ ; return []
+ }
+
+ -- two tvs, left greater => unchanged
+ go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
+ | tv1 > tv2
+ = mkRewriteVar False tv1 ty2 co
+
+ -- two tvs, right greater => swap
+ | otherwise
+ = do { co' <- mkSymEqInstCo co (ty2, ty1)
+ ; mkRewriteVar True tv2 ty1 co'
+ }
+
+ -- only lhs is a tv => unchanged
+ go ty1@(TyVarTy tv1) ty2
+ | ty1 `tcPartOfType` ty2 -- occurs check!
+ = occurCheckErr ty1 ty2
+ | otherwise
+ = mkRewriteVar False tv1 ty2 co
+
+ -- only rhs is a tv => swap
+ go ty1 ty2@(TyVarTy tv2)
+ | ty2 `tcPartOfType` ty1 -- occurs check!
+ = occurCheckErr ty2 ty1
+ | otherwise
+ = do { co' <- mkSymEqInstCo co (ty2, ty1)
+ ; mkRewriteVar True tv2 ty1 co'
+ }
+
+ -- type applications => decompose
+ go ty1 ty2
+ | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1 -- won't split fam apps
+ , Just (ty2_l, ty2_r) <- repSplitAppTy_maybe ty2
+ = do { (co_l, co_r) <- mkAppEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
+ ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
+ ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
+ ; return $ eqs_l ++ eqs_r
+ }
+-- !!!TODO: would be more efficient to handle the FunApp and the data
+-- constructor application explicitly.
+
+ -- inconsistency => type error
+ go ty1 ty2
+ = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
+ eqInstMisMatch inst
+
+ mkRewriteVar swapped tv ty co = return [RewriteVar
+ { rwi_var = tv
+ , rwi_right = ty
+ , rwi_co = co
+ , rwi_loc = tci_loc inst
+ , rwi_name = tci_name inst
+ , rwi_swapped = swapped
+ }]
+
+flattenType :: Inst -- context to get location & name
+ -> Type -- the type to flatten
+ -> TcM (Type, -- the flattened type
+ Coercion, -- coercion witness of flattening wanteds
+ [RewriteInst], -- extra equalities
+ TyVarSet) -- new intermediate skolems
+-- Removes all family synonyms from a type by moving them into extra equalities
+flattenType inst ty
+ = go ty
+ where
+ -- look through synonyms
+ go ty | Just ty' <- tcView ty
+ = do { (ty_flat, co, eqs, skolems) <- go ty'
+ ; if null eqs
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [], emptyVarSet)
+ else
+ return (ty_flat, co, eqs, skolems)
+ }
+
+ -- type variable => nothing to do
+ go ty@(TyVarTy _)
+ = return (ty, ty, [] , emptyVarSet)
+
+ -- type family application & family arity matches number of args
+ -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
+ go ty@(TyConApp con args)
+ | isOpenSynTyConApp ty -- only if not oversaturated
+ = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
+ ; alpha <- newFlexiTyVar (typeKind ty)
+ ; let alphaTy = mkTyVarTy alpha
+ ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
+ ; let thisRewriteFam = RewriteFam
+ { rwi_fam = con
+ , rwi_args = args'
+ , rwi_right = alphaTy
+ , rwi_co = mkWantedCo cotv
+ , rwi_loc = tci_loc inst
+ , rwi_name = tci_name inst
+ , rwi_swapped = True
+ }
+ ; return (alphaTy,
+ mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
+ thisRewriteFam : concat args_eqss,
+ unionVarSets args_skolemss `extendVarSet` alpha)
+ } -- adding new unflatten var inst
+
+ -- data constructor application => flatten subtypes
+ -- NB: Special cased for efficiency - could be handled as type application
+ go ty@(TyConApp con args)
+ | not (isOpenSynTyCon con) -- don't match oversaturated family apps
+ = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
+ ; if null args_eqss
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [], emptyVarSet)
+ else
+ return (mkTyConApp con args',
+ mkTyConApp con cargs,
+ concat args_eqss,
+ unionVarSets args_skolemss)
+ }
+
+ -- function type => flatten subtypes
+ -- NB: Special cased for efficiency - could be handled as type application
+ go ty@(FunTy ty_l ty_r)
+ = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
+ ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
+ ; if null eqs_l && null eqs_r
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [], emptyVarSet)
+ else
+ return (mkFunTy ty_l' ty_r',
+ mkFunTy co_l co_r,
+ eqs_l ++ eqs_r,
+ skolems_l `unionVarSet` skolems_r)
+ }
+
+ -- type application => flatten subtypes
+ go ty
+ | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
+ -- need to use the smart split as ty may be an
+ -- oversaturated family application
+ = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
+ ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
+ ; if null eqs_l && null eqs_r
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [], emptyVarSet)
+ else
+ return (mkAppTy ty_l' ty_r',
+ mkAppTy co_l co_r,
+ eqs_l ++ eqs_r,
+ skolems_l `unionVarSet` skolems_r)
+ }
+
+ -- forall type => panic if the body contains a type family
+ -- !!!TODO: As long as the family does not contain a quantified variable
+ -- we might pull it out, but what if it does contain a quantified
+ -- variable???
+ go ty@(ForAllTy _ body)
+ | null (tyFamInsts body)
+ = return (ty, ty, [] , emptyVarSet)
+ | otherwise
+ = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
+
+ -- we should never see a predicate type
+ go (PredTy _)
+ = panic "TcTyFuns.flattenType: unexpected PredType"
+
+ go _ = panic "TcTyFuns: suppress bogus warning"
+
+adjustCoercions :: EqInstCo -- coercion of original equality
+ -> Coercion -- coercion witnessing the left rewrite
+ -> Coercion -- coercion witnessing the right rewrite
+ -> (Type, Type) -- types of flattened equality
+ -> [RewriteInst] -- equalities from flattening
+ -> TcM (EqInstCo, -- coercion for flattened equality
+ [RewriteInst]) -- final equalities from flattening
+-- Depending on whether we flattened a local or wanted equality, that equality's
+-- coercion and that of the new equalities produced during flattening are
+-- adjusted .
+adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
+ -- wanted => generate a fresh coercion variable for the flattened equality
+ = do { cotv' <- newMetaCoVar ty_l ty_r
+ ; writeMetaTyVar cotv $
+ (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
+ ; return (Left cotv', all_eqs)
+ }
+
+adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
+ -- local => turn all new equalities into locals and update (but not zonk)
+ -- the skolem
+ = do { all_eqs' <- mapM wantedToLocal all_eqs
+ ; return (co, all_eqs')
+ }
+
+mkDictBind :: Inst -- original instance
+ -> Bool -- is this a wanted contraint?
+ -> Coercion -- coercion witnessing the rewrite
+ -> PredType -- coerced predicate
+ -> TcM (Inst, -- new inst
+ TcDictBinds) -- binding for coerced dictionary
+mkDictBind dict isWanted rewriteCo pred
+ = do { 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 rewriteCo)
+ | otherwise = (dict', dict, rewriteCo)
+ -- 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 (WpCast st_co) expr
+ rhs = L (instLocSpan loc) cast_expr
+ binds = instToDictBind target_dict rhs
+ ; return (dict', binds)