Use unified notation to refer to equations that implement a certain typing rule.

The project is structured in such a way that functions prefixed with "tc" implement certain judgements, and their equations implements the corresponding judgement's rules.

We already have a certain notation for connecting rules and their implementation by using the following template: -- | Rule: JUDGEMENT-RULE

For example, the equation -- or in this case, the guarded expression -- that implements the Pat-ConCheck rule is annotated with -- | Rule: Pat-ConCheck:

         -- | Rule: Pat-ConCheck
         -- | Rule: Pat-KPInfer
         DataConRes dt@(MkDataConType { dctPsis  = psis
                                     , dctTyCon = tyCon
                                     , dctArgs  = taus }) ->
           do traceTc "tcPat - Pat-{ConCheck,KPInfer}"
                      $ vsep [pretty "DataCon:" <+> pprConLike cl
                             ,pretty "DataCon's type:" <+> pprDataConType dt
                             ,pretty "APats:" <+> pprArgs apats]
              mvs <- matchExpectedConTy expType tyCon taus -- See Note [matchExpectedConTy]
              (psps, dlt, qs1, toSkolSubst) <- tcSkolAPats gamma psis apats
              -- TODO: Refactor me
              (omegaSk, gadtWanteds) <- tcSolve $ zip (map (tauToSigma . appTvSubstTau toSkolSubst) taus)
                                                      (map tauToSigma mvs)
              traceTc "Delta returned by tcSkolAPats:" (pprDelta dlt)
              qs1ts <- mapM (fmap (mkCt CtGiven) . sigmaToTauTc . appSkSubstSigma omegaSk) qs1
              emitSimples $ gadtWanteds ++ qs1ts
              (dlt', qs3) <- tcPatsCheck (modifyDelta (dlt <>) gamma)
                                         (map (second (appSkSubstSigma omegaSk)) psps)
              traceTc "Delta returned by tcPatsCheck:" (pprDelta dlt')
              pure (dlt <> dlt', qs1 ++ qs3)

What if we want to refer to this "equation"? I think the best notation is to prepend the rule with the function name. I.e, in the case of this specific example, we'd have to write: tcPat-Pat-ConCheck.