Commit cad764aa authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

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.
parent 3f1d7cd8
......@@ -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.
%************************************************************************
%* *
......
......@@ -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
......
......@@ -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
......
......@@ -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}
......
......@@ -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)
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment