[GHC] #8565: New GeneralisedNewtypeDeriving needs help with higher rank types
#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 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Consider {{{ {-# LANGUAGE RankNTypes, GeneralizedNewtypeDeriving #-} module Foo where class C a where op :: (forall b. b -> a) -> a newtype T x = MkT x deriving( C ) }}} With the new "coerce" implementation of GND, this fails: {{{ Foo.hs:7:31: Cannot instantiate unification variable ‛b0’ with a type involving foralls: (forall b. b -> T x) -> T x Perhaps you want ImpredicativeTypes In the expression: GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) :: (forall (b :: *). b -> T x) -> T x In an equation for ‛op’: op = GHC.Prim.coerce (op :: (forall (b :: *). b -> x) -> x) :: (forall (b :: *). b -> T x) -> T x }}} We want to coerce betweeen {{{ (forall b. b -> x) -> x ~R (forall b. b -> T x) -> T x }}} There are two difficulties with the new `coerce` approach: * Regarded as source code, instance declaration {{{ instance C x => C (T x) where op = coerce (op :: (forall b. b -> x) -> x) }}} requires impredicative instantiation. * We probably don't have a decomposition rule for `Coercible (forall a. t1) (forall a. t2)` There is no difficulty in principle here, but it's not quite obvious what the best approach to a fix is. But it would be good to fix before release; we don't want to break `conduit` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Joachim Breitner
#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: -------------------------------------------------+------------------------- Changes (by nomeata): * testcase: => typecheck/should_compile/T8565 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by kazu-yamamoto): * cc: kazu@… (added) * testcase: typecheck/should_compile/T8565 => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: -------------------------------------------------+------------------------- Changes (by nomeata): * testcase: => typecheck/should_compile/T8565 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 goldfire): I just tested this with `ImpredicativeTypes` on, and the error message was from the `Coercible` stuff. With another case in that code (and `ImpredicativeTypes`), I think this would work. The underlying roles machinery is certainly strong enough to handle this case. I'm OK if we require a user to specify `ImpredicativeTypes` for this to work -- it really is impredicative! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 nomeata): I’m working on {{{ instance (forall a. (Coercible t1 t2)) => Coercible (forall a. t1) (forall a. t2) }}} and am almost done, just trying to get the desugarer cope with new type variables in derived constraints. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 nomeata): Unfortunately, it seems that no such instances, with `forall` on the left, existed so far, so writing it by hand yields `Malformed instance head`. I tried to trick GHC to accept a forall on the left hand side of the instance heads (using `ConstraintTypes` and `KindSignatures`) {{{ class C a where op :: a type Foo (a:: * -> Constraint) = forall b. a b instance Foo C => C Int }}} but that only yielded {{{ Malformed predicate ‛Foo C’ In the context: (Foo C) While checking an instance declaration In the instance declaration for ‛C Int’ }}} Do we really want instances for `Coercible` where the instance head is not valid GHC code? (I don’t even dare to call it Haskell code ;-)) Or can the instance be somehow phrased differently? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 nomeata): Hmm, after more reading of the type class inference code I have doubts that this can be implemented without a larger refactoring of the the the typechecker and desugarer for instances. One of the reasons is that when `instance (forall a. (Coercible t1 t2)) => Coercible (forall a. t1) (forall a. t2)` were used when solving a constraint, the type variable will get turned into a parameter to the dictionary for the superclass, so is local to that. But if that constraint requires further instances, their dictionaries will require the same parameter, so this would require, in a way, a nested structure for the type class solver. The only work-around I can think of is asking the user to write the instance for `C` (or in the case of conduit, `MFunctor`) by hand. Which is unsatisfying. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 nomeata): Thanks for pointing me to `deferTcSForAllEq`, I’ll look into it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Joachim Breitner
#8565: New GeneralisedNewtypeDeriving needs help with higher rank types -------------------------------------------------+------------------------- Reporter: simonpj | Owner: Type: bug | Status: Priority: normal | closed Component: Compiler | Milestone: Resolution: fixed | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple typecheck/should_compile/T8565 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by nomeata): * status: new => closed * resolution: => fixed Comment: After a day of refactoring I got it to work. The code will still need `{-# LANGUAGES ImpredicativeTypes #-}, but otherwise things work as expected. Pushing as we speak... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8565#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC