X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=56652c7d8ce21aaf673930cd4853424665ef016d;hb=3d638f1b7b665c0e67e4e20827ad98cf307ff381;hp=9f5daeb0bc843eee9969f58dad8c4b5d7b432efb;hpb=654d07dd0fb679d014ac363e13c004b0086d0d6e;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 9f5daeb..56652c7 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -611,7 +611,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
                         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
@@ -1294,8 +1297,8 @@ Note [TyCon app]
 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.
 
@@ -1870,7 +1873,7 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (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