#14883 closed bug (fixed)

QuantifiedConstraints don't kick in when used in TypeApplications

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #15290 Differential Rev(s): Phab:D4895
Wiki Page:

Description

Consider the following program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind

type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)

class Representational1 f => Functor' f where
  fmap' :: (a -> b) -> f a -> f b

class Functor' f => Applicative' f where
  pure'  :: a -> f a
  (<*>@) :: f (a -> b) -> f a -> f b

class Functor' t => Traversable' t where
  traverse' :: Applicative' f => (a -> f b) -> t a -> f (t b)

-- Typechecks
newtype T1 m a = MkT1 (m a) deriving Functor'
instance Traversable' m => Traversable' (T1 m) where
  traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b)
  traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                     @((a -> f b) -> T1 m a -> f (T1 m b))
                     traverse'

-- Doesn't typecheck
newtype T2 m a = MkT2 (m a) deriving Functor'
instance Traversable' m => Traversable' (T2 m) where
  traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
                     @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                     traverse'

This defines a variant of Functor that has forall a b. Coercible a b. Coercible (m a) (m b) as a superclass, and also defines versions of Applicative and Traversable that use this Functor variant. This is towards the ultimate goal of defining Traversable' à la GeneralizedNewtypeDeriving.

This attempt (using InstanceSigs) typechecks:

newtype T1 m a = MkT1 (m a) deriving Functor'
instance Traversable' m => Traversable' (T1 m) where
  traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b)
  traverse' = coerce @((a -> f b) ->    m a -> f    (m b))
                     @((a -> f b) -> T1 m a -> f (T1 m b))
                     traverse'

However, this version (which is closer to what GeneralizedNewtypeDeriving would actually create) does not typecheck:

newtype T2 m a = MkT2 (m a) deriving Functor'
instance Traversable' m => Traversable' (T2 m) where
  traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
                     @(forall f a b. Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                     traverse'
$ ghc-cq/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:38:15: error:
    • Couldn't match representation of type ‘f1 (m b1)’
                               with that of ‘f1 (T2 m b1)’
        arising from a use of ‘coerce’
      NB: We cannot know what roles the parameters to ‘f1’ have;
        we must assume that the role is nominal
    • In the expression:
        coerce
          @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b))
          @(forall f a b.
            Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
          traverse'
      In an equation for ‘traverse'’:
          traverse'
            = coerce
                @(forall f a b. Applicative' f => (a -> f b) -> m a -> f (m b))
                @(forall f a b.
                  Applicative' f => (a -> f b) -> T2 m a -> f (T2 m b))
                traverse'
      In the instance declaration for ‘Traversable' (T2 m)’
    • Relevant bindings include
        traverse' :: (a -> f b) -> T2 m a -> f (T2 m b)
          (bound at Bug.hs:38:3)
   |
38 |   traverse' = coerce @(forall f a b. Applicative' f => (a -> f b) ->    m a -> f    (m b))
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Shouldn't it, though? These instance declarations out to be equivalent (morally, at least).

Change History (11)

comment:1 Changed 19 months ago by RyanGlScott

Another example in the same vein:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind

type Phantom1 p = (forall a b. Coercible (p a) (p b) :: Constraint)

class Foo a where
  bar :: Phantom1 proxy => proxy a -> Int

instance Foo Int where
  bar _ = 42

-- Typecheck
newtype Age1 = MkAge1 Int
instance Foo Age1 where
  bar :: forall proxy. Phantom1 proxy => proxy Age1 -> Int
  bar = coerce @(proxy Int  -> Int)
               @(proxy Age1 -> Int)
               bar

-- Doesn't typecheck
newtype Age2 = MkAge2 Int
instance Foo Age2 where
  bar = coerce @(forall proxy. Phantom1 proxy => proxy Int  -> Int)
               @(forall proxy. Phantom1 proxy => proxy Age2 -> Int)
               bar

comment:2 Changed 19 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 19 months ago by RyanGlScott

Here's a simpler version of the original program, if Traversable is too dense:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind

type Representational1 m = (forall a b. Coercible a b => Coercible (m a) (m b) :: Constraint)

class Distributive g where
  distribute :: Representational1 f => f (g a) -> g (f a)

-- Typechecks
newtype T1 g a = MkT1 (g a)
instance Distributive g => Distributive (T1 g) where
  distribute :: forall f a. Representational1 f => f (T1 g a) -> T1 g (f a)
  distribute = coerce @(f    (g a) ->    g (f a))
                      @(f (T1 g a) -> T1 g (f a))
                      distribute

-- Doesn't typecheck
newtype T2 g a = MkT2 (g a)
instance Distributive g => Distributive (T2 g) where
  distribute = coerce @(forall f a. Representational1 f => f    (g a) ->    g (f a))
                      @(forall f a. Representational1 f => f (T2 g a) -> T2 g (f a))
                      distribute

comment:4 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:5 Changed 15 months ago by RyanGlScott

Blocked By: 15290 added

It turns out the original program now panics due to #15290, so that ticket is blocking this one.

comment:6 Changed 15 months ago by RyanGlScott

In light of https://ghc.haskell.org/trac/ghc/ticket/15290#comment:5, perhaps it's best that we not pursue making the impredicative variants typecheck. If we incorporate the change to deriving that Simon suggests in that ticket, then the code that would be generated for the original program would be:

instance Traversable' m => Traversable' (T1 m) where
  traverse' :: forall f a b. (Applicative' f) => (a -> f b) -> T1 m a -> f (T1 m b)
  traverse' = coerce @((a -> f b) -> m a -> f (m b))
                     traverse'

Which, conveniently enough, is pretty much exactly the -- Typechecks variant! So that's convenient.

I'll keep this ticket open since as a reminder to check in these two lovely test cases, but implementing the deriving change in #15290 should make this whole issue moot.

comment:7 Changed 15 months ago by simonpj

implementing the deriving change in #15290 should make this whole issue moot.

Hurrah!

comment:8 Changed 15 months ago by RyanGlScott

Blocked By: 15290 removed

comment:9 Changed 15 months ago by RyanGlScott

Differential Rev(s): Phab:D4895
Status: newpatch

comment:10 Changed 15 months ago by Ryan Scott <ryan.gl.scott@…>

In 132273f3/ghc:

Instantiate GND bindings with an explicit type signature

Summary:
Before, we were using visible type application to apply
impredicative types to `coerce` in
`GeneralizedNewtypeDeriving`-generated bindings. This approach breaks
down when combined with `QuantifiedConstraints` in certain ways,
which #14883 and #15290 provide examples of. See
Note [GND and QuantifiedConstraints] for all the gory details.

To avoid this issue, we instead use an explicit type signature to
instantiate each GND binding, and use that to bind any type variables
that might be bound by a class method's type signature. This reduces
the need to impredicative type applications, and more importantly,
makes the programs from #14883 and #15290 work again.

Test Plan: make test TEST="T15290b T15290c T15290d T14883"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14883, #15290

Differential Revision: https://phabricator.haskell.org/D4895

comment:11 Changed 15 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: patchclosed

As noted in comment:6, #15290 completely obviates the need for a setup like the Traversable' instance for T2, so this issue can be closed.

Note: See TracTickets for help on using tickets.