Opened 19 months ago
Closed 15 months ago
#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
comment:2 Changed 19 months ago by
Cc: | Iceland_jack added |
---|
comment:3 Changed 19 months ago by
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
Keywords: | wipT2893 removed |
---|
comment:5 Changed 15 months ago by
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
Related Tickets: | → #15290 |
---|
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
implementing the deriving change in #15290 should make this whole issue moot.
Hurrah!
comment:8 Changed 15 months ago by
Blocked By: | 15290 removed |
---|
comment:9 Changed 15 months ago by
Differential Rev(s): | → Phab:D4895 |
---|---|
Status: | new → patch |
comment:11 Changed 15 months ago by
Milestone: | → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | patch → closed |
Another example in the same vein: