Note [Tricky scoping in generaliseTcTyCon]
Consider #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 Name 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.
References 0
This Note does not link to any other.
Referenced by 1
- Inferring kinds for type declarations GHC.Tc.TyCl