Opened 8 months ago

Closed 7 months ago

Last modified 7 months ago

#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@…>

In e19dc21f8a876a0b4849311d664472e61658d06d/testsuite:

Testcase #8565 no longer broken

at least with ImpredicativeTypes enabled in this module.

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...

Last edited 7 months ago by nomeata (previous) (diff)
Note: See TracTickets for help on using tickets.