+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = do_match arg1 arg2 (go res1 res2)
+ -- Match the args, and sub-match the results
+
+ go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match]
+
+ go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind
+
+ do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst
+
+------------
+boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
+ = ASSERT( length tmpl_tys == length boxy_tys )
+ boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
+ -- ToDo: add error context?
+
+boxy_match_s tmpl_tvs [] boxy_tvs [] subst
+ = subst
+boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
+ = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $
+ boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst
+
+------------
+boxy_match :: TcTyVarSet -> TcType -- Template
+ -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these
+ -> BoxySigmaType -- Match against this type
+ -> TvSubst
+ -> TvSubst
+
+-- The boxy_tvs argument prevents this match:
+-- [a] forall b. a ~ forall b. b
+-- We don't want to bind the template variable 'a'
+-- to the quantified type variable 'b'!
+
+boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
+ = go orig_tmpl_ty orig_boxy_ty
+ where
+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (ForAllTy _ ty1) (ForAllTy tv2 ty2)
+ = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst
+
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ | tc1 == tc2 = go_s tys1 tys2
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = go_s [arg1,res1] [arg2,res2]
+
+ go t_ty b_ty
+ | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
+ Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
+ typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant
+ = go_s [s1,t1] [s2,t2]
+
+ go (TyVarTy tv) b_ty
+ | tv `elemVarSet` tmpl_tvs -- Template type variable in the template
+ , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
+ , typeKind b_ty `isSubKind` tyVarKind tv
+ = extendTvSubst subst tv boxy_ty'
+ where
+ boxy_ty' = case lookupTyVar subst tv of
+ Nothing -> orig_boxy_ty
+ Just ty -> ty `boxyLub` orig_boxy_ty
+
+ go _ _ = subst -- Always safe
+
+ --------
+ go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
+
+
+boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
+-- Combine boxy information from the two types
+-- If there is a conflict, return the first
+boxyLub orig_ty1 orig_ty2
+ = go orig_ty1 orig_ty2
+ where
+ go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2, length ts1 == length ts2
+ = TyConApp tc1 (zipWith boxyLub ts1 ts2)
+
+ go (TyVarTy tv1) ty2 -- This is the whole point;
+ | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box
+ = ty2
+
+ -- Look inside type synonyms, but only if the naive version fails
+ go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+ | Just ty2' <- tcView ty1 = go ty1 ty2'
+
+ -- For now, we don't look inside ForAlls, PredTys
+ go ty1 ty2 = orig_ty1 -- Default