#8565: New GeneralisedNewtypeDeriving needs help with higher rank types -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: typecheck/should_compile/T8565 | Unknown Blocking: | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by simonpj): It should be fine. Solving `Coercible s t` constraints is very very like solving `s ~ t` constraints. Just as we have a rule for `[s] ~ [t]` (by solving the constraint `s~t`), so we have a rule for `Coercible [s] [t]`. Now, we do have a rule for `(forall a. s) ~ (forall a. t)`, but it's a bit tricky because of the scoping of `a`. We have to solve the implication constraint `forall a. s~t`. To see how we do this for equality constraint, look on line 745 of `TcCanonical`, and the key support function `TcSMonad.deferTcSForAllEq`. The latter is the whole reason for `TcLetCo`, which was a significant innovation at the time. (Previously we could not decompose `forall/forall` equalities.) But now it's there, you should be able to use the exact same strategy for `Coercible`. (Provided you complete the `EvCoercible` refactoring you started.) Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler