Here's a gnarly test case

{-# LANGUAGE MultiParamTypeClasses, TypeInType, ConstrainedClassMethods, ScopedTypeVariables #-}

module Foo where

import Data.Proxy

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)

This crashes every recent GHC outright, with

    • GHC internal error: ‘kb’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [avu :-> Type variable ‘b’ = b :: ka,
                               avv :-> Type variable ‘y’ = y :: *,
                               avw :-> Identifier[x::Proxy b, NotLetBound],
                               avx :-> Type variable ‘ka’ = ka :: *]
    • In the kind ‘kb’
      In the first argument of ‘Proxy’, namely ‘(b :: kb)’
      In an expression type signature: Proxy (b :: kb)
   |
13 |   dop _ x = x :: Proxy (b::kb)
   |                            ^^

Yikes.

Reason:

• C and D are mutually recursive
• ka and kb get bound to unification variables, and then get unified in the kind-inference phase
• As a result the utterly-final class for C and D end up with the same TyVar for ka/kb.
• And then, for one of them, the tyvar is not in scope when (much, much later) we check the default declaration.

Gah! In generaliseTcTyCon I think we may need to do a reverse-map to ensure that each of the final tyConTyVars has the Name from this declaration, rather than accidentally getting a Name from another decl in the mutually recursive group.