Improve skolemisation

This patch avoids skolemiseUnboundMetaTyVar making
up a fresh Name when it doesn't need to.

See Note [Skolemising and identity]

Improves error messsages for partial type signatures.

18 files changed, 55 insertions, 34 deletions

diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index ef75635..8a50e66 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1753,16 +1753,17 @@ skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
 skolemiseUnboundMetaTyVar tv
   = ASSERT2( isMetaTyVar tv, ppr tv )
     do  { when debugIsOn (check_empty tv)
-        ; span <- getSrcSpanM    -- Get the location from "here"
+        ; here <- getSrcSpanM    -- Get the location from "here"
                                  -- ie where we are generalising
         ; kind <- zonkTcType (tyVarKind tv)
-        ; let uniq        = getUnique tv
-                -- NB: Use same Unique as original tyvar. This is
-                -- convenient in reading dumps, but is otherwise inessential.
-
-              tv_name     = getOccName tv
-              final_name  = mkInternalName uniq tv_name span
-              final_tv    = mkTcTyVar final_name kind details
+        ; let tv_name     = tyVarName tv
+              -- See Note [Skolemising and identity]
+              final_name | isSystemName tv_name
+                         = mkInternalName (nameUnique tv_name)
+                                          (nameOccName tv_name) here
+                         | otherwise
+                         = tv_name
+              final_tv = mkTcTyVar final_name kind details
 
         ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
@@ -1875,9 +1876,29 @@ 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 require for a quantified variable), but is still a TcTyVar that the
-simplifier knows how to deal with.
+We can avoid this problem by zonking with a skolem TcTyVar.  The
+skolem is rigid (which we require for a quantified variable), but is
+still a TcTyVar that the simplifier knows how to deal with.
+
+Note [Skolemising and identity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some places, we make a TyVarTv for a binder. E.g.
+    class C a where ...
+As Note [Inferring kinds for type declarations] discusses,
+we make a TyVarTv for 'a'.  Later we skolemise it, and we'd
+like to retain its identity, location info etc.  (If we don't
+retain its identity we'll have to do some pointless swizzling;
+see TcTyClsDecls.swizzleTcTyConBndrs.  If we retain its identity
+but not its location we'll lose the detailed binding site info.
+
+Conclusion: use the Name of the TyVarTv.  But we don't want
+to do that when skolemising random unification variables;
+there the location we want is the skolemisation site.
+
+Fortunately we can tell the difference: random unification
+variables have System Names.  That's why final_name is
+set based on the isSystemName test.
+
 
 Note [Silly Type Synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
index ea7e3d5..6e23ec6 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExprSigLocal.stderr
@@ -3,7 +3,7 @@ ExprSigLocal.hs:9:35: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of <expression> :: a -> a
-               at ExprSigLocal.hs:9:20-35
+               at ExprSigLocal.hs:9:27
     • In the type ‘a -> _’
       In an expression type signature: forall a. a -> _
       In the expression: (\ x -> x) :: forall a. a -> _
@@ -14,6 +14,6 @@ ExprSigLocal.hs:11:21: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of g :: a -> a
-               at ExprSigLocal.hs:12:1-7
+               at ExprSigLocal.hs:11:13
     • In the type ‘a -> _’
       In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
index ad78bc9..c12cf30 100644
--- a/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SplicesUsed.stderr
@@ -29,7 +29,7 @@ SplicesUsed.hs:10:16: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(Char, a)’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of charA :: a -> (Char, a)
-               at SplicesUsed.hs:11:1-18
+               at SplicesUsed.hs:10:1-26
     • In the type ‘a -> (_)’
       In the type signature: charA :: a -> (_)
 
diff --git a/testsuite/tests/partial-sigs/should_compile/T10519.stderr b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
index f57144d..13f1104 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10519.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10519.stderr
@@ -3,5 +3,5 @@ T10519.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Eq a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of foo :: Eq a => a -> a -> Bool
-               at T10519.hs:6:1-16
+               at T10519.hs:5:15
     • In the type signature: foo :: forall a. _ => a -> a -> Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T12844.stderr b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
index 0e01cd3..3d80311 100644
--- a/testsuite/tests/partial-sigs/should_compile/T12844.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T12844.stderr
@@ -6,5 +6,5 @@ T12844.hs:12:9: warning: [-Wpartial-type-signatures (in -Wdefault)]
                are rigid type variables bound by
                the inferred type of
                  bar :: (Foo rngs, Head rngs ~ '(r, r')) => FooData rngs
-               at T12844.hs:13:1-9
+               at T12844.hs:(12,1)-(13,9)
     • In the type signature: bar :: _ => FooData rngs
diff --git a/testsuite/tests/partial-sigs/should_compile/T13482.stderr b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
index a21b7dc..dc2b156 100644
--- a/testsuite/tests/partial-sigs/should_compile/T13482.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T13482.stderr
@@ -4,7 +4,7 @@ T13482.hs:10:32: warning: [-Wpartial-type-signatures (in -Wdefault)]
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of
                  minimal1_noksig :: (Eq m, Monoid m) => Int -> Bool
-               at T13482.hs:11:1-50
+               at T13482.hs:10:27
     • In the type signature:
         minimal1_noksig :: forall m. _ => Int -> Bool
 
@@ -12,20 +12,20 @@ T13482.hs:13:33: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘(Eq m, Monoid m)’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal1 :: (Eq m, Monoid m) => Bool
-               at T13482.hs:14:1-41
+               at T13482.hs:13:21
     • In the type signature: minimal1 :: forall (m :: Type). _ => Bool
 
 T13482.hs:16:30: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Monoid m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal2 :: (Eq m, Monoid m) => Bool
-               at T13482.hs:17:1-41
+               at T13482.hs:16:20
     • In the type signature: minimal2 :: forall m. (Eq m, _) => Bool
 
 T13482.hs:19:34: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Eq m’
       Where: ‘m’ is a rigid type variable bound by
                the inferred type of minimal3 :: (Monoid m, Eq m) => Bool
-               at T13482.hs:20:1-41
+               at T13482.hs:19:20
     • In the type signature:
         minimal3 :: forall m. (Monoid m, _) => Bool
diff --git a/testsuite/tests/partial-sigs/should_compile/T14217.stderr b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
index ebecbb9..97f7854 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14217.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14217.stderr
@@ -91,7 +91,7 @@ T14217.hs:32:11: error:
                             a62
                             a63
                           -> Bool
-               at T14217.hs:41:1-14
+               at T14217.hs:(32,1)-(40,13)
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         eqFoo :: _ =>
diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
index 4e69a4c..901ece0 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
@@ -5,7 +5,7 @@ T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)]
                the inferred type of
                  bench_mulPublic :: (z ~ LiftOf zq, Reduce (LiftOf zq) zq) =>
                                     Cyc zp -> Cyc z -> IO (zp, zq)
-               at T14715.hs:(14,1)-(16,14)
+               at T14715.hs:13:32-33
     • In the type signature:
         bench_mulPublic :: forall z zp zq.
                            (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp, zq)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
index d07ce73..e52d911 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
@@ -51,6 +51,6 @@ T15039a.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Coercible a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible a b => Coercion a b
-               at T15039a.hs:36:1-14
+               at T15039a.hs:35:1-44
     • In the type signature:
         ex7 :: _ => Coercion (a :: Type) (b :: Type)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
index 949995d..da14f26 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
@@ -52,6 +52,6 @@ T15039b.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Coercible @(*) a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible @(*) a b => Coercion @{*} a b
-               at T15039b.hs:36:1-14
+               at T15039b.hs:35:1-44
     • In the type signature:
         ex7 :: _ => Coercion (a :: Type) (b :: Type)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
index 261a82e..c7ad5e8 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
@@ -51,6 +51,6 @@ T15039c.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Coercible a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible a b => Coercion a b
-               at T15039c.hs:36:1-14
+               at T15039c.hs:35:1-44
     • In the type signature:
         ex7 :: _ => Coercion (a :: Type) (b :: Type)
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
index 6e26d5a..68882c3 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
@@ -53,6 +53,6 @@ T15039d.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Coercible @(*) a b’
       Where: ‘a’, ‘b’ are rigid type variables bound by
                the inferred type of ex7 :: Coercible @(*) a b => Coercion @{*} a b
