Put the decision of when a unification variable can unify with a polytype
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Nov 2014 10:59:49 +0000 (10:59 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Nov 2014 11:35:24 +0000 (11:35 +0000)
This was being doing independently in two places. Now it's done in one
place, TcType.canUnifyWithPolyType

compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs

index a9b44ab..5665730 100644 (file)
@@ -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}
index eb39038..966e564 100644 (file)
@@ -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