Wibble to Taming the Kind Inference Monster

I had allowed rename/should_fail/T15828 (Trac #15828) to regress a bit.
The main payload of this patch is to fix that problem, at the cost of
more contortions in checkConsistentFamInst.  Oh well, at least they are
highly localised.

I also update the -ddump-types code in TcRnDriver to print out some
more expicit information about each type constructor, thus instead of

   DF{3} :: forall k. * -> k -> *

we get

   data family DF{3} :: forall k. * -> k -> *

Remember, this is debug-printing only.  This change is the reason
that so many .stderr files change.

6 files changed, 86 insertions, 34 deletions

diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs
index 1b6ab12d0f..516b89849f 100644
--- a/compiler/typecheck/ClsInst.hs
+++ b/compiler/typecheck/ClsInst.hs
@@ -55,6 +55,8 @@ data AssocInstInfo
   = NotAssociated
   | InClsInst { ai_class    :: Class
               , ai_tyvars   :: [TyVar]      -- ^ The /scoped/ tyvars of the instance
+                                            -- Why scoped?  See bind_me in
+                                            -- TcValidity.checkConsistentFamInst
               , ai_inst_env :: VarEnv Type  -- ^ Maps /class/ tyvars to their instance types
                 -- See Note [Matching in the consistent-instantation check]
     }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 8d2ef94453..e2150e7b8b 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -484,7 +484,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
                            fst $ splitForAllVarBndrs dfun_ty
               visible_skol_tvs = drop n_inferred skol_tvs
 
-        ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs $$ ppr visible_skol_tvs)
+        ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs)
 
         -- Next, process any associated types.
         ; (datafam_stuff, tyfam_insts)
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index b13ae21b20..3b12837bdc 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2745,11 +2745,12 @@ ppr_tycons debug fam_insts type_env
                      | otherwise  = isExternalName (tyConName tycon) &&
                                     not (tycon `elem` fi_tycons)
     ppr_tc tc
-       = vcat [ ppWhen show_roles $
-                hang (text "type role" <+> ppr tc)
-                   2 (hsep (map ppr roles))
-              , hang (ppr tc <> braces (ppr (tyConArity tc)) <+> dcolon)
-                   2 (ppr (tidyTopType (tyConKind tc))) ]
+       = vcat [ hang (ppr (tyConFlavour tc) <+> ppr tc
+                      <> braces (ppr (tyConArity tc)) <+> dcolon)
+                   2 (ppr (tidyTopType (tyConKind tc)))
+              , nest 2 $
+                ppWhen show_roles $
+                text "roles" <+> (sep (map ppr roles)) ]
        where
          show_roles = debug || not (all (== boring_role) roles)
          roles = tyConRoles tc
@@ -2758,6 +2759,9 @@ ppr_tycons debug fam_insts type_env
             -- Matches the choice in IfaceSyn, calls to pprRoles
 
     ppr_ax ax = ppr (coAxiomToIfaceDecl ax)
+      -- We go via IfaceDecl rather than using pprCoAxiom
+      -- This way we get the full axiom (both LHS and RHS) with
+      -- wildcard binders tidied to _1, _2, etc.
 
 ppr_datacons :: Bool -> TypeEnv -> SDoc
 ppr_datacons debug type_env
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index f82e394590..ca5db45608 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -39,8 +39,8 @@ import Class
 import TyCon
 
 -- others:
-import IfaceType( pprIfaceType )
-import ToIface( toIfaceType )
+import IfaceType( pprIfaceType, pprIfaceTypeApp )
+import ToIface( toIfaceType, toIfaceTyCon, toIfaceTcArgs )
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
 import TcEnv       ( tcInitTidyEnv, tcInitOpenTidyEnv )
@@ -1931,7 +1931,10 @@ checkConsistentFamInst (InClsInst { ai_class = clas
                        fam_tc branch
   = do { traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
                                                 , ppr arg_triples
-                                                , ppr mini_env ])
+                                                , ppr mini_env
+                                                , ppr ax_tvs
+                                                , ppr ax_arg_tys
+                                                , ppr arg_triples ])
        -- Check that the associated type indeed comes from this class
        -- See [Mismatched class methods and associated type families]
        -- in TcInstDecls.