-               at T15039d.hs:36:1-14
+               at T15039d.hs:35:1-44
     • In the type signature:
         ex7 :: _ => Coercion (a :: Type) (b :: Type)
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.stderr b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
index 6efdae3..ebd0164 100644
--- a/testsuite/tests/partial-sigs/should_compile/T16728.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
@@ -3,7 +3,7 @@ T16728.hs:8:37: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘k’
       Where: ‘k’ is a rigid type variable bound by
                the inferred type of f :: Proxy x
-               at T16728.hs:9:1-9
+               at T16728.hs:8:13
     • In the kind ‘_’
       In the first argument of ‘Proxy’, namely ‘(x :: _)’
       In the type ‘Proxy (x :: _)’
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
index 712acfe..9948e78 100644
--- a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
@@ -8,6 +8,6 @@ T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of g :: a -> a
-               at T16728b.hs:6:1-7
+               at T16728b.hs:4:14
     • In the type ‘a -> _’
       In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
index e6c2780..3fc90ec 100644
--- a/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ExtraConstraintsWildcardNotEnabled.stderr
@@ -3,6 +3,6 @@ ExtraConstraintsWildcardNotEnabled.hs:4:10: error:
     • Found type wildcard ‘_’ standing for ‘Show a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of show' :: Show a => a -> String
-               at ExtraConstraintsWildcardNotEnabled.hs:5:1-16
+               at ExtraConstraintsWildcardNotEnabled.hs:4:1-25
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: show' :: _ => a -> String
diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
index 69207b1..8366318 100644
--- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
@@ -3,7 +3,7 @@ InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
     • Found type wildcard ‘_a’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
-               at InstantiatedNamedWildcardsInConstraints.hs:5:1-26
+               at InstantiatedNamedWildcardsInConstraints.hs:4:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (Enum _a, _) => _a -> (String, b)
 
@@ -11,6 +11,6 @@ InstantiatedNamedWildcardsInConstraints.hs:4:18: error:
     • Found type wildcard ‘_’ standing for ‘Show b’
       Where: ‘b’ is a rigid type variable bound by
                the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
-               at InstantiatedNamedWildcardsInConstraints.hs:5:1-26
+               at InstantiatedNamedWildcardsInConstraints.hs:4:1-40
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: foo :: (Enum _a, _) => _a -> (String, b)
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
index 2bae8ab..4c22dc6 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
@@ -26,7 +26,7 @@ NamedWildcardExplicitForall.hs:14:16: error:
     • Couldn't match expected type ‘Bool’ with actual type ‘_a’
       ‘_a’ is a rigid type variable bound by
         the inferred type of baz :: _a -> Bool -> (_a, Bool)
-        at NamedWildcardExplicitForall.hs:14:1-24
+        at NamedWildcardExplicitForall.hs:13:15-16
     • In the first argument of ‘not’, namely ‘x’
       In the expression: not x
       In the expression: (not x, not y)
diff --git a/testsuite/tests/partial-sigs/should_fail/T10615.stderr b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
index f95df86..b474e3d 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10615.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
@@ -10,7 +10,7 @@ T10615.hs:5:6: error:
     • Couldn't match type ‘f’ with ‘b1 -> a1’
       ‘f’ is a rigid type variable bound by
         the inferred type of f1 :: a1 -> f
-        at T10615.hs:5:1-10
+        at T10615.hs:4:1-12
       Expected type: a1 -> f
         Actual type: a1 -> b1 -> a1
     • In the expression: const
@@ -28,7 +28,7 @@ T10615.hs:8:6: error:
     • Couldn't match type ‘_f’ with ‘b0 -> a0’
       ‘_f’ is a rigid type variable bound by
         the inferred type of f2 :: a0 -> _f
-        at T10615.hs:8:1-10
+        at T10615.hs:7:1-13
       Expected type: a0 -> _f
         Actual type: a0 -> b0 -> a0
     • In the expression: const