Opened 8 months ago

Closed 8 months ago

Last modified 8 months ago

#16194 closed bug (wontfix)

deriving, wrong code: newtype T cat a = MkT ((forall xx. cat xx xx) -> a) deriving stock Functor

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.7
Keywords: DeriveFunctor deriving RankNTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This fails (deriving stock Functor) (data type comes from Applicative Archery)

$ ./ghc-stage2 --interactive -ignore-dot-ghci
GHCi, version 8.7.20181230: https://www.haskell.org/ghc/  :? for help
Prelude> :set prompt "> "
> :set -XRankNTypes -XDeriveFunctor -ddump-deriv
> :set -dsuppress-idinfo -dsuppress-coercions -dsuppress-type-applications -dsuppress-uniques -dsuppress-module-prefixes
> newtype T cat a = MkT ((forall xx. cat xx xx) -> a) deriving Functor

==================== Derived instances ====================
Derived class instances:
  instance Functor (T cat) where
    fmap f (MkT a1) = MkT ((\ b2 b3 -> f (b2 ((\ b1 -> b1) b3))) a1)
    (<$) z (MkT a1)
      = MkT ((\ b3 b4 -> (\ b2 -> z) (b3 ((\ b1 -> b1) b4))) a1)


Derived type family instances:



<interactive>:4:62: error:
    • Couldn't match type ‘forall xx. cat xx xx’ with ‘cat xx0 xx0’
      Expected type: cat xx0 xx0 -> a
        Actual type: (forall xx. cat xx xx) -> a
    • In the first argument of ‘\ b2 b3
                                  -> f (b2 ((\ b1 -> b1) b3))’, namely
        ‘a1’
      In the first argument of ‘MkT’, namely
        ‘((\ b2 b3 -> f (b2 ((\ b1 -> b1) b3))) a1)’
      In the expression: MkT ((\ b2 b3 -> f (b2 ((\ b1 -> b1) b3))) a1)
      When typechecking the code for ‘fmap’
        in a derived instance for ‘Functor (T cat)’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        a1 :: (forall xx. cat xx xx) -> a (bound at <interactive>:4:62)
        fmap :: (a -> b) -> T cat a -> T cat b
          (bound at <interactive>:4:62)

<interactive>:4:62: error:
    • Couldn't match type ‘forall xx. cat xx xx’ with ‘cat xx1 xx1’
      Expected type: cat xx1 xx1 -> b
        Actual type: (forall xx. cat xx xx) -> b
    • In the first argument of ‘\ b3 b4
                                  -> (\ b2 -> z) (b3 ((\ b1 -> b1) b4))’, namely
        ‘a1’
      In the first argument of ‘MkT’, namely
        ‘((\ b3 b4 -> (\ b2 -> z) (b3 ((\ b1 -> b1) b4))) a1)’
      In the expression:
        MkT ((\ b3 b4 -> (\ b2 -> z) (b3 ((\ b1 -> b1) b4))) a1)
      When typechecking the code for ‘<$’
        in a derived instance for ‘Functor (T cat)’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        a1 :: (forall xx. cat xx xx) -> b (bound at <interactive>:4:62)
        (<$) :: a -> T cat b -> T cat a (bound at <interactive>:4:62)
>

Generates odd code

fmap .. = MkT ((\ b2 b3 -> f (b2 ((\ b1 -> b1) b3))) a1)

It works fine (in HEAD) to deriving newtype Functor (it didn't in 8.2 where I checked)

Change History (5)

comment:1 Changed 8 months ago by Iceland_jack

Fortunately -XDerivingVia handles it

> newtype T cat a = MkT ((forall xx. cat xx xx) -> a) deriving Functor via ((->) (forall xx. cat xx xx))

==================== Derived instances ====================
Derived class instances:
  instance Functor (T cat) where
    fmap
      = coerce
          @((a -> b)
            -> ((forall (xx :: TYPE LiftedRep). cat xx xx) -> a)
               -> (forall (xx :: TYPE LiftedRep). cat xx xx) -> b)
          @((a -> b) -> T cat a -> T cat b)
          (fmap
             @((->) (forall (xx :: TYPE LiftedRep). cat xx xx) :: TYPE LiftedRep
                                                                  -> TYPE LiftedRep)) ::
          forall (a :: TYPE LiftedRep) (b :: TYPE LiftedRep).
          (a -> b) -> T cat a -> T cat b
    (<$)
      = coerce
          @(a
            -> ((forall (xx :: TYPE LiftedRep). cat xx xx) -> b)
               -> (forall (xx :: TYPE LiftedRep). cat xx xx) -> a)
          @(a -> T cat b -> T cat a)
          ((<$)
             @((->) (forall (xx :: TYPE LiftedRep). cat xx xx) :: TYPE LiftedRep
                                                                  -> TYPE LiftedRep)) ::
          forall (a :: TYPE LiftedRep) (b :: TYPE LiftedRep).
          a -> T cat b -> T cat a


Derived type family instances:

comment:2 Changed 8 months ago by RyanGlScott

This is rather delicate. Here is the instance you likely have in your head:

instance Functor (T cat) where
  fmap f (MkT g) = MkT (\x -> f (g x))

As -ddump-deriv reveals, this isn't quite the code that GHC is producing. It's actually producing this:

instance Functor (T cat) where
  fmap f (MkT g) = MkT ((\g' x -> f (g' x)) g)

Normally, these two implementations would be equivalent. However, because g has a higher-rank type forall xx. cat xx xx, applying (\g' x -> f (g' x)) to g causes its type to be instantiated with a skolem xx0. This is why you get this error message:

Couldn't match type ‘forall xx. cat xx xx’ with ‘cat xx0 xx0’

There are advantages to generating code similar to the second instance. In more complicated examples (e.g., newtype T a = MkT (Int -> Int -> a)), using the unapplied form allows for a more compositional code-generation strategy that doesn't have to reason about substituting in arguments.

In short, could this be fixed? Theoretically speaking, yes, but it would require a lot of work for not much gain. Personally, I'm inclined to just require users to write out this particular instance by hand.

comment:3 Changed 8 months ago by Iceland_jack

That's fine, newtype works and it's a contrived example. I agree the gain isn't worth it

comment:4 Changed 8 months ago by RyanGlScott

Resolution: wontfix
Status: newclosed

comment:5 Changed 8 months ago by Iceland_jack

Thought: The second representation (g & \g' -> f (g' x)) can maybe be captured as a newtype with an instance (like DList changes the representation of [a] to Endo [a]). GHC would generate the newtype form, the instance takes care of the operation and coerce back.

edit We can represent one :: a -> b' as (one .) aka `liftYoneda one :: Yoneda ((-> a) b`

newtype One a b = One (a -> b)

instance Functor (One a) where
 fmap :: (b -> b') -> (One a b -> One a b')
 fmap f (One one) | let
  x = liftYoneda one :: Yoneda ((->) a) b
  y = fmap f x       :: Yoneda ((->) a) b'
  z = lowerYoneda y  :: (a -> b')
    = One z          :: One a b'

may be useful, anyway

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