Wibbles in response to Richardwip/T16342

5 files changed, 150 insertions, 68 deletions

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 74f6d86eec..d40b722b6b 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -34,7 +34,7 @@ module TcHsSyn (
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
         zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
-        zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrsX,
+        zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
         zonkTcTypesToTypes, zonkTcTypesToTypesX,
         zonkTyVarOcc,
@@ -459,13 +459,15 @@ zonkTyVarBinderX env (Bndr tv vis)
   = do { (env', tv') <- zonkTyBndrX env tv
        ; return (env', Bndr tv' vis) }
 
-zonkRecTyVarBndrsX :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
-zonkRecTyVarBndrsX names tc_tvs
+zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
+-- This rather specialised function is used in exactly one place.
+-- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls.
+zonkRecTyVarBndrs names tc_tvs
   = initZonkEnv $ \ ze ->
-    fixM $ \ ~(_, new_tvs) ->
+    fixM $ \ ~(_, rec_new_tvs) ->
     do { let ze' = extendTyZonkEnvN ze $
                    zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv))
-                               tc_tvs new_tvs
+                               tc_tvs rec_new_tvs
        ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs
        ; return (ze', new_tvs) }
   where
@@ -475,7 +477,7 @@ zonkRecTyVarBndrsX names tc_tvs
               vcat [ text "old:" <+> ppr tc_tv <+> dcolon <+> ppr (tyVarKind tc_tv)
                    , text "new:" <+> ppr name <+> dcolon <+> ppr ki ]
            ; return (mkTyVar name ki) }
-    
+
 zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc)
 zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
 
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 57623ba925..11cc61ceaf 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1924,6 +1924,9 @@ kcLHsQTyVars_NonCusk name flav
 
              all_tv_prs = (kv_ns                `zip` scoped_kvs) ++
                           (hsLTyVarNames hs_tvs `zip` tc_tvs)
+               -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
+               --     variables, hence the need to zip here.  Ditto bindExplicit..
+               -- See TcMType Note [Unification variables get fresh Names]
              tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
                                False -- not yet generalised
                                flav
@@ -2085,7 +2088,7 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
 
 newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
 newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
-   -- See Note [Unification variables should have fresh Names] in TcMType
+   -- See Note [Unification variables get fresh Names] in TcMType
 
 --------------------------------------
 -- Explicit binders
@@ -2127,6 +2130,8 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
             -- Extend the environment as we go, in case a binder
             -- is mentioned in the kind of a later binder
             --   e.g. forall k (a::k). blah
+            -- NB: tv's Name may differ from hs_tv's
+            -- See TcMType Note [Unification variables get fresh Names]
             ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
                            go hs_tvs
             ; return (tv:tvs, res) }
@@ -2215,8 +2220,8 @@ kcLookupTcTyCon nm
 
 zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
 zonkAndScopedSort spec_tkvs
-  = do { spec_tkvs <- mapM zonkTcTyCoVarBndr spec_tkvs
-          -- Use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
+  = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs
+          -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv
 
        -- Do a stable topological sort, following
        -- Note [Ordering of implicit variables] in RnTypes
@@ -2520,7 +2525,7 @@ tcHsPartialSigType ctxt sig_ty
          -- we need to promote the TyVarTvs so we don't violate the TcLevel
          -- invariant
        ; implicit_tvs <- zonkAndScopedSort implicit_tvs
-       ; explicit_tvs <- mapM zonkTcTyCoVarBndr explicit_tvs
+       ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs
        ; theta        <- mapM zonkTcType theta
        ; tau          <- zonkTcType tau
 
@@ -2638,6 +2643,7 @@ tcHsPatSigType ctxt sig_ty
                        RuleSigCtxt {} -> newSkolemTyVar name kind
                        _              -> newTauTyVar    name kind
                        -- See Note [Pattern signature binders]
+             -- NB: tv's Name may be fresh (in the case of newTauTyVar)
            ; return (name, tv) }
 
 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index d0af40e264..c641662689 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -70,9 +70,8 @@ module TcMType (
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
   CandidatesQTvs(..), delCandidates, candidateKindVars,
-  skolemiseQuantifiedTyVar, defaultTyVar,
-  quantifyTyVars,
-  zonkTcTyCoVarBndr,
+  zonkAndSkolemise, skolemiseQuantifiedTyVar,
+  defaultTyVar, quantifyTyVars,
   zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind,
 
@@ -681,28 +680,29 @@ cloneMetaTyVarName name
 At the moment we give a unification variable a System Name, which
 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
 
-Note [Unification variables should have fresh Names]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Unification variables get fresh Names]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Whenever we allocate a unification variable (MetaTyVar) we give
 it a fresh name.   Trac #16221 is a very tricky case that illustrates
 why this is important:
 
