-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
+ -- 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)
+ }
+
+ -- 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) <- mapAndUnzip3M go args
+ ; if null args_eqss
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [])
+ else
+ return (mkTyConApp con args',
+ mkTyConApp con cargs,
+ concat args_eqss)
+ }
+
+ -- 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) <- go ty_l
+ ; (ty_r', co_r, eqs_r) <- go ty_r
+ ; if null eqs_l && null eqs_r
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [])
+ else
+ return (mkFunTy ty_l' ty_r',
+ mkFunTy co_l co_r,
+ eqs_l ++ eqs_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) <- go ty_l
+ ; (ty_r', co_r, eqs_r) <- go ty_r
+ ; if null eqs_l && null eqs_r
+ then -- unchanged, keep the old type with folded synonyms
+ return (ty, ty, [])
+ else
+ return (mkAppTy ty_l' ty_r',
+ mkAppTy co_l co_r,
+ eqs_l ++ eqs_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, [])
+ | 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
+ ; bindMetaTyVar 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.
+--
+-- We do actually update alpha and gamma by side effect (instead of
+-- only remembering the binding with `bindMetaTyVar', as we do for all
+-- other tyvars). We can do this as the side effects are strictly
+-- *local*; we know that both alpha and gamma were just a moment ago
+-- introduced by 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"