Note [Retrying TyClGroups]

GHC/Tc/TyCl.hs:155 compiler 3 tickets

After renaming type, class, and instance declarations in a module (or, to be
more precise, in an HsGroup), GHC.Rename.Module.rnTyClDecls does dependency
analysis on the renamed declarations and returns a topologically sorted list
of SCCs, each SCC represented by one TyClGroup.

If the dependency analysis were complete, i.e. if it were able to discover all
dependencies between all declarations, then tcTyAndClassDecls could simply
kind-check TyClGroups in order. Unfortunately, this is not the case, because
dependencies come in two varieties:

* Lexical dependencies arise when X mentions Y by name:

    data X (a :: Y) = MkX   -- depends on Y
    data Y = MkY

* Non-lexical dependencies arise when an instance must be in the
  typing environment:

    type family F x
    data X (a :: F Int) = MkX a   -- depends on (F Int ~ Type)
    type instance F x = Type

Non-lexical dependencies can't be discovered by looking at the free variables of
a declaration (attempts to find a good heuristic did not bear fruit, see the
long discussion at #12088 and the linked Wiki pages). As a consequence, the
order of SCCs (i.e. TyClGroups) coming out of the renamer is determined solely
by lexical dependencies.

In other words, the TyClGroups are in /lexical dependency order/, meaning:
- definitely in dependency order if all dependencies are lexical
- possibly not in dependency order if there are non-lexical dependencies

Here are some examples how type checking declarations might go wrong due to
non-lexical dependencies:

* Consider (#11348)

    type family F a
    type instance F Int = Bool

    data R = MkR (F Int)

    type Foo = 'MkR 'True

  For Foo to kind-check we need to know that (F Int) ~ Bool.  But we won't
  know that unless we've looked at the type instance declaration for F
  before kind-checking Foo.

* Things become more complicated when we introduce transitive
  dependencies through imported definitions, like in this scenario:

      A.hs
        type family Closed (t :: Type) :: Type where
          Closed t = Open t

        type family Open (t :: Type) :: Type

      B.hs
        data Q where
          Q :: Closed Bool -> Q

        type instance Open Int = Bool

        type S = 'Q 'True

  Somehow, we must ensure that the instance Open Int = Bool is checked before
  the type synonym S. While we know that S depends upon 'Q depends upon Closed,
  we have no idea that Closed depends upon Open!

* Another example is this (#3990).

    data family Complex a
    data instance Complex Double = CD {-# UNPACK #

References 0

This Note does not link to any other.

Referenced by 10