[commit: ghc] master: Put the decision of when a unification variable can unify with a polytype (073119e)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/073119e8e3eff54e64e2f89aa3a00dcf87b36ded/ghc

>---------------------------------------------------------------

commit 073119e8e3eff54e64e2f89aa3a00dcf87b36ded
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Nov 21 10:59:49 2014 +0000

    Put the decision of when a unification variable can unify with a polytype
    
    This was being doing independently in two places. Now it's done in one
    place, TcType.canUnifyWithPolyType


>---------------------------------------------------------------

073119e8e3eff54e64e2f89aa3a00dcf87b36ded
 compiler/typecheck/TcType.lhs  | 40 ++++++++++++++++++++++++++++++----------
 compiler/typecheck/TcUnify.lhs | 26 +++-----------------------
 2 files changed, 33 insertions(+), 33 deletions(-)

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index a9b44ab..5665730 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -41,6 +41,7 @@ module TcType (
   metaTyVarUntouchables, setMetaTyVarUntouchables, metaTyVarUntouchables_maybe,
   isTouchableMetaTyVar, isTouchableOrFmv,
   isFloatedTouchableMetaTyVar,
+  canUnifyWithPolyType,
 
   --------------------------------
   -- Builders
@@ -1202,16 +1203,7 @@ occurCheckExpand dflags tv ty
   where
     details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
 
-    impredicative
-      = case details of
-          MetaTv { mtv_info = ReturnTv } -> True
-          MetaTv { mtv_info = SigTv }    -> False
-          MetaTv { mtv_info = TauTv }    -> xopt Opt_ImpredicativeTypes dflags
-                                         || isOpenTypeKind (tyVarKind tv)
-                                          -- Note [OpenTypeKind accepts foralls]
-                                          -- in TcUnify
-          _other                         -> True
-          -- We can have non-meta tyvars in given constraints
+    impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
 
     -- Check 'ty' is a tyvar, or can be expanded into one
     go_sig_tv ty@(TyVarTy {})            = OC_OK ty
@@ -1259,8 +1251,36 @@ occurCheckExpand dflags tv ty
           bad | Just ty' <- tcView ty -> go ty'
               | otherwise             -> bad
                       -- Failing that, try to expand a synonym
+
+canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> TcKind -> Bool
+canUnifyWithPolyType dflags details kind
+  = case details of
+      MetaTv { mtv_info = ReturnTv } -> True      -- See Note [ReturnTv]
+      MetaTv { mtv_info = SigTv }    -> False
+      MetaTv { mtv_info = TauTv }    -> xopt Opt_ImpredicativeTypes dflags
+                                     || isOpenTypeKind kind
+                                          -- Note [OpenTypeKind accepts foralls]
+      _other                         -> True
+          -- We can have non-meta tyvars in given constraints
 \end{code}
 
+Note [OpenTypeKind accepts foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is a common paradigm:
+   foo :: (forall a. a -> a) -> Int
+   foo = error "urk"
+To make this work we need to instantiate 'error' with a polytype.
+A similar case is
+   bar :: Bool -> (forall a. a->a) -> Int
+   bar True = \x. (x 3)
+   bar False = error "urk"
+Here we need to instantiate 'error' with a polytype.
+
+But 'error' has an OpenTypeKind type variable, precisely so that
+we can instantiate it with Int#.  So we also allow such type variables
+to be instantiate with foralls.  It's a bit of a hack, but seems
+straightforward.
+
 %************************************************************************
 %*                                                                      *
 \subsection{Predicate types}
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index eb39038..966e564 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1011,13 +1011,10 @@ checkTauTvUpdate dflags tv ty
                    _ -> return Nothing
               | otherwise   -> return (Just ty1) }
   where
-    info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
-      -- See Note [ReturnTv] in TcType
+    details = ASSERT2( isMetaTyVar tv, ppr tv ) tcTyVarDetails tv
+    info         = mtv_info details
     is_return_tv = case info of { ReturnTv -> True; _ -> False }
-
-    impredicative = xopt Opt_ImpredicativeTypes dflags
-                 || isOpenTypeKind (tyVarKind tv)
-                       -- Note [OpenTypeKind accepts foralls]
+    impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
 
     defer_me :: TcType -> Bool
     -- Checks for (a) occurrence of tv
@@ -1031,23 +1028,6 @@ checkTauTvUpdate dflags tv ty
     defer_me (ForAllTy _ ty)   = not impredicative || defer_me ty
 \end{code}
 
-Note [OpenTypeKind accepts foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here is a common paradigm:
-   foo :: (forall a. a -> a) -> Int
-   foo = error "urk"
-To make this work we need to instantiate 'error' with a polytype.
-A similar case is
-   bar :: Bool -> (forall a. a->a) -> Int
-   bar True = \x. (x 3)
-   bar False = error "urk"
-Here we need to instantiate 'error' with a polytype.
-
-But 'error' has an OpenTypeKind type variable, precisely so that
-we can instantiate it with Int#.  So we also allow such type variables
-to be instantiate with foralls.  It's a bit of a hack, but seems
-straightforward.
-
 Note [Conservative unification check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When unifying (tv ~ rhs), w try to avoid creating deferred constraints