Beautiful new approach to the skolem-escape check and untouchable
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index 8a81b48..950d733 100644 (file)
@@ -57,6 +57,7 @@ module TcMType (
   zonkTcType, zonkTcTypes, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, 
   zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+  zonkTcTypeAndSubst,
   tcGetGlobalTyVars, 
 
   readKindVar, writeKindVar
@@ -299,7 +300,7 @@ tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 -- Make a new meta tyvar out of thin air
 newMetaTyVar meta_info kind
-  = do { uniq <- newUnique
+  = do { uniq <- newMetaUnique
        ; ref <- newMutVar Flexi
        ; let name = mkSysTvName uniq fs 
              fs = case meta_info of
@@ -311,7 +312,7 @@ instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
 -- Make a new meta tyvar whose Name and Kind 
 -- come from an existing TyVar
 instMetaTyVar meta_info tyvar
-  = do { uniq <- newUnique
+  = do { uniq <- newMetaUnique
        ; ref <- newMutVar Flexi
        ; let name = setNameUnique (tyVarName tyvar) uniq
              kind = tyVarKind tyvar
@@ -468,7 +469,7 @@ tcGetGlobalTyVars :: TcM TcTyVarSet
 tcGetGlobalTyVars
   = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
        ; gbl_tvs  <- readMutVar gtv_var
-       ; gbl_tvs' <- zonkTcTyVarsAndFV (varSetElems gbl_tvs)
+       ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
        ; writeMutVar gtv_var gbl_tvs'
        ; return gbl_tvs' }
 \end{code}
@@ -479,31 +480,29 @@ tcGetGlobalTyVars
 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 
-zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
+zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
 
 -----------------  Types
 
 zonkTcTypeCarefully :: TcType -> TcM TcType
+-- Do not zonk type variables free in the environment
 zonkTcTypeCarefully ty
   = do { env_tvs <- tcGetGlobalTyVars
-       ; zonkType (zonkTcTyVarCarefully env_tvs) ty }
-
-
-zonkTcTyVarCarefully :: TcTyVarSet -> TcTyVar -> TcM TcType
--- Do not zonk type variables free in the environment
-zonkTcTyVarCarefully env_tvs tv 
-  | tv `elemVarSet` env_tvs 
-  = return (TyVarTy tv)
-  | otherwise
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-      SkolemTv {}  -> return (TyVarTy tv)
-      FlatSkol ty  -> zonkType (zonkTcTyVarCarefully env_tvs) ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
-                            Flexi       -> return (TyVarTy tv)
-                            Indirect ty -> zonkType (zonkTcTyVarCarefully env_tvs) ty }
+       ; zonkType (zonk_tv env_tvs) ty }
+  where
+    zonk_tv env_tvs tv
+      | tv `elemVarSet` env_tvs 
+      = return (TyVarTy tv)
+      | otherwise
+      = ASSERT( isTcTyVar tv )
+       case tcTyVarDetails tv of
+         SkolemTv {}    -> return (TyVarTy tv)
+         FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> return (TyVarTy tv)
+                                  Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 
 zonkTcType :: TcType -> TcM TcType
 -- Simply look through all Flexis
@@ -514,12 +513,29 @@ zonkTcTyVar :: TcTyVar -> TcM TcType
 zonkTcTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-      SkolemTv {}  -> return (TyVarTy tv)
+      SkolemTv {}    -> return (TyVarTy tv)
       FlatSkol ty  -> zonkTcType ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
-                            Flexi       -> return (TyVarTy tv)
-                            Indirect ty -> zonkTcType ty }
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> return (TyVarTy tv)
+                              Indirect ty -> zonkTcType ty }
+
+zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
+-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
+zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
+  where
+    zonk_tv tv 
+      = case tcTyVarDetails tv of
+         SkolemTv {}    -> return (TyVarTy tv)
+         FlatSkol ty    -> zonkType zonk_tv ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> zonk_flexi tv
+                                  Indirect ty -> zonkType zonk_tv ty }
+    zonk_flexi tv
+      = case lookupTyVar subst tv of
+          Just ty -> zonkType zonk_tv ty
+          Nothing -> return (TyVarTy tv)
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mapM zonkTcType tys
@@ -567,8 +583,10 @@ zonkQuantifiedTyVar tv
        -- Create the new, frozen, skolem type variable
         -- We zonk to a skolem, not to a regular TcVar
         -- See Note [Zonking to Skolem]
+        ; uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
        ; let final_kind = defaultKind (tyVarKind tv)
-             final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
+              final_name = setNameUnique (tyVarName tv) uniq
+             final_tv   = mkSkolTyVar final_name final_kind UnkSkol
 
        -- Bind the meta tyvar to the new tyvar
        ; case details of
@@ -585,13 +603,11 @@ zonkQuantifiedTyVar tv
 
 \begin{code}
 zonkImplication :: Implication -> TcM Implication
