Refactor occurrence-check logic
authorSimon Peyton Jones <simonpj@microsoft.com>
Sun, 25 Sep 2016 02:50:13 +0000 (03:50 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 21 Oct 2016 16:16:03 +0000 (17:16 +0100)
This patch does two related things

* Combines the occurrence-check logic in the on-the-fly unifier with
  that in the constraint solver.  They are both doing the same job,
  after all.  The resulting code is now in TcUnify:
     metaTyVarUpdateOK
     occCheckExpand
     occCheckForErrors (called in TcErrors)

* In doing this I disovered checking for family-free-ness and foralls
  can be unnecessarily inefficient, because it expands type synonyms.
  It's easy just to cache this info in the type syononym TyCon, which
  I am now doing.

13 files changed:
compiler/basicTypes/DataCon.hs
compiler/iface/TcIface.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/vectorise/Vectorise/Type/Env.hs

index 6fda33a..1cd90d1 100644 (file)
@@ -24,7 +24,7 @@ module DataCon (
         FieldLbl(..), FieldLabel, FieldLabelString,
 
         -- ** Type construction
-        mkDataCon, buildAlgTyCon, fIRST_TAG,
+        mkDataCon, buildAlgTyCon, buildSynTyCon, fIRST_TAG,
 
         -- ** Type deconstruction
         dataConRepType, dataConSig, dataConInstSig, dataConFullSig,
@@ -1310,3 +1310,11 @@ buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
                rhs parent gadt_syn
   where
     binders = mkTyConBindersPreferAnon ktvs liftedTypeKind
+
+buildSynTyCon :: Name -> [TyConBinder] -> Kind   -- ^ /result/ kind
+                  -> [Role] -> Type -> TyCon
+buildSynTyCon name binders res_kind roles rhs
+  = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+  where
+    is_tau      = isTauTy rhs
+    is_fam_free = isFamFreeTy rhs
index bb04883..1ad5114 100644 (file)
@@ -547,7 +547,7 @@ tc_iface_decl _ _ (IfaceSynonym {ifName = tc_name,
      { res_kind' <- tcIfaceType res_kind     -- Note [Synonym kind loop]
      ; rhs      <- forkM (mk_doc tc_name) $
                    tcIfaceType rhs_ty
-     ; let tycon = mkSynonymTyCon tc_name binders' res_kind' roles rhs
+     ; let tycon = buildSynTyCon tc_name binders' res_kind' roles rhs
      ; return (ATyCon tycon) }
    where
      mk_doc n = text "Type synonym" <+> ppr n
index 7430ec8..364aea4 100644 (file)
@@ -454,6 +454,8 @@ tYPETyCon = mkKindTyCon tYPETyConName
 unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
                           [] liftedTypeKind []
                           (tYPE (TyConApp ptrRepUnliftedDataConTyCon []))
+                          True   -- no foralls
+                          True   -- family free
 
 --------------------------
 -- ... and now their names
index a954f04..7f4d072 100644 (file)
@@ -1055,15 +1055,15 @@ liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon :: TyCon
 -- type *    = tYPE 'PtrRepLifted
 -- type *    = tYPE 'PtrRepLifted  -- Unicode variant
 
-liftedTypeKindTyCon   = mkSynonymTyCon liftedTypeKindTyConName
+liftedTypeKindTyCon   = buildSynTyCon liftedTypeKindTyConName
                                        [] liftedTypeKind []
                                        (tYPE ptrRepLiftedTy)
 
-starKindTyCon         = mkSynonymTyCon starKindTyConName
+starKindTyCon         = buildSynTyCon starKindTyConName
                                        [] liftedTypeKind []
                                        (tYPE ptrRepLiftedTy)
 
-unicodeStarKindTyCon  = mkSynonymTyCon unicodeStarKindTyConName
+unicodeStarKindTyCon  = buildSynTyCon unicodeStarKindTyConName
                                        [] liftedTypeKind []
                                        (tYPE ptrRepLiftedTy)
 
index d955d60..9caef47 100644 (file)
@@ -10,7 +10,7 @@ module TcCanonical(
 #include "HsVersions.h"
 
 import TcRnTypes
-import TcUnify( swapOverTyVars )
+import TcUnify( swapOverTyVars, metaTyVarUpdateOK )
 import TcType
 import Type
 import TcFlatten
@@ -1374,7 +1374,7 @@ canEqTyVar2 :: DynFlags
 -- preserved as much as possible
 
 canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-  | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2  -- No occurs check
+  | Just xi2' <- metaTyVarUpdateOK dflags tv1 xi2  -- No occurs check
      -- Must do the occurs check even on tyvar/tyvar
      -- equalities, in case have  x ~ (y :: ..x...)
      -- Trac #12593
@@ -1499,12 +1499,6 @@ canEqTyVarTyVar, are these
 
  * If either is a flatten-meta-variables, it goes on the left.
 
- * If one is a strict sub-kind of the other e.g.
-       (alpha::?) ~ (beta::*)
-   orient them so RHS is a subkind of LHS.  That way we will replace
-   'a' with 'b', correctly narrowing the kind.
-   This establishes the subkind invariant of CTyEqCan.
-
  * Put a meta-tyvar on the left if possible
        alpha[3] ~ r
 
index 7cf688d..783b6ef 100644 (file)
@@ -12,6 +12,7 @@ module TcErrors(
 import TcRnTypes
 import TcRnMonad
 import TcMType
+import TcUnify( occCheckForErrors, OccCheckResult(..) )
 import TcType
 import RnEnv( unknownNameSuggestions )
 import Type
@@ -1434,7 +1435,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
              tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
        ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, extra3, report] }
 
-  | OC_Forall <- occ_check_expand
+  | OC_Bad <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
                           <+> quotes (ppr tv1)
                         , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
@@ -1505,8 +1506,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
         -- Consider an ambiguous top-level constraint (a ~ F a)
         -- Not an occurs check, because F is a type function.
   where
-    occ_check_expand = occurCheckExpand dflags tv1 ty2
-    ty1    = mkTyVarTy tv1
+    ty1 = mkTyVarTy tv1
+    occ_check_expand = occCheckForErrors dflags tv1 ty2
 
     what = case ctLocTypeOrKind_maybe (ctLoc ct) of
       Just KindLevel -> text "kind"
index b575c51..24a3358 100644 (file)
@@ -12,6 +12,7 @@ module TcFlatten(
 import TcRnTypes
 import TcType
 import Type
+import TcUnify( occCheckExpand )
 import TcEvidence
 import TyCon
 import TyCoRep   -- performs delicate algorithm on types
@@ -21,7 +22,6 @@ import VarEnv
 import NameEnv
 import Outputable
 import TcSMonad as TcS
-import DynFlags( DynFlags )
 
 import Util
 import Bag
@@ -1448,8 +1448,7 @@ We must solve both!
 
 unflatten :: Cts -> Cts -> TcS Cts
 unflatten tv_eqs funeqs
- = do { dflags   <- getDynFlags
-      ; tclvl    <- getTcLevel
+ = do { tclvl    <- getTcLevel
 
       ; traceTcS "Unflattening" $ braces $
         vcat [ text "Funeqs =" <+> pprCts funeqs
@@ -1460,11 +1459,11 @@ unflatten tv_eqs funeqs
          --                 ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv]
          --                 ==> (unify)   [W] F [fmv] ~ fmv
          -- See Note [Unflatten using funeqs first]
-      ; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs
+      ; funeqs <- foldrBagM unflatten_funeq emptyCts funeqs
       ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
 
           -- Step 2: unify the tv_eqs, if possible
-      ; tv_eqs  <- foldrBagM (unflatten_eq dflags tclvl) emptyCts tv_eqs
+      ; tv_eqs  <- foldrBagM (unflatten_eq tclvl) emptyCts tv_eqs
       ; traceTcS "Unflattening 2" $ braces (pprCts tv_eqs)
 
           -- Step 3: fill any remaining fmvs with fresh unification variables
@@ -1483,25 +1482,25 @@ unflatten tv_eqs funeqs
       ; zonkSimples all_flat }
   where
     ----------------
-    unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts
-    unflatten_funeq dflags ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
+    unflatten_funeq :: Ct -> Cts -> TcS Cts
+    unflatten_funeq ct@(CFunEqCan { cc_fun = tc, cc_tyargs = xis
                                          , cc_fsk = fmv, cc_ev = ev }) rest
       = do {   -- fmv should be an un-filled flatten meta-tv;
                -- we now fix its final value by filling it, being careful
                -- to observe the occurs check.  Zonking will eliminate it
                -- altogether in due course
              rhs' <- zonkTcType (mkTyConApp tc xis)
-           ; case occurCheckExpand dflags fmv rhs' of
-               OC_OK rhs''    -- Normal case: fill the tyvar
+           ; case occCheckExpand fmv rhs' of
+               Just rhs''    -- Normal case: fill the tyvar
                  -> do { setEvBindIfWanted ev
                                (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
                        ; unflattenFmv fmv rhs''
                        ; return rest }
 
-               _ ->  -- Occurs check
-                     return (ct `consCts` rest) }
+               Nothing ->  -- Occurs check
+                          return (ct `consCts` rest) }
 
-    unflatten_funeq other_ct _
+    unflatten_funeq other_ct _
       = pprPanic "unflatten_funeq" (ppr other_ct)
 
     ----------------
@@ -1512,23 +1511,23 @@ unflatten tv_eqs funeqs
     finalise_funeq ct = pprPanic "finalise_funeq" (ppr ct)
 
     ----------------
-    unflatten_eq ::  DynFlags -> TcLevel -> Ct -> Cts -> TcS Cts
-    unflatten_eq dflags tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
+    unflatten_eq :: TcLevel -> Ct -> Cts -> TcS Cts
+    unflatten_eq tclvl ct@(CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest
       | isFmvTyVar tv   -- Previously these fmvs were untouchable,
                         -- but now they are touchable
                         -- NB: unlike unflattenFmv, filling a fmv here does
                         --     bump the unification count; it is "improvement"
                         -- Note [Unflattening can force the solver to iterate]
-      = do { lhs_elim <- tryFill dflags tv rhs ev
+      = do { lhs_elim <- tryFill tv rhs ev
            ; if lhs_elim then return rest else
-        do { rhs_elim <- try_fill dflags tclvl ev rhs (mkTyVarTy tv)
+        do { rhs_elim <- try_fill tclvl ev rhs (mkTyVarTy tv)
            ; if rhs_elim then return rest else
              return (ct `consCts` rest) } }
 
       | otherwise
       = return (ct `consCts` rest)
 
-    unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
+    unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
 
     ----------------
     finalise_eq :: Ct -> Cts -> TcS Cts
@@ -1549,33 +1548,33 @@ unflatten tv_eqs funeqs
     finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
 
     ----------------
-    try_fill dflags tclvl ev ty1 ty2
+    try_fill tclvl ev ty1 ty2
       | Just tv1 <- tcGetTyVar_maybe ty1
       , isTouchableOrFmv tclvl tv1
       , typeKind ty1 `eqType` tyVarKind tv1
-      = tryFill dflags tv1 ty2 ev
+      = tryFill tv1 ty2 ev
       | otherwise
       = return False
 
-tryFill :: DynFlags -> TcTyVar -> TcType -> CtEvidence -> TcS Bool
+tryFill :: TcTyVar -> TcType -> CtEvidence -> TcS Bool
 -- (tryFill tv rhs ev) sees if 'tv' is an un-filled MetaTv
 -- If so, and if tv does not appear in 'rhs', set tv := rhs
 -- bind the evidence (which should be a CtWanted) to Refl<rhs>
 -- and return True.  Otherwise return False
-tryFill dflags tv rhs ev
+tryFill tv rhs ev
   = ASSERT2( not (isGiven ev), ppr ev )
     do { is_filled <- isFilledMetaTyVar tv
        ; if is_filled then return False else
     do { rhs' <- zonkTcType rhs
-       ; case occurCheckExpand dflags tv rhs' of
-           OC_OK rhs''    -- Normal case: fill the tyvar
+       ; case occCheckExpand tv rhs' of
+           Just rhs''    -- Normal case: fill the tyvar
              -> do { setEvBindIfWanted ev
                                (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
                    ; unifyTyVar tv rhs''
                    ; return True }
 
-           _ ->  -- Occurs check
-                 return False } }
+           Nothing ->  -- Occurs check
+                      return False } }
 
 {-
 Note [Unflatten using funeqs first]
index b8db1d4..46784f6 100644 (file)
@@ -912,7 +912,7 @@ tcTySynRhs roles_info tc_name binders res_kind hs_ty
        ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; let roles = roles_info tc_name
-             tycon = mkSynonymTyCon tc_name binders res_kind roles rhs_ty
+             tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
        ; return tycon }
 
 tcDataDefn :: RolesInfo -> Name
index 159c6dc..c829936 100644 (file)
@@ -46,7 +46,6 @@ module TcType (
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar, isTouchableOrFmv,
   isFloatedTouchableMetaTyVar,
-  canUnifyWithPolyType,
 
   --------------------------------
   -- Builders
@@ -83,8 +82,8 @@ module TcType (
 
   ---------------------------------
   -- Misc type manipulators
-  deNoteType, occurCheckExpand, OccCheckResult(..),
-  occCheckExpand,
+
+  deNoteType,
   orphNamesOfType, orphNamesOfCo,
   orphNamesOfTypes, orphNamesOfCoCon,
   getDFunTyKey,
@@ -216,7 +215,6 @@ import BasicTypes
 import Util
 import Bag
 import Maybes
-import Pair( pFst )
 import Outputable
 import FastString
 import ErrUtils( Validity(..), MsgDoc, isValid )
@@ -224,7 +222,6 @@ import FV
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.IORef
-import Control.Monad (liftM, ap)
 import Data.Functor.Identity
 
 {-
@@ -1165,24 +1162,6 @@ mkSpecSigmaTy tyvars ty = mkSigmaTy (mkTyVarBinders Specified tyvars) ty
 mkPhiTy :: [PredType] -> Type -> Type
 mkPhiTy = mkFunTys
 
--- @isTauTy@ tests if a type is "simple"..
-isTauTy :: Type -> Bool
-isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
-isTauTy (TyVarTy _)           = True
-isTauTy (LitTy {})            = True
-isTauTy (TyConApp tc tys)     = all isTauTy tys && isTauTyCon tc
-isTauTy (AppTy a b)           = isTauTy a && isTauTy b
-isTauTy (FunTy a b)           = isTauTy a && isTauTy b
-isTauTy (ForAllTy {})         = False
-isTauTy (CastTy _ _)          = False
-isTauTy (CoercionTy _)        = False
-
-isTauTyCon :: TyCon -> Bool
--- Returns False for type synonyms whose expansion is a polytype
-isTauTyCon tc
-  | Just (_, rhs) <- synTyConDefn_maybe tc = isTauTy rhs
-  | otherwise                              = True
-
 ---------------
 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
                                 -- construct a dictionary function name
@@ -1567,262 +1546,6 @@ pickyEqType ty1 ty2
   = isNothing $
     tc_eq_type (const Nothing) ty1 ty2
 
-{-
-Note [Occurs check expansion]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
-of occurrences of tv outside type function arguments, if that is
-possible; otherwise, it returns Nothing.
-
-For example, suppose we have
-  type F a b = [a]
-Then
-  occurCheckExpand b (F Int b) = Just [Int]
-but
-  occurCheckExpand a (F a Int) = Nothing
-
-We don't promise to do the absolute minimum amount of expanding
-necessary, but we try not to do expansions we don't need to.  We
-prefer doing inner expansions first.  For example,
-  type F a b = (a, Int, a, [a])
-  type G b   = Char
-We have
-  occurCheckExpand b (F (G b)) = F Char
-even though we could also expand F to get rid of b.
-
-The two variants of the function are to support TcUnify.checkTauTvUpdate,
-which wants to prevent unification with type families. For more on this
-point, see Note [Prevent unification with type families] in TcUnify.
-
-Note [Occurrence checking: look inside kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are considering unifying
-   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
-This may be an error (what is that alpha doing inside beta's kind?),
-but we must not make the mistake of actuallyy unifying or we'll
-build an infinite data structure.  So when looking for occurrences
-of alpha in the rhs, we must look in the kinds of type variables
-that occur there.
-
-NB: we may be able to remove the problem via expansion; see
-    Note [Occurs check expansion].  So we have to try that.
-
-Note [Checking for foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Unless we have -XImpredicativeTypes (which is a totally unsupported
-feature), we do not want to unify
-    alpha ~ (forall a. a->a) -> Int
-So we look for foralls hidden inside the type, and it's convenient
-to do that at the same time as the occurs check (which looks for
-occurrences of alpha).
-
-However, it's not just a question of looking for foralls /anywhere/!
-Consider
-   (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
-This is legal; e.g. dependent/should_compile/T11635.
-
-We don't want to reject it because of the forall in beta's kind,
-but (see Note [Occurrence checking: look inside kinds]) we do
-need to look in beta's kind.  So we carry a flag saying if a 'forall'
-is OK, and sitch the flag on when stepping inside a kind.
-
-Why is it OK?  Why does it not count as impredicative polymorphism?
-The reason foralls are bad is because we reply on "seeing" foralls
-when doing implicit instantiation.  But the forall inside the kind is
-fine.  We'll generate a kind equality constraint
-  (forall k. k->*) ~ (forall k. k->*)
-to check that the kinds of lhs and rhs are compatible.  If alpha's
-kind had instead been
-  (alpha :: kappa)
-then this kind equality would rightly complain about unifying kappa
-with (forall k. k->*)
-
--}
-
-data OccCheckResult a
-  = OC_OK a
-  | OC_Forall
-  | OC_Occurs
-
-instance Functor OccCheckResult where
-      fmap = liftM
-
-instance Applicative OccCheckResult where
-      pure = OC_OK
-      (<*>) = ap
-
-instance Monad OccCheckResult where
-  OC_OK x       >>= k = k x
-  OC_Forall     >>= _ = OC_Forall
-  OC_Occurs     >>= _ = OC_Occurs
-
-occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
--- See Note [Occurs check expansion]
--- Check whether
---   a) the given variable occurs in the given type.
---   b) there is a forall in the type (unless we have -XImpredicativeTypes)
---
--- We may have needed to do some type synonym unfolding in order to
--- get rid of the variable (or forall), so we also return the unfolded
--- version of the type, which is guaranteed to be syntactically free
--- of the given type variable.  If the type is already syntactically
--- free of the variable, then the same type is returned.
---
--- NB: in the past we also rejected a SigTv matched with a non-tyvar
---     But it is wrong to reject that for Givens;
---     and SigTv is in any case handled separately by
---        - TcUnify.checkTauTvUpdate (on-the-fly unifier)
---        - TcInteract.canSolveByUnification (main constraint solver)
-occurCheckExpand dflags tv ty
-  = case fast_check impredicative ty of
-      OC_OK _   -> OC_OK ty
-      OC_Forall -> OC_Forall
-      OC_Occurs -> case occCheckExpand tv ty of
-                     Nothing  -> OC_Occurs
-                     Just ty' -> OC_OK ty'
-  where
-    details       = tcTyVarDetails tv
-    impredicative = canUnifyWithPolyType dflags details
-
-    ok :: OccCheckResult ()
-    ok = OC_OK ()
-
-    fast_check :: Bool -> TcType -> OccCheckResult ()
-      -- True <=> Foralls are ok; otherwise stop with OC_Forall
-      -- See Note [Checking for foralls]
-
-    fast_check _ (TyVarTy tv')
-      | tv == tv' = OC_Occurs
-      | otherwise = fast_check True (tyVarKind tv')
-           -- See Note [Occurrence checking: look inside kinds]
-
-    fast_check b (TyConApp tc tys)
-      | not (b || isTauTyCon tc) = OC_Forall
-      | otherwise                = mapM (fast_check b) tys >> ok
-    fast_check _ (LitTy {})      = ok
-    fast_check b (FunTy a r)     = fast_check b a   >> fast_check b r
-    fast_check b (AppTy fun arg) = fast_check b fun >> fast_check b arg
-    fast_check b (CastTy ty co)  = fast_check b ty >> fast_check_co co
-    fast_check _ (CoercionTy co) = fast_check_co co
-    fast_check b (ForAllTy (TvBndr tv' _) ty)
-       | not b     = OC_Forall
-       | tv == tv' = ok
-       | otherwise = do { fast_check True (tyVarKind tv')
-                        ; fast_check b ty }
-
-     -- we really are only doing an occurs check here; no bother about
-     -- impredicativity in coercions, as they're inferred
-    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
-                     | otherwise                       = ok
-
-
-occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
-occCheckExpand tv ty
-  = go emptyVarEnv ty
-  where
-    go :: VarEnv TyVar -> Type -> Maybe Type
-          -- The Varenv carries mappings necessary
-          -- because of kind expansion
-    go env (TyVarTy tv')
-      | tv == tv'                         = Nothing
-      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
-      | otherwise                         = do { k' <- go env (tyVarKind tv')
-                                               ; return (mkTyVarTy $
-                                                         setTyVarKind tv' k') }
-           -- See Note [Occurrence checking: look inside kinds]
-
-    go _   ty@(LitTy {}) = return ty
-    go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
-                                ; ty2' <- go env ty2
-                                ; return (mkAppTy ty1' ty2') }
-    go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
-                                ; ty2' <- go env ty2
-                                ; return (mkFunTy ty1' ty2') }
-    go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
-       | tv == tv'         = return ty
-       | otherwise         = do { ki' <- go env (tyVarKind tv')
-                                ; let tv'' = setTyVarKind tv' ki'
-                                      env' = extendVarEnv env tv' tv''
-                                ; body' <- go env' body_ty
-                                ; return (ForAllTy (TvBndr tv'' vis) body') }
-
-    -- For a type constructor application, first try expanding away the
-    -- offending variable from the arguments.  If that doesn't work, next
-    -- see if the type constructor is a type synonym, and if so, expand
-    -- it and try again.
-    go env ty@(TyConApp tc tys)
-      = case mapM (go env) tys of
-          Just tys' -> return (mkTyConApp tc tys')
-          Nothing | Just ty' <- coreView ty -> go env ty'
-                  | otherwise               -> Nothing
-                      -- Failing that, try to expand a synonym
-
-    go env (CastTy ty co) =  do { ty' <- go env ty
-                                ; co' <- go_co env co
-                                ; return (mkCastTy ty' co') }
-    go env (CoercionTy co) = do { co' <- go_co env co
-                                ; return (mkCoercionTy co') }
-
-    go_co env (Refl r ty)               = do { ty' <- go env ty
-                                             ; return (mkReflCo r ty') }
-      -- Note: Coercions do not contain type synonyms
-    go_co env (TyConAppCo r tc args)    = do { args' <- mapM (go_co env) args
-                                             ; return (mkTyConAppCo r tc args') }
-    go_co env (AppCo co arg)            = do { co' <- go_co env co
-                                             ; arg' <- go_co env arg
-                                             ; return (mkAppCo co' arg') }
-    go_co env co@(ForAllCo tv' kind_co body_co)
-      | tv == tv'         = return co
-      | otherwise         = do { kind_co' <- go_co env kind_co
-                               ; let tv'' = setTyVarKind tv' $
-                                            pFst (coercionKind kind_co')
-                                     env' = extendVarEnv env tv' tv''
-                               ; body' <- go_co env' body_co
-                               ; return (ForAllCo tv'' kind_co' body') }
-    go_co env (CoVarCo c)               = do { k' <- go env (varType c)
-                                             ; return (mkCoVarCo (setVarType c k')) }
-    go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
-                                             ; return (mkAxiomInstCo ax ind args') }
-    go_co env (UnivCo p r ty1 ty2)      = do { p' <- go_prov env p
-                                             ; ty1' <- go env ty1
-                                             ; ty2' <- go env ty2
-                                             ; return (mkUnivCo p' r ty1' ty2') }
-    go_co env (SymCo co)                = do { co' <- go_co env co
-                                             ; return (mkSymCo co') }
-    go_co env (TransCo co1 co2)         = do { co1' <- go_co env co1
-                                             ; co2' <- go_co env co2
-                                             ; return (mkTransCo co1' co2') }
-    go_co env (NthCo n co)              = do { co' <- go_co env co
-                                             ; return (mkNthCo n co') }
-    go_co env (LRCo lr co)              = do { co' <- go_co env co
-                                             ; return (mkLRCo lr co') }
-    go_co env (InstCo co arg)           = do { co' <- go_co env co
-                                             ; arg' <- go_co env arg
-                                             ; return (mkInstCo co' arg') }
-    go_co env (CoherenceCo co1 co2)     = do { co1' <- go_co env co1
-                                             ; co2' <- go_co env co2
-                                             ; return (mkCoherenceCo co1' co2') }
-    go_co env (KindCo co)               = do { co' <- go_co env co
-                                             ; return (mkKindCo co') }
-    go_co env (SubCo co)                = do { co' <- go_co env co
-                                             ; return (mkSubCo co') }
-    go_co env (AxiomRuleCo ax cs)       = do { cs' <- mapM (go_co env) cs
-                                             ; return (mkAxiomRuleCo ax cs') }
-
-    go_prov _   UnsafeCoerceProv    = return UnsafeCoerceProv
-    go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
-    go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
-    go_prov _   p@(PluginProv _)    = return p
-    go_prov _   p@(HoleProv _)      = return p
-
-canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
-canUnifyWithPolyType dflags details
-  = case details of
-      MetaTv { mtv_info = SigTv }    -> False
-      MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
-      _other                         -> True
-          -- We can have non-meta tyvars in given constraints
-
 {- Note [Expanding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we expand superclasses, we use the following algorithm:
index 4b0b749..dc436a3 100644 (file)
@@ -31,7 +31,10 @@ module TcUnify (
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  wrapFunResCoercion
+  wrapFunResCoercion,
+
+  occCheckExpand, metaTyVarUpdateOK,
+  occCheckForErrors, OccCheckResult(..)
 
   ) where
 
@@ -58,6 +61,8 @@ import BasicTypes
 import Name   ( Name )
 import Bag
 import Util
+import Pair( pFst )
+import qualified GHC.LanguageExtensions as LangExt
 import Outputable
 import FastString
 
@@ -1397,76 +1402,6 @@ maybe_sym :: SwapFlag -> Coercion -> Coercion
 maybe_sym IsSwapped  = mkSymCo
 maybe_sym NotSwapped = id
 
-----------------
-metaTyVarUpdateOK :: DynFlags
-                  -> TcTyVar             -- tv :: k1
-                  -> TcType              -- ty :: k2
-                  -> Maybe TcType        -- possibly-expanded ty
--- (metaTyFVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty.
--- Check (a) that tv doesn't occur in ty (occurs check)
---       (b) that ty does not have any foralls
---           (in the impredicative case), or type functions
---
--- We have two possible outcomes:
--- (1) Return the type to update the type variable with,
---        [we know the update is ok]
--- (2) Return Nothing,
---        [the update might be dodgy]
---
--- Note that "Nothing" does not mean "definite error".  For example
---   type family F a
---   type instance F Int = Int
--- consider
---   a ~ F a
--- This is perfectly reasonable, if we later get a ~ Int.  For now, though,
--- we return Nothing, leaving it to the later constraint simplifier to
--- sort matters out.
-
-metaTyVarUpdateOK dflags tv ty
-  = case defer_me impredicative ty of
-      OC_OK _   -> Just ty
-      OC_Forall -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand tv ty
-  where
-    details       = tcTyVarDetails tv
-    impredicative = canUnifyWithPolyType dflags details
-
-    defer_me :: Bool    -- True <=> foralls are ok
-             -> TcType
-             -> OccCheckResult ()
-    -- Checks for (a) occurrence of tv
-    --            (b) type family applications
-    --            (c) foralls if the Bool is false
-    -- See Note [Prevent unification with type families]
-    -- See Note [Refactoring hazard: checkTauTvUpdate]
-    -- See Note [Checking for foralls] in TcType
-
-    defer_me _ (TyVarTy tv')
-       | tv == tv' = OC_Occurs
-       | otherwise = defer_me True (tyVarKind tv')
-    defer_me b (TyConApp tc tys)
-       | isTypeFamilyTyCon tc = OC_Forall   -- We use OC_Forall to signal
-                                            -- forall /or/ type function
-       | not (isTauTyCon tc)  = OC_Forall
-       | otherwise            = mapM (defer_me b) tys >> OC_OK ()
-
-    defer_me b (ForAllTy (TvBndr tv' _) t)
-       | not b     = OC_Forall
-       | tv == tv' = OC_OK ()
-       | otherwise = do { defer_me True (tyVarKind tv'); defer_me b t }
-
-    defer_me _ (LitTy {})        = OC_OK ()
-    defer_me b (FunTy fun arg)   = defer_me b fun >> defer_me b arg
-    defer_me b (AppTy fun arg)   = defer_me b fun >> defer_me b arg
-    defer_me b (CastTy ty co)    = defer_me b ty  >> defer_me_co co
-    defer_me _ (CoercionTy co)   = defer_me_co co
-
-      -- We don't really care if there are type families in a coercion,
-      -- but we still can't have an occurs-check failure
-    defer_me_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
-                   | otherwise                       = OC_OK ()
-
 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
 -- See Note [Canonical orientation for tyvar/tyvar equality constraints]
 swapOverTyVars tv1 tv2
@@ -2021,4 +1956,3 @@ canUnifyWithPolyType dflags details
       MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
       _other                         -> True
           -- We can have non-meta tyvars in given constraints
-
index 5778ca8..40e8562 100644 (file)
@@ -50,6 +50,7 @@ module TyCon(
         mightBeUnsaturatedTyCon,
         isPromotedDataCon, isPromotedDataCon_maybe,
         isKindTyCon, isLiftedTypeKindTyConName,
+        isTauTyCon, isFamFreeTyCon,
 
         isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
         isDataSumTyCon_maybe,
@@ -619,8 +620,16 @@ data TyCon
                                  -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
-        synTcRhs     :: Type     -- ^ Contains information about the expansion
+        synTcRhs     :: Type,    -- ^ Contains information about the expansion
                                  -- of the synonym
+
+        synIsTau     :: Bool,   -- True <=> the RHS of this synonym does not
+                                 --          have any foralls, after expanding any
+                                 --          nested synonyms
+        synIsFamFree  :: Bool    -- True <=> the RHS of this synonym does mention
+                                 --          any type synonym families (data families
+                                 --          are fine), again after expanding any
+                                 --          nested synonyms
     }
 
   -- | Represents families (both type and data)
@@ -1543,8 +1552,8 @@ mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
 
 -- | Create a type synonym 'TyCon'
 mkSynonymTyCon :: Name -> [TyConBinder] -> Kind   -- ^ /result/ kind
-               -> [Role] -> Type -> TyCon
-mkSynonymTyCon name binders res_kind roles rhs
+               -> [Role] -> Type -> Bool -> Bool -> TyCon
+mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
   = SynonymTyCon {
         tyConName    = name,
         tyConUnique  = nameUnique name,
@@ -1554,7 +1563,9 @@ mkSynonymTyCon name binders res_kind roles rhs
         tyConArity   = length binders,
         tyConTyVars  = binderVars binders,
         tcRoles      = roles,
-        synTcRhs     = rhs
+        synTcRhs     = rhs,
+        synIsTau     = is_tau,
+        synIsFamFree = is_fam_free
     }
 
 -- | Create a type family 'TyCon'
@@ -1805,6 +1816,14 @@ isTypeSynonymTyCon :: TyCon -> Bool
 isTypeSynonymTyCon (SynonymTyCon {}) = True
 isTypeSynonymTyCon _                 = False
 
+isTauTyCon :: TyCon -> Bool
+isTauTyCon (SynonymTyCon { synIsTau = is_tau }) = is_tau
+isTauTyCon _                                    = True
+
+isFamFreeTyCon :: TyCon -> Bool
+isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
+isFamFreeTyCon (FamilyTyCon { famTcFlav = flav })         = isDataFamFlav flav
+isFamFreeTyCon _                                          = True
 
 -- As for newtypes, it is in some contexts important to distinguish between
 -- closed synonyms and synonym families, as synonym families have no unique
index bf92c37..f615757 100644 (file)
@@ -99,7 +99,7 @@ module Type (
         -- ** Predicates on types
         isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
         isCoercionTy_maybe, isCoercionType, isForAllTy,
-        isPiTy,
+        isPiTy, isTauTy, isFamFreeTy,
 
         -- (Lifting and boxity)
         isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
@@ -1383,6 +1383,17 @@ partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
     go _ _ xs = ([], xs)  -- something is ill-kinded. But this can happen
                           -- when printing errors. Assume everything is visible.
 
+-- @isTauTy@ tests if a type has no foralls
+isTauTy :: Type -> Bool
+isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
+isTauTy (TyVarTy _)           = True
+isTauTy (LitTy {})            = True
+isTauTy (TyConApp tc tys)     = all isTauTy tys && isTauTyCon tc
+isTauTy (AppTy a b)           = isTauTy a && isTauTy b
+isTauTy (FunTy a b)           = isTauTy a && isTauTy b
+isTauTy (ForAllTy {})         = False
+isTauTy (CastTy ty _)         = isTauTy ty
+isTauTy (CoercionTy _)        = False  -- Not sure about this
 
 {-
 %************************************************************************
@@ -1829,6 +1840,18 @@ pprSourceTyCon tycon
   | otherwise
   = ppr tycon
 
+-- @isTauTy@ tests if a type has no foralls
+isFamFreeTy :: Type -> Bool
+isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty'
+isFamFreeTy (TyVarTy _)       = True
+isFamFreeTy (LitTy {})        = True
+isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
+isFamFreeTy (AppTy a b)       = isFamFreeTy a && isFamFreeTy b
+isFamFreeTy (FunTy a b)       = isFamFreeTy a && isFamFreeTy b
+isFamFreeTy (ForAllTy _ ty)   = isFamFreeTy ty
+isFamFreeTy (CastTy ty _)     = isFamFreeTy ty
+isFamFreeTy (CoercionTy _)    = False  -- Not sure about this
+
 {-
 ************************************************************************
 *                                                                      *
index b6c8bec..421b1dd 100644 (file)
@@ -360,7 +360,7 @@ vectTypeEnv tycons vectTypeDecls vectClassDecls
         origName  = tyConName origTyCon
         vectName  = tyConName vectTyCon
 
-        mkSyn canonName ty = mkSynonymTyCon canonName [] (typeKind ty) [] ty
+        mkSyn canonName ty = buildSynTyCon canonName [] (typeKind ty) [] ty
 
         defDataCons
           | isAbstract = return ()