Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ (TyVarTy tv) | isMetaTyVar tv
+ go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+ -- NB: A TyVar (not TcTyVar) is possible here, representing
+ -- a skolem, because in this pure boxy_match function
+ -- we don't instantiate foralls to TcTyVars; cf Trac #2714
= subst -- Don't fail if the template has more info than the target!
-- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
-- would fail to instantiate 'a', because the meta-type-variable
When we find two TyConApps, the argument lists are guaranteed equal
length. Reason: intially the kinds of the two types to be unified is
the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
which we do, that ensures that f1,f2 have the same kind; and that
means a1,a2 have the same kind. And now the argument repeats.
-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
-- If the flag is False, it requires k <: sk
-- E.g. kindSimpleKind False ?? = *
--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where