Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,252
    • Issues 5,252
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 562
    • Merge requests 562
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14883
Closed
Open
Issue created Mar 03, 2018 by Ryan Scott@RyanGlScottMaintainer

QuantifiedConstraints don't kick in when used in TypeApplications

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

Trac metadata
Trac field Value
Version 8.5
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking