Fix Trac #4401: meta-tyvars allocated by the constraint solver are always touchable

  See Note [Touchable meta type variables] in TcSMonad

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 950d733..65330ac 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -35,7 +35,7 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
-  tcInstType, tcInstSigType,
+  tcInstType, tcInstSigType, instMetaTyVar,
   tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
   tcSkolSigType, tcSkolSigTyVars, 
 
@@ -305,6 +305,7 @@ newMetaTyVar meta_info kind
        ; let name = mkSysTvName uniq fs 
              fs = case meta_info of
                        TauTv   -> fsLit "t"
+                       TcsTv   -> fsLit "u"
                        SigTv _ -> fsLit "a"
        ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 93c795d..3c1961b 100644 (file)
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -566,40 +566,58 @@ pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 
 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
--- is touchable variable!
 isTouchableMetaTyVar tv 
-  | isMetaTyVar tv = do { untch <- getUntouchables
-                        ; return (inTouchableRange untch tv) }
-  | otherwise      = return False
+  = case tcTyVarDetails tv of
+      MetaTv TcsTv _ -> return True    -- See Note [Touchable meta type variables]
+      MetaTv {}      -> do { untch <- getUntouchables
+                           ; return (inTouchableRange untch tv) }
+      _              -> return False
+\end{code}
+
+Note [Touchable meta type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Meta type variables allocated *by the constraint solver itself* are always
+touchable.  Example: 
+   instance C a b => D [a] where...
+if we use this instance declaration we "make up" a fresh meta type
+variable for 'b', which we must later guess.  (Perhaps C has a
+functional dependency.)  But since we aren't in the constraint *generator*
+we can't allocate a Unique in the touchable range for this implication
+constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 
 
+\begin{code}
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 newFlattenSkolemTy :: TcType -> TcS TcType
 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
-  where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
-        newFlattenSkolemTyVar ty
-            = wrapTcS $ do { uniq <- TcM.newUnique
-                           ; let name = mkSysTvName uniq (fsLit "f")
-                           ; return $ 
-                             mkTcTyVar name (typeKind ty) (FlatSkol ty) 
-                           }
+
+newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
+newFlattenSkolemTyVar ty
+  = wrapTcS $ do { uniq <- TcM.newUnique
+                 ; let name = mkSysTvName uniq (fsLit "f")
+                 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 
 -- Instantiations 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
-instDFunTypes mb_inst_tys = 
-  let inst_tv :: Either TyVar TcType -> TcS Type
-      inst_tv (Left tv)  = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
-      inst_tv (Right ty) = return ty 
-  in mapM inst_tv mb_inst_tys
-
+instDFunTypes mb_inst_tys 
+  = mapM inst_tv mb_inst_tys
+  where
+    inst_tv :: Either TyVar TcType -> TcS Type
+    inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
+    inst_tv (Right ty) = return ty 
 
 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
 
+newFlexiTcS :: TyVar -> TcS TcTyVar
+-- Make a TcsTv meta tyvar; it is always touchable,
+-- but we are supposed to guess its instantiation
+-- See Note [Touchable meta type variables]
+newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
 
 -- Superclasses and recursive dictionaries 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -800,11 +818,13 @@ mkWantedFunDepEqns loc eqns
   where
     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
     to_work_item ((qtvs, pairs), _, _)
-      = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
-           ; mapM (do_one tenv) pairs }
+      = do { let tvs = varSetElems qtvs
+           ; tvs' <- mapM newFlexiTcS tvs
+           ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+           ; mapM (do_one subst) pairs }
 
-    do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1 
-                                      sty2 = substTy tenv ty2 
+    do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 
+                                       sty2 = substTy subst ty2 
                                 ; ev <- newWantedCoVar sty1 sty2
                                 ; return (WantedEvVar ev loc) }
 

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index b49dbff..b20d32e 100644 (file)
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -302,6 +302,11 @@ data MetaInfo
                   -- The Name is the name of the function from whose
                   -- type signature we got this skolem
 
+   | TcsTv        -- A MetaTv allocated by the constraint solver
+                  -- Its particular property is that it is always "touchable"
+                  -- Nevertheless, the constraint solver has to try to guess
+                  -- what type to instantiate it to
+
 ----------------------------------
 -- SkolemInfo describes a site where 
 --   a) type variables are skolemised
@@ -408,6 +413,7 @@ pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 pprTcTyVarDetails (SkolemTv _)         = ptext (sLit "sk")
 pprTcTyVarDetails (FlatSkol {})        = ptext (sLit "fsk")
 pprTcTyVarDetails (MetaTv TauTv _)     = ptext (sLit "tau")
+pprTcTyVarDetails (MetaTv TcsTv _)     = ptext (sLit "tcs")
 pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
 
 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
@@ -433,8 +439,9 @@ pprSkolTvBinding tv
   where
     ppr_details (SkolemTv info)      = ppr_skol info
     ppr_details (FlatSkol {})       = ptext (sLit "is a flattening type variable")
-    ppr_details (MetaTv TauTv _)     = ptext (sLit "is a meta type variable")
-    ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") <+> quotes (ppr n)
+    ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for")
+                                       <+> quotes (ppr n)
+    ppr_details (MetaTv _ _)         = ptext (sLit "is a meta type variable")
 
     ppr_skol UnkSkol       = ptext (sLit "is an unknown type variable")        -- Unhelpful
     ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type")
@@ -615,8 +622,8 @@ isTyConableTyVar tv
        -- not a SigTv
   = ASSERT( isTcTyVar tv) 
     case tcTyVarDetails tv of
-       MetaTv TauTv _ -> True
-       _              -> False
+       MetaTv (SigTv _) _ -> False
+       _                  -> True
        
 isSkolemTyVar tv 
   = ASSERT2( isTcTyVar tv, ppr tv )