-normaliseGivens :: [Inst] -> TcM ([Inst],TcM ())
-normaliseGivens givens =
- do { traceTc (text "normaliseGivens <-" <+> ppr givens)
- ; (result,action) <- given_eq_rewrite
- ("(SkolemOccurs)", skolemOccurs)
- (return ())
- [("(Occurs)", simple_rewrite_check $ occursCheckInsts),
- ("(ZONK)", simple_rewrite $ zonkInsts),
- ("(TRIVIAL)", trivialInsts),
- ("(SWAP)", swapInsts),
- ("(DECOMP)", decompInsts),
- ("(TOP)", topInsts),
- ("(SUBST)", substInsts)]
- givens
- ; traceTc (text "normaliseGivens ->" <+> ppr result)
- ; return (result,action)
- }
-
-skolemOccurs :: [Inst] -> TcM ([Inst],TcM ())
-skolemOccurs [] = return ([], return ())
-skolemOccurs (inst@(EqInst {}):insts)
- = do { (insts',actions) <- skolemOccurs insts
- -- check whether the current inst co :: ty1 ~ ty2 suffers
- -- from the occurs check issue: F ty1 \in ty2
- ; let occurs = go False ty2
- ; if occurs
- then
- -- if it does generate two new coercions:
- do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
- ; let skolem_ty = TyVarTy skolem_var
- -- ty1 :: ty1 ~ b
- ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
- -- sym co :: ty2 ~ b
- ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
- -- to replace the old one
- -- the corresponding action is
- -- b := ty1
- ; let action = writeMetaTyVar skolem_var ty1
- ; return (inst1:inst2:insts', action >> actions)
- }
- else
- return (inst:insts', actions)
- }
- where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
- co = eqInstCoercion inst
- check :: Bool -> TcType -> Bool
- check flag ty
- = if flag && ty1 `tcEqType` ty
- then True
- else go flag ty
-
- go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
- go flag (FunTy arg res) = or $ map (check flag) [arg,res]
- go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
- go flag ty = False
+ -- 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)
+ }
+ where
+ loc = tci_loc dict
+
+-- gamma ::^l Fam args ~ alpha
+-- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
+-- (the update of alpha will not be apparent during propagation, as we
+-- never follow the indirections of meta variables; it will be revealed
+-- when the equality is zonked)
+--
+-- NB: It's crucial to update *both* alpha and gamma, as gamma may already
+-- have escaped into some other coercions during normalisation.
+--
+wantedToLocal :: RewriteInst -> TcM RewriteInst
+wantedToLocal eq@(RewriteFam {rwi_fam = fam,
+ rwi_args = args,
+ rwi_right = TyVarTy alpha,
+ rwi_co = Left gamma})
+ = do { writeMetaTyVar alpha (mkTyConApp fam args)
+ ; writeMetaTyVar gamma (mkTyConApp fam args)
+ ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
+ }
+wantedToLocal _ = panic "TcTyFuns.wantedToLocal"