Allow scoped type variables refer to types

This patch implements GHC proposal 29:
(sorry, URL is too long for the commit message linter)
and fixess #15050.

The change is simple: Just use a different meta variable form.

Test suite and documentation updated.

Differential Revision: https://phabricator.haskell.org/D4980

compiler/typecheck/TcHsType.hs

@@ -1572,7 +1572,7 @@ kcLHsQTyVars name flav cusk
   | otherwise
   = do { (scoped_kvs, (tc_tvs, res_kind))
            -- Why kcImplicitTKBndrs which uses newSigTyVar?
-           -- See Note [Kind generalisation and sigTvs]
+           -- See Note [Kind generalisation and SigTvs]
            <- kcImplicitTKBndrs kv_ns $
               kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
 
@@ -2421,9 +2421,8 @@ tcHsPatSigType ctxt sig_ty
 
     new_tv = case ctxt of
                RuleSigCtxt {} -> newSkolemTyVar
-               _              -> newSigTyVar
+               _              -> newTauTyVar
       -- See Note [Pattern signature binders]
-      -- See Note [Unifying SigTvs]
 
     mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
                        ; return (tyVarName tv, tv') }
@@ -2500,24 +2499,31 @@ patBindSigErr sig_tvs
 {- Note [Pattern signature binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
-   data T = forall a. T a (a->Int)
-   f (T x (f :: b->Int)) = blah
+
+  data T where
+    MkT :: forall a. a -> (a -> Int) -> T
+
+  f :: T -> ...
+  f (MkT x (f :: b -> c)) = ...
 
 Here
- * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk',
+ * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk',
    It must be a skolem so that that it retains its identity, and
    TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
 
- * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig
-   (a SigTv), and binds "b" :-> b_sig in the envt
+ * The type signature pattern (f :: b -> c) makes freshs meta-tyvars
+   beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
+   environment
 
- * Then unification makes b_sig := a_sk
-   That's why we must make b_sig a MetaTv (albeit a SigTv),
-   not a SkolemTv, so that it can unify to a_sk.
+ * 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)
 
- * Finally, in 'blah' we must have the envt "b" :-> a_sk.  The pair
-   ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by
-   mk_tv_pair in that function.
+ * 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.
 
 Another example (Trac #13881):
    fl :: forall (l :: [a]). Sing l -> Sing l
@@ -2526,7 +2532,7 @@ When we reach the pattern signature, 'l' is in scope from the
 outer 'forall':
    "a" :-> a_sk :: *
    "l" :-> l_sk :: [a_sk]
-We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check
+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
@@ -2538,23 +2544,6 @@ 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.
 
-Note [Unifying SigTvs]
-~~~~~~~~~~~~~~~~~~~~~~
-ALAS we have no decent way of avoiding two SigTvs getting unified.
-Consider
-  f (x::(a,b)) (y::c)) = [fst x, y]
-Here we'd really like to complain that 'a' and 'c' are unified. But
-for the reasons above we can't make a,b,c into skolems, so they
-are just SigTvs that can unify.  And indeed, this would be ok,
-  f x (y::c) = case x of
-                 (x1 :: a1, True) -> [x,y]
-                 (x1 :: a2, False) -> [x,y,y]
-Here the type of x's first component is called 'a1' in one branch and
-'a2' in the other.  We could try insisting on the same OccName, but
-they definitely won't have the sane lexical Name.
-
-I think we could solve this by recording in a SigTv a list of all the
-in-scope variables that it should not unify with, but it's fiddly.
 
 
 ************************************************************************

compiler/typecheck/TcMType.hs

@@ -51,7 +51,7 @@ module TcMType (
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   newMetaSigTyVars, newMetaSigTyVarX,
-  newSigTyVar, newSkolemTyVar, newWildCardX,
+  newSigTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
   tcInstSkolTyVars,tcInstSkolTyVarsX,
   tcInstSuperSkolTyVarsX,
@@ -620,13 +620,28 @@ instead of the buggous
 ************************************************************************
 -}
 
--- a SigTv can unify with type *variables* only, including other SigTvs
--- and skolems. Sometimes, they can unify with type variables that the
--- user would rather keep distinct; see #11203 for an example.
--- So, any client of this
--- function needs to either allow the SigTvs to unify with each other
+{-
+Note [SigTv]
+~~~~~~~~~~~~
+
+A SigTv can unify with type *variables* only, including other SigTvs and
+skolems. Sometimes, they can unify with type variables that the user would
+rather keep distinct; see #11203 for an example.  So, any client of this
+function needs to either allow the SigTvs to unify with each other or check
+that they don't (say, with a call to findDubSigTvs).
+
+Before #15050 this was used for ScopedTypeVariables in patterns, to make sure
+these type variables only refer to other type variables, but this restriction
+was dropped, and ScopedTypeVariables can now refer to full types (GHC Proposal
+29).
+
+The remaining uses of newSigTyVars are
+* in kind signatures, see Note [Kind generalisation and SigTvs]
+  and Note [Use SigTvs in kind-checking pass]
+* in partial type signatures, see Note [Quantified variables in partial type signatures]
+-}
+
+-- see Note [SigTv]
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
   = do { details <- newMetaDetails SigTv
@@ -634,6 +649,7 @@ newSigTyVar name kind
        ; traceTc "newSigTyVar" (ppr tyvar)
        ; return tyvar }
 
+
 -- makes a new skolem tv
 newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
 newSkolemTyVar name kind = do { lvl <- getTcLevel
@@ -807,6 +823,14 @@ coercion variables, except for the special case of the promoted Eq#. But,
 that can't ever appear in user code, so we're safe!
 -}
 
+newTauTyVar :: Name -> Kind -> TcM TcTyVar
+newTauTyVar name kind
+  = do { details <- newMetaDetails TauTv
+       ; let tyvar = mkTcTyVar name kind details
+       ; traceTc "newTauTyVar" (ppr tyvar)
+       ; return tyvar }
+
+
 mkMetaTyVarName :: Unique -> FastString -> Name
 -- Makes a /System/ Name, which is eagerly eliminated by
 -- the unifier; see TcUnify.nicer_to_update_tv1, and

docs/users_guide/glasgow_exts.rst

@@ -10430,11 +10430,6 @@ scope, because it is bound by the pattern match.
 The effect is to bring it into scope,
 standing for the existentially-bound type variable.
 
-When a pattern type signature binds a type variable in this way, GHC
-insists that the type variable is bound to a *rigid*, or fully-known,
-type variable. This means that any user-written type signature always
-stands for a completely known type.
-
 It does seem odd that the existentially-bound type variable *must not*
 be already in scope. Contrast that usually name-bindings merely shadow
 (make a 'hole') in a same-named outer variable's scope.

testsuite/tests/indexed-types/should_compile/all.T

@@ -280,6 +280,7 @@ test('T14237', normal, compile, [''])
 test('T14554', normal, compile, [''])
 test('T14680', normal, compile, [''])
 test('T15057', normal, compile, [''])
+test('T7786', normal, compile, [''])
 test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
@@ -289,4 +290,3 @@ test('T15322', normal, compile, [''])
 test('T15322a', normal, compile_fail, [''])
 test('T15142', normal, compile, [''])
 test('T15352', normal, compile, [''])
-

testsuite/tests/indexed-types/should_fail/T7786.stderr

-
-T7786.hs:96:41: error:
-    • Couldn't match type ‘xxx’
-                     with ‘Intersect (BuriedUnder sub k 'Empty) inv’
-      Expected type: Maybe (Sing xxx)
-        Actual type: Maybe
-                       (Sing (Intersect (BuriedUnder sub k 'Empty) inv))
-    • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub
-      In the expression:
-        do Nil :: Sing xxx <- foogle db k sub
-           return $ Sub db k sub
-      In an equation for ‘addSub’:
-          addSub db k sub
-            = do Nil :: Sing xxx <- foogle db k sub
-                 return $ Sub db k sub
-    • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:96:13)
-        k :: Sing k (bound at T7786.hs:96:11)
-        db :: Database inv (bound at T7786.hs:96:8)
-        addSub :: Database inv
-                  -> Sing k
-                  -> Database sub
-                  -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:96:1)
-
-T7786.hs:97:31: error:
-    • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv
-                        ~ 'Empty
-        arising from a use of ‘Sub’
-      from the context: xxx ~ 'Empty
-        bound by a pattern with constructor: Nil :: forall a. Sing 'Empty,
-                 in a pattern binding in
-                      a 'do' block
-        at T7786.hs:96:22-24
-    • In the second argument of ‘($)’, namely ‘Sub db k sub’
-      In a stmt of a 'do' block: return $ Sub db k sub
-      In the expression:
-        do Nil :: Sing xxx <- foogle db k sub
-           return $ Sub db k sub
-    • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:96:13)
-        k :: Sing k (bound at T7786.hs:96:11)
-        db :: Database inv (bound at T7786.hs:96:8)
-        addSub :: Database inv
-                  -> Sing k
-                  -> Database sub
-                  -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:96:1)

testsuite/tests/indexed-types/should_fail/all.T

@@ -87,7 +87,6 @@ test('T7536', normal, compile_fail, [''])
 
 test('T7729', normal, compile_fail, [''])
 test('T7729a', normal, compile_fail, [''])
-test('T7786', normal, compile_fail, [''])
 
 test('NoGood', normal, compile_fail, [''])
 test('T7967', normal, compile_fail, [''])

testsuite/tests/typecheck/should_compile/all.T

@@ -620,7 +620,7 @@ test('SplitWD', normal, compile, [''])
 #       (2) Build the program twice: once with -dynamic, and then
 #           with -prof using -osuf to set a different object file suffix.
 test('T14441', omit_ways(['profasm']), compile, [''])
-test('T15050', [expect_broken(15050)], compile, [''])
+test('T15050', normal, compile, [''])
 test('T14735', normal, compile, [''])
 test('T15180', normal, compile, [''])
 test('T15232', normal, compile, [''])

testsuite/tests/typecheck/should_compile/tc141.stderr

@@ -37,13 +37,13 @@ tc141.hs:13:13: error:
         in v
 
 tc141.hs:15:18: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘p’
-      ‘a2’ is a rigid type variable bound by
+    • Couldn't match expected type ‘a1’ with actual type ‘p1’
+      ‘a1’ is a rigid type variable bound by
         the type signature for:
-          v :: forall a2. a2
+          v :: forall a1. a1
         at tc141.hs:14:14-19
-      ‘p’ is a rigid type variable bound by
-        the inferred type of g :: a -> p -> a1
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of g :: p -> p1 -> a
         at tc141.hs:(13,1)-(16,13)
     • In the expression: b
       In an equation for ‘v’: v = b
@@ -53,6 +53,6 @@ tc141.hs:15:18: error:
           v = b
         in v
     • Relevant bindings include
-        v :: a2 (bound at tc141.hs:15:14)
-        b :: p (bound at tc141.hs:13:5)
-        g :: a -> p -> a1 (bound at tc141.hs:13:1)
+        v :: a1 (bound at tc141.hs:15:14)
+        b :: p1 (bound at tc141.hs:13:5)
+        g :: p -> p1 -> a (bound at tc141.hs:13:1)

testsuite/tests/typecheck/should_fail/T5689.stderr

 
-T5689.hs:10:36: error:
-    • Couldn't match expected type ‘Bool’ with actual type ‘t’
-    • In the expression: v
-      In the expression: if v then False else True
-      In the second argument of ‘writeIORef’, namely
-        ‘(\ v -> if v then False else True)’
-    • Relevant bindings include
-        v :: t (bound at T5689.hs:10:28)
-        r :: IORef (t -> t) (bound at T5689.hs:7:14)
+T5689.hs:15:23: error:
+    • No instance for (Num Bool) arising from the literal ‘1234’
+    • In the first argument of ‘c’, namely ‘1234’
+      In the second argument of ‘($)’, namely ‘c 1234’
+      In a stmt of a 'do' block: print $ c 1234

testsuite/tests/typecheck/should_fail/T5691.stderr

 
-T5691.hs:14:9: error:
-    • Couldn't match type ‘p’ with ‘PrintRuleInterp’
-      Expected type: PrintRuleInterp a
-        Actual type: p a
-    • When checking that the pattern signature: p a
-        fits the type of its context: PrintRuleInterp a
-      In the pattern: f :: p a
-      In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
-
 T5691.hs:24:10: error:
     • No instance for (Alternative RecDecParser)
         arising from the superclasses of an instance declaration