+-- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
+-- "Boxy types: inference for higher rank types and impredicativity"
+
+boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
+ = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
+ where
+ go t_tvs t_ty b_tvs b_ty
+ | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
+ | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
+
+ go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings
+ -- Rule S-ANY covers (a) type variables and (b) boxy types
+ -- in the template. Both look like a TyVarTy.
+ -- See Note [Sub-match] below
+
+ go t_tvs t_ty b_tvs b_ty
+ | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
+ = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC
+ -- Under a forall on the left, if there is shadowing,
+ -- do not bind! Hence the delVarSetList.
+ | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
+ = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL
+ -- Add to the variables we must not bind to
+ -- NB: it's *important* to discard the theta part. Otherwise
+ -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
+ -- and end up with a completely bogus binding (b |-> Bool), by lining
+ -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
+ -- This pre-subsumption stuff can return too few bindings, but it
+ -- must *never* return bogus info.
+
+ go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2) -- Rule S-FUN
+ = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
+ -- Match the args, and sub-match the results
+
+ go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
+ -- Otherwise defer to boxy matching
+ -- This covers TyConApp, AppTy, PredTy
+\end{code}
+
+Note [Sub-match]
+~~~~~~~~~~~~~~~~
+Consider this
+ head :: [a] -> a
+ |- head xs : <rhobox>
+We will do a boxySubMatchType between a ~ <rhobox>
+But we *don't* want to match [a |-> <rhobox>] because
+ (a) The box should be filled in with a rho-type, but
+ but the returned substitution maps TyVars to boxy
+ *sigma* types
+ (b) In any case, the right final answer might be *either*
+ instantiate 'a' with a rho-type or a sigma type
+ head xs : Int vs head xs : forall b. b->b
+So the matcher MUST NOT make a choice here. In general, we only
+bind a template type variable in boxyMatchType, not in boxySubMatchType.
+
+
+\begin{code}