--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-occursCheckInsts :: [Inst] -> TcM ()
-occursCheckInsts insts = mappM_ occursCheckInst insts
-
-
- -- (OccursCheck)
- -- t ~ s[T t]
- -- >-->
- -- fail
- --
-occursCheckInst :: Inst -> TcM ()
-occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
- = go ty2
- where
- check ty = if ty `tcEqType` ty1
- then occursError
- else go ty
-
- go (TyConApp con tys) = if isOpenSynTyCon con then return () else mappM_ check tys
- go (FunTy arg res) = mappM_ check [arg,res]
- go (AppTy fun arg) = mappM_ check [fun,arg]
- go _ = return ()
-
- occursError = do { env0 <- tcInitTidyEnv
- ; let (env1, tidy_ty1) = tidyOpenType env0 ty1
- (env2, tidy_ty2) = tidyOpenType env1 ty2
- extra = sep [ppr tidy_ty1, char '~', ppr tidy_ty2]
- ; failWithTcM (env2, hang msg 2 extra)
- }
- where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
+Instantiate meta variables: unifyMetaRule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If an equality equates a meta type variable with a type, we simply instantiate
+the meta variable.
+
+ (UnifyMeta)
+ g : alpha ~ t
+ >-->
+ alpha := t
+ g := t
+
+Meta variables can only appear in wanted constraints, and this rule should
+only be applied to wanted constraints. We also know that t definitely is
+distinct from alpha (as the trivialRule) has been run on the insts beforehand.
+
+NB: We cannot assume that meta tyvars are empty. They may have been updated
+by another inst in the currently processed wanted list. We need to be very
+careful when updateing type variables (see TcUnify.uUnfilledVar), but at least
+we know that we have no boxes. It's unclear that it would be an advantage to
+common up the code in TcUnify and the code below. Firstly, we don't want
+calls to TcUnify.defer_unification here, and secondly, TcUnify import the
+current module, so we would have to move everything here (Yuk!) or to
+TcMType. Besides, the code here is much simpler due to the lack of boxes.
+
+\begin{code}
+unifyMetaRule :: RewriteRule
+unifyMetaRule insts
+ = do { (insts', changed) <- mapAndUnzipM unifyMeta insts
+ ; return (concat insts', or changed)
+ }
+ where
+ unifyMeta inst
+ = ASSERT( isEqInst inst )
+ go ty1 ty2
+ (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
+ where
+ (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)
+
+ kind_err = addErrCtxtM (unifyKindCtxt swapped 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_tv1 = isSystemName (Var.varName tv1)
+ -- Try to update sys-y type variables in preference to ones
+ -- gotten (say) by instantiating a polymorphic function with
+ -- a user-written type sig
+
+ uMetaVar _ _ _ _ _ _ = panic "uMetaVar"