Coercion Quantification

This patch corresponds to #15497.

According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2,
 we would like to have coercion quantifications back. This will
allow us to migrate (~#) to be homogeneous, instead of its current
heterogeneous definition. This patch is (lots of) plumbing only. There
should be no user-visible effects.

An overview of changes:

- Both `ForAllTy` and `ForAllCo` can quantify over coercion variables,
but only in *Core*. All relevant functions are updated accordingly.
- Small changes that should be irrelevant to the main task:
    1. removed dead code `mkTransAppCo` in Coercion
    2. removed out-dated Note Computing a coercion kind and
       roles in Coercion
    3. Added `Eq4` in Note Respecting definitional equality in
       TyCoRep, and updated `mkCastTy` accordingly.
    4. Various updates and corrections of notes and typos.
- Haddock submodule needs to be changed too.

Acknowledgments:
This work was completed mostly during Ningning Xie's Google Summer
of Code, sponsored by Google. It was advised by Richard Eisenberg,
supported by NSF grant 1704041.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar

Subscribers: RyanGlScott, monoidal, rwbarton, carter

GHC Trac Issues: #15497

Differential Revision: https://phabricator.haskell.org/D5054

1 files changed, 0 insertions, 1 deletions

diff --git a/compiler/specialise/SpecConstr.hs b/compiler/specialise/SpecConstr.hs
index 0d57860941..f6d27ccba5 100644
--- a/compiler/specialise/SpecConstr.hs
+++ b/compiler/specialise/SpecConstr.hs
@@ -38,7 +38,6 @@ import TyCon            ( tyConName )
 import Id
 import PprCore          ( pprParendExpr )
 import MkCore           ( mkImpossibleExpr )
-import Var
 import VarEnv
 import VarSet
 import Name