Beautiful new approach to the skolem-escape check and untouchable
[ghc.git] / compiler / typecheck / TcMType.lhs
index 84fb1b8..950d733 100644 (file)
@@ -300,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
@@ -312,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
@@ -497,12 +497,12 @@ zonkTcTypeCarefully ty
       | otherwise
       = ASSERT( isTcTyVar tv )
        case tcTyVarDetails tv of
-         SkolemTv {}  -> return (TyVarTy tv)
+         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 }
+         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
@@ -513,12 +513,12 @@ 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
@@ -526,12 +526,12 @@ 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 }
+         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
@@ -583,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
@@ -601,13 +603,11 @@ zonkQuantifiedTyVar tv
 
 \begin{code}
 zonkImplication :: Implication -> TcM Implication
-zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given 
+zonkImplication implic@(Implic { ic_given = given 
                                , ic_wanted = wanted })
-  = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs
-       ; given'   <- mapM zonkEvVar given
+  = do { given'   <- mapM zonkEvVar given
        ; wanted'  <- mapBagM zonkWanted wanted
-       ; return (implic { ic_untch = 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)
@@ -750,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).