Zonk quantified tyvars with skolems

We used to zonk quantified type variables to regular TyVars.  However, this
leads to problems.  Consider this program from the regression test suite:

  eval :: Int -> String -> String -> String
  eval 0 root actual = evalRHS 0 root actual

  evalRHS :: Int -> a
  evalRHS 0 root actual = eval 0 root actual

It leads to the deferral of an equality

  (String -> String -> String) ~ a

which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
In the meantime `a' is zonked and quantified to form `evalRHS's signature.
This has the *side effect* of also zonking the `a' in the deferred equality
(which at this point is being handed around wrapped in an implication
constraint).

Finally, the equality (with the zonked `a') will be handed back to the
simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
If we zonk `a' with a regular type variable, we will have this regular type
variable now floating around in the simplifier, which in many places assumes to
only see proper TcTyVars.

We can avoid this problem by zonking with a skolem.  The skolem is rigid
(which we requirefor a quantified variable), but is still a TcTyVar that the
simplifier knows how to deal with.

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index ebcf5b3..bcd99b5 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -756,17 +756,17 @@ zonkTopTyVar tv
     k = tyVarKind tv
     default_k = defaultKind k
 
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
 
-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 --
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 --                     -- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+-- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
@@ -780,9 +780,11 @@ zonkQuantifiedTyVar tv
   | otherwise  -- It's a meta-type-variable
   = do { details <- readMetaTyVar tv
 
-       -- Create the new, frozen, regular type variable
+       -- Create the new, frozen, skolem type variable
+        -- We zonk to a skolem, not to a regular TcVar
+        -- See Note [Zonking to Skolem]
        ; let final_kind = defaultKind (tyVarKind tv)
-             final_tv   = mkTyVar (tyVarName tv) final_kind
+             final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
 
        -- Bind the meta tyvar to the new tyvar
        ; case details of
@@ -797,8 +799,8 @@ zonkQuantifiedTyVar tv
        ; return final_tv }
 \end{code}
 
-[Silly Type Synonyms]
-
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
        type C u a = u  -- Note 'a' unused
 
@@ -832,6 +834,37 @@ Consider this:
 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 a /\a in the final result but all the occurrences of a will be zonked to ()
 
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars.  However, this
+leads to problems.  Consider this program from the regression test suite:
+
+  eval :: Int -> String -> String -> String
+  eval 0 root actual = evalRHS 0 root actual
+
+  evalRHS :: Int -> a
+  evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality
+
+  (String -> String -> String) ~ a
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem.  The skolem is rigid
+(which we requirefor a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
+
 
 %************************************************************************
 %*                                                                     *

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 3be5415..f5bdc51 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -3110,11 +3110,6 @@ mkMonomorphismMsg tidy_env inst_tvs
                nest 2 (vcat docs),
                monomorphism_fix dflags]
 
-isRuntimeUnk :: TyVar -> Bool
-isRuntimeUnk x | isTcTyVar x
-               , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
   = ptext SLIT("Probable fix:") <+> vcat

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index 4e3f728..19fe506 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -1236,7 +1236,7 @@ ppr_ty env ty
 -- (ppr_extra env ty) shows extra info about 'ty'
 ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
 ppr_extra env (TyVarTy tv)
-  | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv)
+  | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
   = return (env1, pprSkolTvBinding tv1)
   where
     (env1, tv1) = tidySkolemTyVar env tv

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 1d4d166..e96fdd4 100644 (file)
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -38,7 +38,7 @@ module TcType (
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isBoxyTyVar, 
   isSigTyVar, isExistentialTyVar,  isTyConableTyVar,
   metaTvRef, 
-  isFlexi, isIndirect, 
+  isFlexi, isIndirect, isRuntimeUnk, isUnk,
 
   --------------------------------
   -- Builders
@@ -556,6 +556,16 @@ isFlexi other     = False
 
 isIndirect (Indirect _) = True
 isIndirect other        = False
+
+isRuntimeUnk :: TyVar -> Bool
+isRuntimeUnk x | isTcTyVar x
+               , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
+               | otherwise = False
+
+isUnk :: TyVar -> Bool
+isUnk x | isTcTyVar x
+        , SkolemTv UnkSkol <- tcTyVarDetails x = True
+        | otherwise = False
 \end{code}
 
 

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index af7463d..7256940 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -200,7 +200,10 @@ subFunTys error_herald n_pats res_ty thing_inside
       = do { arg_tys <- newFlexiTyVarTys n argTypeKind
            ; res_ty' <- newFlexiTyVarTy openTypeKind
            ; let fun_ty = mkFunTys arg_tys res_ty'
-           ; coi <- defer_unification False False fun_ty ty
+                 err    = error_herald <> comma $$
+                          text "which does not match its type"
+           ; coi <- addErrCtxt err $
+                      defer_unification False False fun_ty ty
            ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
            ; return (coiToHsWrapper coi, res)
            }