#8565 closed bug (fixed)
New GeneralisedNewtypeDeriving needs help with higher rank types
Reported by: | simonpj | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.6.3 |
Keywords: | Cc: | nomeata, goldfire, kazu@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Difficulty: | Unknown |
Test Case: | typecheck/should_compile/T8565 | Blocked By: | |
Blocking: | Related Tickets: |
Description
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
Change History (12)
comment:1 Changed 8 months ago by Joachim Breitner <mail@…>
comment:2 Changed 8 months ago by nomeata
- Test Case set to typecheck/should_compile/T8565
comment:3 Changed 8 months ago by kazu-yamamoto
- Cc kazu@… added
- Test Case typecheck/should_compile/T8565 deleted
comment:4 Changed 8 months ago by nomeata
- Test Case set to typecheck/should_compile/T8565
comment:5 Changed 8 months ago 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!
comment:6 Changed 8 months ago 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.
comment:7 Changed 8 months ago 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?
comment:8 Changed 8 months ago 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.
comment:9 Changed 8 months ago 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
comment:10 Changed 8 months ago by nomeata
Thanks for pointing me to deferTcSForAllEq, I’ll look into it.
comment:11 Changed 7 months ago by Joachim Breitner <mail@…>
comment:12 Changed 7 months ago by nomeata
- Resolution set to fixed
- Status changed from new to closed
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...
In 2f78a4e2ad68b3dd0ca76405e650bc37fe99e00b/testsuite: