[commit: ghc] master: Remove a zonkTcTyVarToTyVar (29978ef)
git at git.haskell.org
git at git.haskell.org
Thu Oct 25 08:10:27 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/29978ef1f834d77dc31bf7054590d526d068df7e/ghc
>---------------------------------------------------------------
commit 29978ef1f834d77dc31bf7054590d526d068df7e
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Thu Oct 25 08:50:59 2018 +0100
Remove a zonkTcTyVarToTyVar
This patch fixes Trac #15778 by removing a zonkTcTyVarToTyVar
from tcHsSigType.
Nww that a pattern-bound type variable can refer to a type, it's
obvoiusly wrong to expect it to be a TyVar! Moreover, that zonk
is entirely unnecessary.
I added a new Note [Type variables in the type environment]
in TcRnTypes
>---------------------------------------------------------------
29978ef1f834d77dc31bf7054590d526d068df7e
compiler/typecheck/TcHsType.hs | 32 ++++++---------
compiler/typecheck/TcRnTypes.hs | 47 ++++++++++++++++++++--
testsuite/tests/typecheck/should_compile/T15778.hs | 6 +++
testsuite/tests/typecheck/should_compile/all.T | 1 +
4 files changed, 62 insertions(+), 24 deletions(-)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 4b755e4..24299dd 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2475,7 +2475,7 @@ tcHsPatSigType ctxt sig_ty
; sig_ty <- zonkPromoteType sig_ty
; checkValidType ctxt sig_ty
- ; tv_pairs <- mapM mk_tv_pair sig_tkvs
+ ; let tv_pairs = mkTyVarNamePairs sig_tkvs
; traceTc "tcHsPatSigType" (ppr sig_vars)
; return (wcs, tv_pairs, sig_ty) }
@@ -2488,14 +2488,9 @@ tcHsPatSigType ctxt sig_ty
_ -> newTauTyVar
-- See Note [Pattern signature binders]
- mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
- ; return (tyVarName tv, tv') }
- -- The Name is one of sig_vars, the lexically scoped name
- -- But if it's a TyVarTv, it might have been unified
- -- with an existing in-scope skolem, so we must zonk
- -- here. See Note [Pattern signature binders]
+
tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
-tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
+tcHsPatSigType _ (XHsWildCardBndrs _) = panic "tcHsPatSigType"
tcPatSig :: Bool -- True <=> pattern binding
-> LHsSigWcType GhcRn
@@ -2532,8 +2527,8 @@ tcPatSig in_pat_bind sig res_ty
-- f :: Int -> Int
-- f (x :: T a) = ...
-- Here 'a' doesn't get a binding. Sigh
- ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
- , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
+ ; let bad_tvs = filterOut (`elemVarSet` exactTyCoVarsOfType sig_ty)
+ (tyCoVarsOfTypeList sig_ty)
; checkTc (null bad_tvs) (badPatTyVarTvs sig_ty bad_tvs)
-- Now do a subsumption check of the pattern signature against res_ty
@@ -2562,13 +2557,14 @@ patBindSigErr sig_tvs
{- Note [Pattern signature binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Type variables in the type environment] in TcRnTypes.
Consider
data T where
MkT :: forall a. a -> (a -> Int) -> T
f :: T -> ...
- f (MkT x (f :: b -> c)) = ...
+ f (MkT x (f :: b -> c)) = <blah>
Here
* The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
@@ -2581,13 +2577,10 @@ Here
* Then unification makes beta := a_sk, gamma := Int
That's why we must make beta and gamma a MetaTv,
- not a SkolemTv, so that it can unify to a_sk rsp. Int.
- Note that gamma unifies with a type, not just a type variable
- (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst)
+ not a SkolemTv, so that it can unify to a_sk (or Int, respectively).
- * Finally, in 'blah' we must have the envt "b" :-> a_sk, "c" :-> Int.
- The pairs ("b" :-> a_sk, "c" :-> Int) are returned by tcHsPatSigType,
- constructed by mk_tv_pair in that function.
+ * Finally, in '<blah>' we have the envt "b" :-> beta, "c" :-> gamma,
+ so we return the pairs ("b" :-> beta, "c" :-> gamma) from tcHsPatSigType,
Another example (Trac #13881):
fl :: forall (l :: [a]). Sing l -> Sing l
@@ -2600,14 +2593,13 @@ We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check
the pattern signature
Sing (l :: [y])
That unifies y_sig := a_sk. We return from tcHsPatSigType with
-the pair ("y" :-> a_sk).
+the pair ("y" :-> y_sig).
For RULE binders, though, things are a bit different (yuk).
RULE "foo" forall (x::a) (y::[a]). f x y = ...
Here this really is the binding site of the type variable so we'd like
to use a skolem, so that we get a complaint if we unify two of them
-together.
-
+together. Hence the new_tv function in tcHsPatSigType.
************************************************************************
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 131e57b..a411975 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1081,10 +1081,7 @@ data TcTyThing
, tct_info :: IdBindingInfo -- See Note [Meaning of IdBindingInfo]
}
- | ATyVar Name TcTyVar -- The type variable to which the lexically scoped type
- -- variable is bound. We only need the Name
- -- for error-message purposes; it is the corresponding
- -- Name in the domain of the envt
+ | ATyVar Name TcTyVar -- See Note [Type variables in the type environment]
| ATcTyCon TyCon -- Used temporarily, during kind checking, for the
-- tycons and clases in this recursive group
@@ -1251,6 +1248,48 @@ variables have ClosedTypeId=True (or imported). This is an extension
compared to the JFP paper on OutsideIn, which used "top-level" as a
proxy for "closed". (It's not a good proxy anyway -- the MR can make
a top-level binding with a free type variable.)
+
+Note [Type variables in the type environment]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type environment has a binding for each lexically-scoped
+type variable that is in scope. For example
+
+ f :: forall a. a -> a
+ f x = (x :: a)
+
+ g1 :: [a] -> a
+ g1 (ys :: [b]) = head ys :: b
+
+ g2 :: [Int] -> Int
+ g2 (ys :: [c]) = head ys :: c
+
+* The forall'd variable 'a' in the signature scopes over f's RHS.
+
+* The pattern-bound type variable 'b' in 'g1' scopes over g1's
+ RHS; note that it is bound to a skolem 'a' which is not itself
+ lexically in scope.
+
+* The pattern-bound type variable 'c' in 'g2' is bound to
+ Int; that is, pattern-bound type variables can stand for
+ arbitrary types. (see
+ GHC proposal #128 "Allow ScopedTypeVariables to refer to types"
+ https://github.com/ghc-proposals/ghc-proposals/pull/128,
+ and the paper
+ "Type variables in patterns", Haskell Symposium 2018.
+
+
+This is implemented by the constructor
+ ATyVar Name TcTyVar
+in the type environment.
+
+* The Name is the name of the original, lexically scoped type
+ variable
+
+* The TcTyVar is sometimes a skolem (like in 'f'), and sometimes
+ a unification variable (like in 'g1', 'g2'). We never zonk the
+ type environment so in the latter case it always stays as a
+ unification variable, although that variable may be later
+ unified with a type (such as Int in 'g2').
-}
instance Outputable IdBindingInfo where
diff --git a/testsuite/tests/typecheck/should_compile/T15778.hs b/testsuite/tests/typecheck/should_compile/T15778.hs
new file mode 100644
index 0000000..4c95d37
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15778.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+
+module T15778 where
+
+f (x :: (Int :: a)) = True :: (Bool :: a)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b9cb68e..36cc4b4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -651,3 +651,4 @@ test('T15473', normal, compile_fail, [''])
test('T15499', normal, compile, [''])
test('T15586', normal, compile, [''])
test('T15368', normal, compile, ['-fdefer-type-errors'])
+test('T15778', normal, compile, [''])
More information about the ghc-commits
mailing list