-zonkImplication implic@(Implic { ic_env_tvs = env_tvs, ic_given = given 
+zonkImplication implic@(Implic { ic_given = given 
                                , ic_wanted = wanted })
-  = do { env_tvs' <- zonkTcTyVarsAndFV (varSetElems env_tvs)
-       ; given'   <- mapM zonkEvVar given
+  = do { given'   <- mapM zonkEvVar given
        ; wanted'  <- mapBagM zonkWanted wanted
-       ; return (implic { ic_env_tvs = env_tvs', ic_given = given'
-                        , ic_wanted = wanted' }) }
+       ; return (implic { ic_given = given', ic_wanted = wanted' }) }
 
 zonkEvVar :: EvVar -> TcM EvVar
 zonkEvVar var = do { ty' <- zonkTcType (varType var)
@@ -734,12 +750,12 @@ mkZonkTcTyVar :: (TcTyVar -> TcM Type)    -- What to do for an unbound mutable var
 mkZonkTcTyVar unbound_var_fn tyvar 
   = ASSERT( isTcTyVar tyvar )
     case tcTyVarDetails tyvar of
-      SkolemTv {}  -> return (TyVarTy tyvar)
-      FlatSkol ty  -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
-                            Flexi       -> unbound_var_fn tyvar  
-                            Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
+      SkolemTv {}    -> return (TyVarTy tyvar)
+      FlatSkol ty    -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> unbound_var_fn tyvar  
+                              Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
 
 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable 
 -- (their kind contains types).
@@ -817,10 +833,10 @@ checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty = do
     traceTc "checkValidType" (ppr ty)
-    unboxed  <- doptM Opt_UnboxedTuples
-    rank2    <- doptM Opt_Rank2Types
-    rankn    <- doptM Opt_RankNTypes
-    polycomp <- doptM Opt_PolymorphicComponents
+    unboxed  <- xoptM Opt_UnboxedTuples
+    rank2    <- xoptM Opt_Rank2Types
+    rankn    <- xoptM Opt_RankNTypes
+    polycomp <- xoptM Opt_PolymorphicComponents
     let 
        gen_rank n | rankn     = ArbitraryRank
                   | rank2     = Rank 2
@@ -950,7 +966,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
          checkTc (tyConArity tc <= length tys) arity_msg
 
        -- See Note [Liberal type synonyms]
-       ; liberal <- doptM Opt_LiberalTypeSynonyms
+       ; liberal <- xoptM Opt_LiberalTypeSynonyms
        ; if not liberal || isSynFamilyTyCon tc then
                -- For H98 and synonym families, do check the type args
                mapM_ (check_mono_type SynArgMonoType) tys
@@ -962,10 +978,10 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
     }
     
   | isUnboxedTupleTyCon tc
-  = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples
+  = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
        ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
 
-       ; impred <- doptM Opt_ImpredicativeTypes        
+       ; impred <- xoptM Opt_ImpredicativeTypes        
        ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
                -- c.f. check_arg_type
                -- However, args are allowed to be unlifted, or
@@ -1009,7 +1025,7 @@ check_arg_type :: Rank -> Type -> TcM ()
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type rank ty 
-  = do { impred <- doptM Opt_ImpredicativeTypes
+  = do { impred <- xoptM Opt_ImpredicativeTypes
        ; let rank' = case rank of          -- Predictive => must be monotype
                        MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
                        _other | impred    -> ArbitraryRank
@@ -1142,7 +1158,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
   = do {       -- Equational constraints are valid in all contexts if type
                -- families are permitted
-       ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+       ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
 
                -- Check the form of the argument types
        ; checkValidMonoType ty1
@@ -1173,8 +1189,8 @@ check_class_pred_tys dflags ctxt tys
                                -- checkInstTermination
        _             -> flexible_contexts || all tyvar_head tys
   where
-    flexible_contexts = dopt Opt_FlexibleContexts dflags
-    undecidable_ok = dopt Opt_UndecidableInstances dflags
+    flexible_contexts = xopt Opt_FlexibleContexts dflags
+    undecidable_ok = xopt Opt_UndecidableInstances dflags
 
 -------------------------
 tyvar_head :: Type -> Bool
@@ -1355,13 +1371,13 @@ checkValidInstHead ty   -- Should be a source type
 check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
 check_inst_head dflags clas tys
   = do { -- If GlasgowExts then check at least one isn't a type variable
-       ; checkTc (dopt Opt_TypeSynonymInstances dflags ||
+       ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
                   all tcInstHeadTyNotSynonym tys)
                  (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
-       ; checkTc (dopt Opt_FlexibleInstances dflags ||
+       ; checkTc (xopt Opt_FlexibleInstances dflags ||
                   all tcInstHeadTyAppAllTyVars tys)
                  (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
-       ; checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+       ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
                   isSingleton tys)
                  (instTypeErr (pprClassPred clas tys) head_one_type_msg)
          -- May not contain type family applications
@@ -1412,7 +1428,7 @@ checkValidInstance hs_type tyvars theta tau
     do { (clas, inst_tys) <- setSrcSpan head_loc $
                               checkValidInstHead tau
 
-        ; undecidable_ok <- doptM Opt_UndecidableInstances
+        ; undecidable_ok <- xoptM Opt_UndecidableInstances
 
        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
@@ -1513,7 +1529,7 @@ checkValidTypeInst typats rhs
        ; checkValidMonoType rhs
 
          -- we have a decidable instance unless otherwise permitted
-       ; undecidable_ok <- doptM Opt_UndecidableInstances
+       ; undecidable_ok <- xoptM Opt_UndecidableInstances
        ; unless undecidable_ok $
           mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
        }
@@ -1616,14 +1632,12 @@ sizeTypes xs               = sum (map sizeType xs)
 
 -- Size of a predicate
 --
--- Equalities are a special case.  The equality itself doesn't contribute to the
--- size and as we do not count class predicates, we have to start with one less.
--- This is easy to see considering that, given
---   class C a b | a -> b
---   type family F a
--- constraints (C a b) and (F a ~ b) are equivalent in size.
+-- We are considering whether *class* constraints terminate
+-- Once we get into an implicit parameter or equality we
+-- can't get back to a class constraint, so it's safe
+-- to say "size 0".  See Trac #4200.
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
-sizePred (IParam _ ty)     = sizeType ty
-sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2 - 1
+sizePred (IParam {})       = 0
+sizePred (EqPred {})       = 0
 \end{code}