GHC Handbook

Note [TcLevel invariants]

GHC/Tc/Utils/TcType.hs:737 compiler 

* Each unification variable (MetaTv)
  and skolem (SkolemTv)
  and each Implication
  has a level number (of type TcLevel)

* INVARIANT (KindInv) Given a type variable (tv::ki) at at level L,
                      the free vars of `ki` all have level <= L

* INVARIANTS.  In a tree of Implications,

    (ImplicInv) The level number (ic_tclvl) of an Implication is
                STRICTLY GREATER THAN that of its parent

    (SkolInv)   The level number of the skolems (ic_skols) of an
                Implication is equal to the level of the implication
                itself (ic_tclvl)

    (GivenInv)  The level number of a unification variable appearing
                in the 'ic_given' of an implication I should be
                STRICTLY LESS THAN the ic_tclvl of I
                See Note [GivenInv]

    (WantedInv) The level number of a unification variable appearing
                in the 'ic_wanted' of an implication I should be
                LESS THAN OR EQUAL TO the ic_tclvl of I
                See Note [WantedInv]

The level of a MetaTyVar also governs its untouchability.  See
Note [Unification preconditions] in GHC.Tc.Utils.Unify.

  See also Note [The QLInstVar TcLevel]

References 4

Referenced by 15