+ -- 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
+