Remove a zonkTcTyVarToTyVar
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 25 Oct 2018 07:50:59 +0000 (08:50 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 25 Oct 2018 08:10:00 +0000 (09:10 +0100)
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

compiler/typecheck/TcHsType.hs
compiler/typecheck/TcRnTypes.hs
testsuite/tests/typecheck/should_compile/T15778.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 4b755e4..24299dd 100644 (file)
@@ -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.
 
 
 ************************************************************************
index 131e57b..a411975 100644 (file)
@@ -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 (file)
index 0000000..4c95d37
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+
+module T15778 where
+
+f (x :: (Int :: a)) = True :: (Bool :: a)
index b9cb68e..36cc4b4 100644 (file)
@@ -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, [''])