Typechecker comments and debug tracing only

4 files changed, 19 insertions, 11 deletions

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 933bacc4cc..8b3aaa9ebb 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -722,7 +722,7 @@ yields a better error message anyway.)
 flatten :: FlattenMode -> CtEvidence -> TcType
         -> TcS (Xi, TcCoercion)
 flatten mode ev ty
-  = do { traceTcS "flatten {" (ppr ty)
+  = do { traceTcS "flatten {" (ppr mode <+> ppr ty)
        ; (ty', co) <- runFlatten mode ev (flatten_one ty)
        ; traceTcS "flatten }" (ppr ty')
        ; return (ty', co) }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index decb6cb18a..1f183ed698 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1026,7 +1026,9 @@ zonkQuantifiedTyVar default_kind tv
       = do { tv' <- skolemiseUnboundMetaTyVar tv
            ; return (Just tv') }
       where
-        -- do not default SigTvs. This would violate the invariants on SigTvs
+        -- Do not default SigTvs. Doing so would violate the invariants
+        -- on SigTvs; see Note [Signature skolems] in TcType.
+        -- Trac #13343 is an example
         not_sig_tv = case info of SigTv -> False
                                   _     -> True
 
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 6a4a989fe9..e5708b612e 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -439,15 +439,23 @@ why Var.hs shouldn't actually have the definition, but it "belongs" here.
 
 Note [Signature skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
+A SigTv is a specialised variant of TauTv, with the following invarints:
+
+    * A SigTv can be unified only with a TyVar,
+      not with any other type
+
+    * Its MetaDetails, if filled in, will always be another SigTv
+      or a SkolemTv
+
+SigTvs are only distinguished to improve error messages.
 Consider this
 
   f :: forall a. [a] -> Int
   f (x::b : xs) = 3
 
 Here 'b' is a lexically scoped type variable, but it turns out to be
-the same as the skolem 'a'.  So we have a special kind of skolem
-constant, SigTv, which can unify with other SigTvs. They are used
-*only* for pattern type signatures.
+the same as the skolem 'a'.  So we make them both SigTvs, which can unify
+with each other.
 
 Similarly consider
   data T (a:k1) = MkT (S a)
@@ -455,6 +463,8 @@ Similarly consider
 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
 because they end up unifying; we want those SigTvs again.
 
+SigTvs are used *only* for pattern type signatures.
+
 Note [TyVars and TcTyVars during type checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The Var type has constructors TyVar and TcTyVar.  They are used
@@ -514,10 +524,7 @@ data MetaInfo
 
    | SigTv         -- A variant of TauTv, except that it should not be
                    -- unified with a type, only with a type variable
-                   -- SigTvs are only distinguished to improve error messages
-                   --      see Note [Signature skolems]
-                   --      The MetaDetails, if filled in, will
-                   --      always be another SigTv or a SkolemTv
+                   -- See Note [Signature skolems]
 
    | FlatMetaTv    -- A flatten meta-tyvar
                    -- It is a meta-tyvar, but it is always untouchable, with level 0
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index acfb0b7a0c..ef0c95ab7a 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1908,8 +1908,7 @@ metaTyVarUpdateOK :: DynFlags
                   -> TcType              -- ty :: k2
                   -> Maybe TcType        -- possibly-expanded ty
 -- (metaTyFVarUpdateOK tv ty)
--- We are about to update the meta-tyvar tv with ty, in
--- our on-the-flyh unifier
+-- We are about to update the meta-tyvar tv with ty
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
 --           (in the impredicative case), or type functions