Fix #11716.

There were several smallish bugs here:
 - We had too small an InScopeSet when rejigging GADT return types.
 - When adding the extra_tvs with a datatype kind signature, we
   were sometimes changing Uniques of an explicitly bound kind var.
 - Using coercionKind in the flattener got the wrong visibility
   for a binder. Now we just zonk to get what we need.

Test case: dependent/should_compile/RaeJobTalk

compiler/typecheck/TcCanonical.hs

@@ -559,7 +559,7 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
 -- Check only when flat because the zonk_eq_types check in canEqNC takes
 -- care of the non-flat case.
 can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
-  | ty1 `eqType` ty2
+  | ty1 `tcEqType` ty2
   = canEqReflexive ev ReprEq ty1
 
 -- When working with ReprEq, unwrap newtypes.
@@ -1505,7 +1505,7 @@ homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise
                            -- the 'Xi' is the new RHS
                   -> TcS (StopOrContinue Ct)
 homogeniseRhsKind ev eq_rel lhs rhs build_ct
-  | k1 `eqType` k2
+  | k1 `tcEqType` k2
   = continueWith (build_ct ev rhs)
 
   | CtGiven { ctev_evar = evar } <- ev

compiler/typecheck/TcFlatten.hs

@@ -1344,8 +1344,8 @@ flatten_tyvar3 tv
 --           (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 --                 , ppr _new_kind
 --                 , ppr kind_co <+> dcolon <+> ppr (coercionKind kind_co) ])
-       ; let Pair _ orig_kind = coercionKind kind_co
-             -- orig_kind might be zonked
+       ; orig_kind <- liftTcS $ zonkTcType kind
+             -- NB: orig_kind is *not* the kind returned from flatten
        ; return (FTRCasted (setTyVarKind tv orig_kind) kind_co) }
 
 {-

compiler/typecheck/TcHsType.hs

@@ -1842,12 +1842,18 @@ tcDataKindSig kind
                             , isNothing (lookupLocalRdrOcc rdr_env occ) ]
                  -- Note [Avoid name clashes for associated data types]
 
-        ; return ( [ mk_tv span uniq occ kind
-                   | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ]
+            -- NB: Use the tv from a binder if there is one. Otherwise,
+            -- we end up inventing a new Unique for it, and any other tv
+            -- that mentions the first ends up with the wrong kind.
+        ; return ( [ tv
+                   | ((bndr, occ), uniq) <- bndrs `zip` occs `zip` uniqs
+                   , let tv | Just bndr_tv <- binderVar_maybe bndr
+                            = bndr_tv
+                            | otherwise
+                            = mk_tv span uniq occ (binderType bndr) ]
                  , bndrs, res_kind ) }
   where
     (bndrs, res_kind) = splitPiTys kind
-    arg_kinds         = map binderType bndrs
     mk_tv loc uniq occ kind
       = mkTyVar (mkInternalName uniq occ loc) kind
 

compiler/typecheck/TcPat.hs

@@ -747,9 +747,14 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
 
               arg_tys' = substTys tenv arg_tys
 
-        ; traceTc "tcConPat" (vcat [ ppr con_name, ppr univ_tvs, ppr ex_tvs
+        ; traceTc "tcConPat" (vcat [ ppr con_name
+                                   , pprTvBndrs univ_tvs
+                                   , pprTvBndrs ex_tvs
                                    , ppr eq_spec
-                                   , ppr ex_tvs', ppr ctxt_res_tys, ppr arg_tys'
+                                   , ppr theta
+                                   , pprTvBndrs ex_tvs'
+                                   , ppr ctxt_res_tys
+                                   , ppr arg_tys'
                                    , ppr arg_pats ])
         ; if null ex_tvs && null eq_spec && null theta
           then do { -- The common case; no class bindings etc

compiler/typecheck/TcTyClsDecls.hs

@@ -1823,6 +1823,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
   = choose [] [] empty_subst empty_subst tmpl_tvs
   where
     in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
+               `unionInScope` getTCvInScope subst
     empty_subst = mkEmptyTCvSubst in_scope
 
     choose :: [TyVar]           -- accumulator of univ tvs, reversed
@@ -1844,12 +1845,12 @@ mkGADTVars tmpl_tvs dc_tvs subst
             ,  tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
             -> -- simple, well-kinded variable substitution.
                choose (r_tv:univs) eqs
-                      (extendTvSubst t_sub t_tv r_ty)
-                      (extendTvSubst r_sub r_tv r_ty)
+                      (extendTvSubst t_sub t_tv r_ty')
+                      (extendTvSubst r_sub r_tv r_ty')
                       t_tvs
             where
               r_tv1  = setTyVarName r_tv (choose_tv_name r_tv t_tv)
-              r_ty   = mkTyVarTy r_tv1
+              r_ty'  = mkTyVarTy r_tv1
 
                -- not a simple substitution. make an equality predicate
           _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)

compiler/typecheck/TcType.hs

@@ -180,6 +180,7 @@ module TcType (
   pprKind, pprParendKind, pprSigmaType,
   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
   pprTheta, pprThetaArrowTy, pprClassPred,
+  pprTvBndr, pprTvBndrs,
 
   TypeSize, sizeType, sizeTypes, toposortTyVars
 

testsuite/tests/dependent/should_compile/all.T

@@ -18,3 +18,4 @@ test('T11311', normal, compile, [''])
 test('T11405', normal, compile, [''])
 test('T11241', normal, compile, [''])
 test('T11711', normal, compile, [''])
+test('RaeJobTalk', normal, compile, [''])