#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #15497 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs/ Richard's thesis] Section 5.8.5.2, there is a restriction on where a coercion variable can appear in `ForAllCo` for the sake of consistency: the coercion variable can appear nowhere except in coherence coercions. Currently this restriction is missing in coercion quantification (see #15497). The goal of this ticket is to add the missing restriction. After discussion with Richard, we restate the restriction a little bit: the coercion variable can appear nowhere except in `GRefl` and `Refl`. Allowing it to appear in `Refl` should not break consistency. Notice that this also means `liftCoSubst` might fail when it lifts a `ForAllTy` over a coercion variable to a `ForAllCo`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15757 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler