+data RewriteInst
+ = RewriteVar -- Form (2) above
+ { rwi_var :: TyVar -- may be rigid or flexible
+ , rwi_right :: TcType -- contains no synonym family applications
+ , rwi_co :: EqInstCo -- the wanted or given coercion
+ , rwi_loc :: InstLoc
+ , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
+ , rwi_swapped :: Bool -- swapped orientation of original EqInst
+ }
+ | RewriteFam -- Forms (1) above
+ { rwi_fam :: TyCon -- synonym family tycon
+ , rwi_args :: [Type] -- contain no synonym family applications
+ , rwi_right :: TcType -- contains no synonym family applications
+ , rwi_co :: EqInstCo -- the wanted or given coercion
+ , rwi_loc :: InstLoc
+ , rwi_name :: Name -- no semantic significance (cf. TcRnTypes.EqInst)
+ , rwi_swapped :: Bool -- swapped orientation of original EqInst
+ }
+
+isWantedRewriteInst :: RewriteInst -> Bool
+isWantedRewriteInst = isWantedCo . rwi_co
+
+isRewriteVar :: RewriteInst -> Bool
+isRewriteVar (RewriteVar {}) = True
+isRewriteVar _ = False
+
+tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
+tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
+ = unitVarSet tv `unionVarSet` tyVarsOfType ty
+tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
+ = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
+
+rewriteInstToInst :: RewriteInst -> TcM Inst
+rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
+ = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
+rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
+ = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
+
+-- Derive an EqInst based from a RewriteInst, possibly swapping the types
+-- around.
+--
+deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
+deriveEqInst rewrite ty1 ty2 co
+ = do { co_adjusted <- if not swapped then return co
+ else mkSymEqInstCo co (ty2, ty1)
+ ; return $ EqInst
+ { tci_left = left
+ , tci_right = right
+ , tci_co = co_adjusted
+ , tci_loc = rwi_loc rewrite
+ , tci_name = rwi_name rewrite
+ }
+ }
+ where
+ swapped = rwi_swapped rewrite
+ (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
+
+instance Outputable RewriteInst where
+ ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
+ = hsep [ pprEqInstCo co <+> text "::"
+ , ppr (mkTyConApp fam args)
+ , text "~>"
+ , ppr rhs
+ ]
+ ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
+ = hsep [ pprEqInstCo co <+> text "::"
+ , ppr tv
+ , text "~>"
+ , ppr rhs
+ ]
+
+pprEqInstCo :: EqInstCo -> SDoc
+pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
+pprEqInstCo (Right co) = ptext (sLit "Local") <+> ppr co
+\end{code}
+
+The following functions turn an arbitrary equality into a set of normal
+equalities. This implements the WFlat and LFlat rules of the paper in one
+sweep. However, we use flexible variables for both locals and wanteds, and
+avoid to carry around the unflattening substitution \Sigma (for locals) by
+already updating the skolems for locals with the family application that they
+represent - i.e., they will turn into that family application on the next
+zonking (which only happens after finalisation).
+
+In a corresponding manner, normDict normalises class dictionaries by
+extracting any synonym family applications and generation appropriate normal
+equalities.
+
+Whenever we encounter a loopy equality (of the form a ~ T .. (F ...a...) ...),
+we drop that equality and raise an error if it is a wanted or a warning if it
+is a local.
+
+\begin{code}
+normEqInst :: Inst -> TcM [RewriteInst]
+-- 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) <- flattenType inst ty1
+ ; (ty2', co2, ty2_eqs) <- 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 ([]) -- drop the equality
+ }
+ else
+ return (eqs ++ ty12_eqs')
+ }
+
+ mkRewriteFam swapped con args ty2 co
+ = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
+ ; (ty2', co2, ty2_eqs) <- 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'
+ }
+
+ -- 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)
+-- Normalise one dictionary or IP constraint.
+normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
+ = do { (args', cargs, args_eqss) <- mapAndUnzip3M (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)
+ else do {
+ ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
+ ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
+ ; return (inst', eqs', bind)
+ }}
+normDict _isWanted inst
+ = return (inst, [], emptyBag)
+-- !!!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 (distinct tvs, due to previous equation)
+ go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
+ = do { isBigger <- tv1 `tvIsBigger` tv2
+ ; if isBigger -- left greater
+ then mkRewriteVar False tv1 ty2 co -- => unchanged
+ else do { co' <- mkSymEqInstCo co (ty2, ty1) -- right greater
+ ; mkRewriteVar True tv2 ty1 co' -- => swap
+ }
+ }
+
+ -- 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'
+ }
+
+ -- data type constructor application => decompose
+ -- NB: Special cased for efficiency - could be handled as type application
+ go (TyConApp con1 args1) (TyConApp con2 args2)
+ | con1 == con2
+ && isInjectiveTyCon con1 -- don't match family synonym apps
+ = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
+ ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
+ args1 args2 co_args
+ ; return $ concat eqss
+ }
+
+ -- function type => decompose
+ -- NB: Special cased for efficiency - could be handled as type application
+ go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
+ = do { (co_l, co_r) <- mkFunEqInstCo 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
+ }
+
+ -- 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
+ }
+
+ -- 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
+ }]
+
+ -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
+ tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
+ tvIsBigger tv1 tv2
+ = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
+ where
+ isBigger tv1 (SkolemTv _) tv2 (SkolemTv _)
+ = return $ tv1 > tv2
+ isBigger _ (MetaTv _ _) _ (SkolemTv _)
+ = return True
+ isBigger _ (SkolemTv _) _ (MetaTv _ _)
+ = return False
+ isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
+ -- meta variable meets meta variable
+ -- => be clever about which of the two to update
+ -- (from TcUnify.uUnfilledVars minus boxy stuff)
+ = case (info1, info2) of
+ -- Avoid SigTvs if poss
+ (SigTv _, SigTv _) -> return $ tv1 > tv2
+ (SigTv _, _ ) | k1_sub_k2 -> return False
+ (_, SigTv _) | k2_sub_k1 -> return True
+
+ (_, _)
+ | k1_sub_k2 &&
+ k2_sub_k1
+ -> case (nicer_to_update tv1, nicer_to_update tv2) of
+ (True, False) -> return True
+ (False, True) -> return False
+ _ -> return $ tv1 > tv2
+ | k1_sub_k2 -> return False
+ | k2_sub_k1 -> return True
+ | otherwise -> kind_err >> return True
+ -- Update the variable with least kind info
+ -- See notes on type inference in Kind.lhs
+ -- The "nicer to" part only applies if the two kinds are the same,
+ -- so we can choose which to do.
+ where
+ kind_err = addErrCtxtM (unifyKindCtxt False 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 tv = isSystemName (Var.varName tv)
+ -- Try to update sys-y type variables in preference to ones
+ -- gotten (say) by instantiating a polymorphic function with
+ -- a user-written type sig
+
+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
+-- 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) <- go ty'
+ ; if null eqs
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [])
+ else
+ return (ty_flat, co, eqs)
+ }
+
+ -- type variable => nothing to do
+ go ty@(TyVarTy _)
+ = return (ty, ty, [])
+
+ -- 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) <- mapAndUnzip3M 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)
+ }
+
+ -- datatype 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) <- mapAndUnzip3M go args
+ ; let args_eqs = concat args_eqss
+ ; if null args_eqs
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [])
+ else
+ return (mkTyConApp con args',
+ mkTyConApp con cargs,
+ args_eqs)
+ }