• Simon Peyton Jones's avatar
    Orient TyVar/TyVar equalities with deepest on the left · 2bbdd00c
    Simon Peyton Jones authored
    Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
    want to orient them with the deepest-bound skolem on the left. As it
    happens, we also want to do the same for Wanteds, but for a different
    reason (more likely to be touchable).  Either way, deepest wins:
    see TcUnify Note [Deeper level on the left].
    
    This observation led me to some significant changes:
    
    * A SkolemTv already had a TcLevel, but the level wasn't really being
      used.   Now it is!
    
    * I updated added invariant (SkolInf) to TcType
      Note [TcLevel and untouchable type variables], documenting that
      the level number of all the ic_skols should be the same as the
      ic_tclvl of the implication
    
    * FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
      zero, which messed the scheme up.   Now they get a level number the
      same way as all other TcTyVars, instead of being a special case.
    
    * To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
      was previously done via their magic zero level) isTouchableMetaTyVar
      just tests for those two cases.
    
    * TcUnify.swapOverTyVars is the crucial orientation function; see the
      new Note [TyVar/TyVar orientation].  I completely rewrote this function,
      and it's now much much easier to understand.
    
    I ended up doing some related refactoring, of course
    
    * I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
      a lot of useless work in the case where there are no skolems; I
      added a fast-patch
    
    * Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
      the higher-order parameter to tcExpliciTKBndrsX.
    
    * Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
      by analogy with TcUnify.checkConstraints.
    
    * Inline TcUnify.buildImplication into its only call-site in
      TcUnify.checkConstraints
    
    * TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
      simpler API
    
    * Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
      nuke the latter, adding Note [No evidence bindings] to TcEvidence.
    2bbdd00c
TcEvidence.hs 35 KB