Adding almost devoid check for covar in ForAllCo
authorNingning Xie <xnningxie@gmail.com>
Fri, 19 Oct 2018 09:10:08 +0000 (17:10 +0800)
committerNingning Xie <xnningxie@gmail.com>
Fri, 19 Oct 2018 09:43:30 +0000 (17:43 +0800)
commit879db5595208fb665ff1a0a2b12b9921d3efae0e
tree6fea8c1af0b77167fa22089c3a5630454f2651a2
parent46f2906d1c6e1fb732a90882487479a2ebf19ca1
Adding almost devoid check for covar in ForAllCo

Summary:
For the sake of consistency of the dependent core, there is a restriction on
where a coercion variable can appear in ForAllCo: the coercion variable can
appear nowhere except in coherence coercions.

Currently this restriction is missing in Core. The goal of this patch is to add
the missing restriction.

After discussion, we decide: coercion variables can appear nowhere except in
`GRefl` and `Refl`. Relaxing the restriction to include `Refl` should not break
consistency, we premuse.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15757

Differential Revision: https://phabricator.haskell.org/D5231
compiler/coreSyn/CoreLint.hs
compiler/types/Coercion.hs
compiler/types/Coercion.hs-boot
compiler/types/TyCoRep.hs