-   data T0 a = forall k2 (b :: k2). MkT0 (T0 b) !Int
+   data SameKind :: k -> k -> *
+   data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int
 
 When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl
 we allocate a unification variable kappa2 for k2, and then we
-end up unifying kappa1 := kappa2 (because of the (T0 b).
+end up unifying kappa1 := kappa2 (because of the (SameKind a b).
 
 Now we generalise over kappa2; but if kappa2's Name is k2,
 we'll end up giving T0 the kind forall k2. k2 -> *.  Nothing
-directly worng with that but when we typecheck the data constrautor
+directly wrong with that but when we typecheck the data constrautor
 we end up giving it the type
   MkT0 :: forall k1 (a :: k1) k2 (b :: k2).
-          T0 @{k2} b -> Int -> T0 @{k2} a
-which is boguus.  The result type should be T0 @{k1} a.
+          SameKind @k2 a b -> Int -> T0 @{k2} a
+which is bogus.  The result type should be T0 @{k1} a.
 
 And there no reason /not/ to clone the Name when making a
-unification variable.  So taht's what we do.
+unification variable.  So that's what we do.
 -}
 
 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
@@ -727,7 +727,7 @@ newSkolemTyVar name kind
 
 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
 -- See Note [TyVarTv]
--- See Note [Unification variables should have fresh Names]
+-- See Note [Unification variables get fresh Names]
 newTyVarTyVar name kind
   = do { details <- newMetaDetails TyVarTv
        ; name' <- cloneMetaTyVarName name
@@ -1493,6 +1493,24 @@ quantifiableTv outer_tclvl tcv
   | otherwise
   = False
 
+zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar
+-- A tyvar binder is never a unification variable (TauTv),
+-- rather it is always a skolem. It *might* be a TyVarTv.
+-- (Because non-CUSK type declarations use TyVarTvs.)
+-- Regardless, it may have a kind that has not yet been zonked,
+-- and may include kind unification variables.
+zonkAndSkolemise tyvar
+  | isTyVarTyVar tyvar
+     -- We want to preserve the binding location of the original TyVarTv.
+     -- This is important for error messages. If we don't do this, then
+     -- we get bad locations in, e.g., typecheck/should_fail/T2688
+  = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
+       ; skolemiseQuantifiedTyVar zonked_tyvar }
+
+  | otherwise
+  = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
+    zonkTyCoVarKind tyvar
+
 skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables
@@ -1994,28 +2012,6 @@ zonkTcType = mapType zonkTcTypeMapper ()
 zonkCo :: Coercion -> TcM Coercion
 zonkCo = mapCoercion zonkTcTypeMapper ()
 
-zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
--- A tyvar binder is never a unification variable (TauTv),
--- rather it is always a skolem. It *might* be a TyVarTv.
--- (Because non-CUSK type declarations use TyVarTvs.)
--- Regardless, it may have a kind that has not yet been zonked,
--- and may include kind unification variables.
-zonkTcTyCoVarBndr tyvar
-  | isTyVarTyVar tyvar
-     -- We want to preserve the binding location of the original TyVarTv.
-     -- This is important for error messages. If we don't do this, then
-     -- we get bad locations in, e.g., typecheck/should_fail/T2688
-  = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
---       ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty
---             zonked_name  = getName zonked_tyvar
---             reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar)
---       ; return (setTyVarName zonked_tyvar reloc'd_name) }
-       ; skolemiseQuantifiedTyVar zonked_tyvar }
-
-  | otherwise
-  = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
-    zonkTyCoVarKind tyvar
-
 zonkTcTyVar :: TcTyVar -> TcM TcType
 -- Simply look through all Flexis
 zonkTcTyVar tv
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index a2f2bc9442..ff8b3437a3 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -552,7 +552,7 @@ generaliseTcTyCon tc
        -- Step 0: zonk and skolemise the Specified and Required binders
        -- It's essential that they are skolems, not MetaTyVars,
        -- for Step 3 to work right
-       ; spec_req_tvs <- mapM zonkTcTyCoVarBndr spec_req_tvs
+       ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs
              -- Running example, where kk1 := kk2, so we get
 
        -- Step 1: find all the variables we want to quantify over,
@@ -575,7 +575,7 @@ generaliseTcTyCon tc
        ; traceTc "generaliseTcTyCon: before zonkRec"
            (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
                  , text "inferred =" <+> pprTyVars inferred ])
-       ; (ze, spec_req_tvs) <- zonkRecTyVarBndrsX spec_req_names spec_req_tvs
+       ; (ze, spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs
            -- So ze maps from the tyvars that have ended up
            --
 
@@ -583,7 +583,7 @@ generaliseTcTyCon tc
        -- (remember they all started as TyVarTvs).
        -- They have been skolemised by quantifyTyVars.
        ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind
-       
+
        ; traceTc "generaliseTcTyCon: post zonk" $
          vcat [ text "tycon =" <+> ppr tc
               , text "inferred =" <+> pprTyVars inferred
@@ -594,6 +594,7 @@ generaliseTcTyCon tc
        -- Step 4: Find the Specified and Inferred variables
        -- NB: spec_req_tvs = spec_tvs ++ req_tvs
        --     And req_tvs is 1-1 with tyConTyVars
+       --     See Note [Scoped tyvars in a TcTyCon] in TyCon
        ; let n_spec        = length spec_req_tvs - tyConArity tc
              (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs
              specified     = scopedSort spec_tvs
@@ -786,12 +787,30 @@ that do not have a CUSK.  Consider
 We do kind inference as follows:
 
 * Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk.
+  Make a unification variable for each of the Required and Specified
+  type varialbes in the header.
+
+  Record the connection between the Names the user wrote and the
+  fresh unification variables in the tcTyConScopedTyVars field
+  of the TcTyCon we are making
+      [ (a,  aa)
+      , (k1, kk1)
+      , (k2, kk2)
+      , (x,  xx) ]
+  (I'm using the convention that double letter like 'aa' or 'kk'
+  mean a unification variable.)
+
+  These unification variables
+    - Are TyVarTvs: that is, unification variables that can
+      unify only with other type variables.
+      See Note [Signature skolems] in TcType
+
+    - Have complete fresh Names; see TcMType
+      Note [Unification variables get fresh Names]
+
   Assign initial monomorophic kinds to S, T
           S :: kk1 -> * -> kk2 -> *
           T :: kk3 -> * -> kk4 -> *
-  Here kk1 etc are TyVarTvs: that is, unification variables that
-  are allowed to unify only with other type variables. See
-  Note [Signature skolems] in TcType
 
 * Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
   T, with these monomophic kinds.  Now kind-check the declarations,
@@ -809,18 +828,20 @@ We do kind inference as follows:
   Note [Required, Specified, and Inferred for types]),
   and perform some validity checks.
 
-  This makes the utterly-final TyConBinders for the TyCon
+  This makes the utterly-final TyConBinders for the TyCon.
 
   All this is very similar at the level of terms: see TcBinds
   Note [Quantified variables in partial type signatures]
 
+  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
+
 * Step 4.  Extend the type environment with a TcTyCon for S and T, now
   with their utterly-final polymorphic kinds (needed for recursive
   occurrences of S, T).  Now typecheck the declarations, and build the
   final AlgTyCOn for S and T resp.
 
-The first three steps are in kcTyClGroup;
-the fourth is in tcTyClDecls.
+The first three steps are in kcTyClGroup; the fourth is in
+tcTyClDecls.
 
 There are some wrinkles
 
@@ -859,7 +880,51 @@ There are some wrinkles
     a) when collecting quantification candidates, in
        candidateQTyVarsOfKind, we must collect skolems
     b) quantifyTyVars should be a no-op on such a skolem
--}
+
+Note [Tricky scoping in generaliseTcTyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider Trac #16342
+  class C (a::ka) x where
+    cop :: D a x => x -> Proxy a -> Proxy a
+    cop _ x = x :: Proxy (a::ka)
+
+  class D (b::kb) y where
+    dop :: C b y => y -> Proxy b -> Proxy b
+    dop _ x = x :: Proxy (b::kb)
+
+C and D are mutually recursive, by the time we get to
+generaliseTcTyCon we'll have unified kka := kkb.
+
+But when typechecking the default declarations for 'cop' and 'dop' in
+tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
+But at that point all we have is the utterly-final Class itself.
+
+Conclusion: the classTyVars of a class must have the same Mame as
+that originally assigned by the user.  In our example, C must have
+classTyVars {a, ka, x} while D has classTyVars {a, kb, y}.  Despite
+the fact that kka and kkb got unified!
+
+We achieve this sleight of hand in generaliseTcTyCon, using
+the specialised function zonkRecTyVarBndrs.  We make the call
+   zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
+where the [ka,a,x] are the Names originally assigned by the user, and
+[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
+zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
+   kkb :-> (ka :: <zonked kind of kkb>)
+   aa  :-> (a  :: <konked kind of aa>)
+   etc
+That is, it maps each skolemised TcTyVars to the utterly-final
+TyVar to put in the class, with its correct user-specified name.
+When generalising D we'll do the same thing, but the ZonkEnv will map
+   kkb :-> (kb :: <zonked kind of kkb>)
+   bb  :-> (b  :: <konked kind of bb>)
+   etc
+Note that 'kkb' again appears in the domain of the mapping, but this
+time mapped to 'kb'.  That's how C and D end up with differently-named
+final TyVars despite the fact that we unified kka:=kkb
+
+zonkRecTyVarBndrs we need to do knot-tying because of the need to
+apply this same substitution to the kind of each.  -}
 
 --------------
 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 571ceeb309..ce40d74278 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -871,29 +871,42 @@ data TyCon
 
         -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyConBinder], -- ^ Full binders
-        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
-        tyConResKind :: Kind,             -- ^ Result kind
-        tyConKind    :: Kind,             -- ^ Kind of this TyCon
-        tyConArity   :: Arity,            -- ^ Arity
+        tyConTyVars  :: [TyVar],       -- ^ TyVar binders
+        tyConResKind :: Kind,          -- ^ Result kind
+        tyConKind    :: Kind,          -- ^ Kind of this TyCon
+        tyConArity   :: Arity,         -- ^ Arity
+
+          -- NB: the TyConArity of a TcTyCon must match
+          -- the number of Required (positional, user-specified)
+          -- arguments to the type constructor; see the use
+          -- of tyConArity in generaliseTcTyCon
 
         tcTyConScopedTyVars :: [(Name,TyVar)],
           -- ^ Scoped tyvars over the tycon's body
-          -- See Note [How TcTyCons work] in TcTyClsDecls
-          --
-          -- This list is specified_tvs ++ required_tvs
-          -- where required_tvs teh same as tyConTyVars
-          --
-          -- Order *does* matter: for TcTyCons with a CUSK,
-          -- it's the correct dependency order. For TcTyCons
-          -- without a CUSK, it's the original left-to-right
-          -- that the user wrote. Nec'y for getting Specified
-          -- variables in the right order.
+          -- See Note [Scoped tyvars in a TcTyCon]
 
         tcTyConIsPoly     :: Bool, -- ^ Is this TcTyCon already generalized?
 
         tcTyConFlavour :: TyConFlavour
                            -- ^ What sort of 'TyCon' this represents.
       }
+{- Note [Scoped tyvars in a TcTyCon]
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The tcTyConScopedTyVars field records the lexicial-binding connection
+between the original, user-specified Name (i.e. thing in scope) and
+the TcTyVar that the Name is bound to.
+
+Order *does* matter; the tcTyConScopedTyvars list consists of
+     specified_tvs ++ required_tvs
+
+where
+   * specified ones first
+   * required_tvs the same as tyConTyVars
+   * tyConArity = length required_tvs
+
+See also Note [How TcTyCons work] in TcTyClsDecls
+-}
 
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
 data AlgTyConRhs