- n = tyConArity con1
- (idxTys1, _) = splitAt n tys1
- (idxTys2, _) = splitAt n tys2
- identicalHead = not (isOpenSynTyCon con1) ||
- idxTys1 `tcEqTypes` idxTys2
-
- go _ _ = return ([i], False)
-decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
-
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-topInsts :: RewriteRule
-topInsts insts
- = do { (insts,bs) <- mapAndUnzipM topInst insts
- ; return (insts,or bs)
- }
-
- -- (Top)
- -- g1 : t ~ s
- -- >--> co1 :: t ~ t' / co2 :: s ~ s'
- -- g2 : t' ~ s'
- -- g1 := co1 * g2 * sym co2
-topInst :: Inst -> TcM (Inst,Bool)
-topInst i@(EqInst {})
- = do { (coi1,ty1') <- tcNormalizeFamInst ty1
- ; (coi2,ty2') <- tcNormalizeFamInst ty2
- ; case (coi1,coi2) of
- (IdCo,IdCo) ->
- return (i,False)
- _ ->
- do { wg_co <- eitherEqInst i
- -- old_co = co1 * new_co * sym co2
- (\old_covar ->
- do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
- ; let new_co = TyVarTy new_cotv
- ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
- ; writeMetaTyVar old_covar (fromACo old_coi)
- ; return $ mkWantedCo new_cotv
- })
- -- new_co = sym co1 * old_co * co2
- (\old_co -> return $ mkGivenCo $ fromACo $ mkSymCoI coi1 `mkTransCoI` ACo old_co `mkTransCoI` coi2)
- ; new_inst <- mkEqInst (EqPred ty1' ty2') wg_co
- ; return (new_inst,True)
- }
- }
- where
- ty1 = eqInstLeftTy i
- ty2 = eqInstRightTy i
-topInst _ = panic "TcTyFuns.topInsts: not EqInst"
-
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-substInsts :: RewriteRule
-substInsts insts = substInstsWorker insts []
-
-substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
-substInstsWorker [] acc
- = return (acc,False)
-substInstsWorker (i:is) acc
- | (TyConApp con _) <- tci_left i, isOpenSynTyCon con
- = do { (is',change) <- substInst i (acc ++ is)
- ; if change
- then return ((i:is'),True)
- else substInstsWorker is (i:acc)
- }
- | (TyVarTy _) <- tci_left i
- = do { (is',change) <- substInst i (acc ++ is)
- ; if change
- then return ((i:is'),True)
- else substInstsWorker is (i:acc)
- }
- | otherwise
- = substInstsWorker is (i:acc)
-
- -- (Subst)
- -- g : F c ~ t,
- -- forall g1 : s1{F c} ~ s2{F c}
- -- >-->
- -- g2 : s1{t} ~ s2{t}
- -- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
-substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
-substInst _inst [] = return ([],False)
-substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
- = do { (is',changed) <- substInst inst is
- ; (coi1,ty1') <- normalise ty1
- ; (coi2,ty2') <- normalise ty2
- ; case (coi1,coi2) of
- (IdCo,IdCo) ->
- return (i:is',changed)
- _ ->
- do { gw_co <- eitherEqInst i
- -- old_co := co1 * new_co * sym co2
- (\old_covar ->
- do { new_cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
- ; let new_co = TyVarTy new_cotv
- ; let old_coi = coi1 `mkTransCoI` ACo new_co `mkTransCoI` (mkSymCoI coi2)
- ; writeMetaTyVar old_covar (fromACo old_coi)
- ; return $ mkWantedCo new_cotv
- })
- -- new_co := sym co1 * old_co * co2
- (\old_co -> return $ mkGivenCo $ fromACo $ (mkSymCoI coi1) `mkTransCoI` ACo old_co `mkTransCoI` coi2)
- ; new_inst <- mkEqInst (EqPred ty1' ty2') gw_co
- ; return (new_inst:is',True)
- }
- }
- where
- normalise = tcEqInstNormalizeFamInst inst
-substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
-
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-unifyInsts :: RewriteRule
-unifyInsts insts
- = do { (insts',changeds) <- mapAndUnzipM unifyInst insts
- ; return (concat insts',or changeds)
- }
+ (ty1,ty2) = eqInstTys inst
+ go ty1 ty2 cotv
+ | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
+ | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
+
+ | TyVarTy tv1 <- ty1
+ , isMetaTyVar tv1 = do { lookupTV <- lookupTcTyVar tv1
+ ; uMeta False tv1 lookupTV ty2 cotv
+ }
+ | TyVarTy tv2 <- ty2
+ , isMetaTyVar tv2 = do { lookupTV <- lookupTcTyVar tv2
+ ; uMeta True tv2 lookupTV ty1 cotv
+ }
+ | otherwise = return ([inst], False)
+
+ -- meta variable has been filled already
+ -- => ignore this inst (we'll come around again, after zonking)
+ uMeta _swapped _tv (IndirectTv _) _ty _cotv
+ = return ([inst], False)
+
+ -- type variable meets type variable
+ -- => check that tv2 hasn't been updated yet and choose which to update
+ uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
+ | tv1 == tv2
+ = return ([inst], False) -- The two types are already identical
+
+ | otherwise
+ = do { lookupTV2 <- lookupTcTyVar tv2
+ ; case lookupTV2 of
+ IndirectTv ty -> uMeta swapped tv1 (DoneTv details1) ty cotv
+ DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
+ }
+
+ ------ Beyond this point we know that ty2 is not a type variable
+
+ -- signature skolem meets non-variable type
+ -- => cannot update!
+ uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
+ = return ([inst], False)
+
+ -- updatable meta variable meets non-variable type
+ -- => occurs check, monotype check, and kinds match check, then update
+ uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
+ = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty -- occurs + monotype check
+ ; case mb_ty' of
+ Nothing -> return ([inst], False) -- tv occurs in faminst
+ Just ty' ->
+ do { checkUpdateMeta swapped tv ref ty' -- update meta var
+ ; writeMetaTyVar cotv ty' -- update co var
+ ; return ([], True)
+ }
+ }
+
+ uMeta _ _ _ _ _ = panic "uMeta"
+
+ -- uMetaVar: unify two type variables
+ -- meta variable meets skolem
+ -- => just update
+ uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
+ = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
+ ; writeMetaTyVar cotv (mkTyVarTy tv2)
+ ; return ([], True)
+ }
+
+ -- meta variable meets meta variable
+ -- => be clever about which of the two to update
+ -- (from TcUnify.uUnfilledVars minus boxy stuff)
+ uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
+ = do { case (info1, info2) of
+ -- Avoid SigTvs if poss
+ (SigTv _, _ ) | k1_sub_k2 -> update_tv2
+ (_, SigTv _) | k2_sub_k1 -> update_tv1
+
+ (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
+ then update_tv1 -- Same kinds
+ else update_tv2
+ | k2_sub_k1 -> update_tv1
+ | otherwise -> kind_err
+ -- 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.
+
+ ; writeMetaTyVar cotv (mkTyVarTy tv2)
+ ; return ([], True)
+ }
+ where
+ -- Kinds should be guaranteed ok at this point
+ update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
+ update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)