@@ -1941,15 +1944,14 @@ checkConsistentFamInst (InClsInst { ai_class = clas
        ; check_match arg_triples
        }
   where
-    CoAxBranch { cab_eta_tvs = eta_tvs, cab_lhs = pats } = branch
-    at_arg_tys = pats ++ mkTyVarTys eta_tvs
+    (ax_tvs, ax_arg_tys, _) = etaExpandCoAxBranch branch
 
     arg_triples :: [(Type,Type, ArgFlag)]
     arg_triples = [ (cls_arg_ty, at_arg_ty, vis)
                   | (fam_tc_tv, vis, at_arg_ty)
                        <- zip3 (tyConTyVars fam_tc)
-                               (tyConArgFlags fam_tc at_arg_tys)
-                               at_arg_tys
+                               (tyConArgFlags fam_tc ax_arg_tys)
+                               ax_arg_tys
                   , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ]
 
     pp_wrong_at_arg vis
@@ -1960,19 +1962,23 @@ checkConsistentFamInst (InClsInst { ai_class = clas
 
     -- Fiddling around to arrange that wildcards unconditionally print as "_"
     -- We only need to print the LHS, not the RHS at all
-    expected_args = [ lookupVarEnv mini_env at_tv `orElse` mk_wildcard at_tv
-                    | at_tv <- tyConTyVars fam_tc ]
+    -- See Note [Printing conflicts with class header]
+    (tidy_env1, _) = tidyVarBndrs emptyTidyEnv inst_tvs
+    (tidy_env2, _) = tidyCoAxBndrsForUser tidy_env1 (ax_tvs \\ inst_tvs)
+
+    pp_expected_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
+                     toIfaceTcArgs fam_tc $
+                     [ case lookupVarEnv mini_env at_tv of
+                         Just cls_arg_ty -> tidyType tidy_env2 cls_arg_ty
+                         Nothing         -> mk_wildcard at_tv
+                     | at_tv <- tyConTyVars fam_tc ]
+
+    pp_actual_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $
+                   toIfaceTcArgs fam_tc $
+                   tidyTypes tidy_env2 ax_arg_tys
+
     mk_wildcard at_tv = mkTyVarTy (mkTyVar tv_name (tyVarKind at_tv))
     tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "_") noSrcSpan
-    pp_expected_ty = pprIfaceType (toIfaceType (mkTyConApp fam_tc expected_args))
-                     -- Do /not/ tidy, because that will rename all those "_"
-                     -- variables we have put in.  And (I think) the intance type
-                     --  is already tidy
-
---    actual_ty   = mkTyConApp fam_tc at_arg_tys
---    (tidy_env, bndrs) = tidyCoAxBndrs (tyCoVarsOfTypesList [expected_ty, actual_ty])
---    pp_actual_ty pprPrecTypeX tidy_env topPrec actual_ty
-    pp_actual_ty = pprCoAxBranchLHS fam_tc branch
 
     -- For check_match, bind_me, see
     -- Note [Matching in the consistent-instantation check]
@@ -1987,8 +1993,8 @@ checkConsistentFamInst (InClsInst { ai_class = clas
       | otherwise
       = addErrTc (pp_wrong_at_arg vis)
 
-    -- The scoped type variables from the class-instance header
-    -- should not be alpha-raenamed.
+    -- The /scoped/ type variables from the class-instance header
+    -- should not be alpha-renamed.  Inferred ones can be.
     no_bind_set = mkVarSet inst_tvs
     bind_me tv | tv `elemVarSet` no_bind_set = Skolem
                | otherwise                   = BindMe
@@ -2123,6 +2129,46 @@ Here the instance is kind-indexed and really looks like
 But if the 'b' didn't scope, we would make F's instance too
 poly-kinded.
 
+Note [Printing conflicts with class header]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's remarkably painful to give a decent error message for conflicts
+with the class header.  Consider
+   clase C b where
+     type F a b c
+   instance C [b] where
+     type F x Int _ _ = ...
+
+Here we want to report a conflict between
+    Expected: F _ [b] _
+    Actual:   F x Int _ _
+
+But if the type instance shadows the class variable like this
+(rename/should_fail/T15828):
+   instance C [b] where
+     type forall b. F x (Tree b) _ _ = ...
+
+then we must use a fresh variable name
+    Expected: F _ [b] _
+    Actual:   F x [b1] _ _
+
+Notice that:
+  - We want to print an underscore in the "Expected" type in
+    positions where the class header has no influence over the
+    parameter.  Hence the fancy footwork in pp_expected_ty
+
+  - Although the binders in the axiom are aready tidy, we must
+    re-tidy them to get a fresh variable name when we shadow
+
+  - The (ax_tvs \\ inst_tvs) is to avoid tidying one of the
+    class-instance variables a second time, from 'a' to 'a1' say.
+    Remember, the ax_tvs of the axiom share identity with the
+    class-instance variables, inst_tvs..
+
+  - We use tidyCoAxBndrsForUser to get underscores rather than
+    _1, _2, etc in the axiom tyvars; see the definition of
+    tidyCoAxBndrsForUser
+
+This all seems absurdly complicated.
 
 Note [Unused explicitly bound variables in a family pattern]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index a55deeb1d3..ff0c9c5e9e 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -98,7 +98,8 @@ module Coercion (
 
         -- * Pretty-printing
         pprCo, pprParendCo,
-        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS, pprCoAxBranchUser,
+        pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
+        pprCoAxBranchUser, tidyCoAxBndrsForUser,
         etaExpandCoAxBranch,
 
         -- * Tidying
@@ -189,7 +190,7 @@ pprCoAxiom :: CoAxiom br -> SDoc
 -- Used in debug-printing only
 pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
   = hang (text "axiom" <+> ppr ax <+> dcolon)
-       2 (vcat (map (pprCoAxBranch tc) (fromBranches branches)))
+       2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
 
 pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
 -- Used when printing injectivity errors (FamInst.makeInjectivityErrors)
@@ -237,9 +238,9 @@ ppr_co_ax_branch ppr_rhs fam_tc branch
     pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
                              (tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)
 
-    (tidy_env, bndrs') = tidyCoAxBndrs ee_tvs
+    (tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
 
-tidyCoAxBndrs :: [Var] -> (TidyEnv, [Var])
+tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
 -- Tidy wildcards "_1", "_2" to "_", and do not return them
 -- in the list of binders to be printed
 -- This is so that in error messages we see
@@ -248,11 +249,10 @@ tidyCoAxBndrs :: [Var] -> (TidyEnv, [Var])
 --     forall a _1 _2. F _1 [a] _2 = ...
 --
 -- This is a rather disgusting function
-tidyCoAxBndrs tcvs
+tidyCoAxBndrsForUser init_env tcvs
   = (tidy_env, reverse tidy_bndrs)
   where
-    (tidy_env, tidy_bndrs) = foldl tidy_one (empty_env, []) tcvs
-    empty_env = mkEmptyTidyEnv (initTidyOccEnv [mkTyVarOcc "_"])
+    (tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
 
     tidy_one (env@(occ_env, subst), rev_bndrs') bndr
       | is_wildcard bndr = (env_wild, rev_bndrs')
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 149ff3f115..c6dcab6ea1 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -224,7 +224,7 @@ pprFamInst :: FamInst -> SDoc
 pprFamInst (FamInst { fi_flavor = flavor, fi_axiom = ax
                     , fi_tvs = tvs, fi_tys = tys, fi_rhs = rhs })
   = hang (ppr_tc_sort <+> text "instance"
-             <+> pprCoAxBranch (coAxiomTyCon ax) (coAxiomSingleBranch ax))
+             <+> pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax))
        2 (whenPprDebug debug_stuff)
   where
     ppr_tc_sort = case flavor of