[commit: ghc] wip/T15050: Update Note [Pattern signature binders] (1aef2b9)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T15050
Link       : http://ghc.haskell.org/trac/ghc/changeset/1aef2b9682bf4e10016aacd05a71b0761e5a7b01/ghc

>---------------------------------------------------------------

commit 1aef2b9682bf4e10016aacd05a71b0761e5a7b01
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Sat Aug 4 12:48:37 2018 -0400

    Update Note [Pattern signature binders]


>---------------------------------------------------------------

1aef2b9682bf4e10016aacd05a71b0761e5a7b01
 compiler/typecheck/TcHsType.hs | 24 +++---------------------
 1 file changed, 3 insertions(+), 21 deletions(-)

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 4855d61..d50c570 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2423,7 +2423,6 @@ tcHsPatSigType ctxt sig_ty
                RuleSigCtxt {} -> newSkolemTyVar
                _              -> newTauTyVar
       -- See Note [Pattern signature binders]
-      -- See Note [Unifying SigTvs]
 
     mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
                        ; return (tyVarName tv, tv') }
@@ -2509,10 +2508,10 @@ Here
    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
+   (a TauTv), and binds "b" :-> b_sig in the envt
 
  * Then unification makes b_sig := a_sk
-   That's why we must make b_sig a MetaTv (albeit a SigTv),
+   That's why we must make b_sig a MetaTv,
    not a SkolemTv, so that it can unify to a_sk.
 
  * Finally, in 'blah' we must have the envt "b" :-> a_sk.  The pair
@@ -2526,7 +2525,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 +2537,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.
 
 
 ************************************************************************