Opened 2 years ago

Last modified 2 years ago

#13731 infoneeded bug

DeriveFunctor and friends don't understand type families

Reported by: spacekitteh Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1-rc2
Keywords: deriving 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

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}

data Test ext a where
  Foo :: a -> Test ext a
  Extend :: (ExtensionType ext a) -> Test ext a

type family ExtensionType ext a
data ListExtension
type instance ExtensionType ListExtension a = [a]

deriving instance Functor (Test ListExtension)

{-

a.hs:15:1: error:
    • Can't make a derived instance of ‘Functor (Test ListExtension)’:
        Constructor ‘Extend’ must use the type variable only as the last argument of a data type
    • In the stand-alone deriving instance for
        ‘Functor (Test ListExtension)’
   |
15 | deriving instance Functor (Test ListExtension)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, modules loaded: none.
-}

Change History (10)

comment:1 Changed 2 years ago by simonpj

The error message is terrible. (Ryan might you look at that?)

But the program IS wrong. In Haskell you can't write

f (xs ++ ys) = ...

which pattern-matches on a function call. And similarly at the type level you can't pattern match on a function call, as in instance Functor (Test ListExtension).

Instead write instance Functor []. Oh! We have that instance already; so you can just omit it!

comment:2 Changed 2 years ago by RyanGlScott

What would you rather the error message say? I do think the phrase "the type variable" is unfortunate, as it should rather be "the last type variable" (since there can be more than one). But other than that, it's pretty spot-on: if you're using the last type variable within another type, it must be a data type, and ExtensionType is not a data type.

comment:3 Changed 2 years ago by Iceland_jack

That instance becomes writable if we mark ExtensionType injective

{-# Language TypeFamilyDependencies, InstanceSigs #-} -- ...

data Test :: Type -> Type -> Type where
  Foo    :: a -> Test ext a
  Extend :: ExtensionType ext a -> Test ext a

type family ExtensionType a = (res :: Type -> Type)  | res -> a
data ListExtension
type instance ExtensionType ListExtension = []

instance Functor (ExtensionType ext) => Functor (Test ext) where
  fmap :: (a -> a') -> (Test ext a -> Test ext a')
  fmap f = \case
    Foo    a  -> Foo (f a)
    Extend ex -> Extend (fmap f ex)

We need to bump the arity of ExtensionType down to one, given that we don't have #10832.

No idea if it's sensible for GHC to generate but it would be nice

Last edited 2 years ago by Iceland_jack (previous) (diff)

comment:4 Changed 2 years ago by simonpj

Oh my mistake. I thought instance Functor (Test ListExtension) involved a type family; but it doesn't. Neither Test nor ListExtension is a type family. My mistake.

Then indeed the error message makes more sense. But not total sense. If you reduce the arity of ExtensionType1 the deriving` clause works fine (as it should)

type family ExtensionType ext :: * -> *
type instance ExtensionType ListExtension  = []

So it's not that it must be a data type; it can be a saturated type-family application.

But I now think this is a non-bug; deriving is working right, and reducing the arity of ExtensionType is the right solution.

But

comment:5 Changed 2 years ago by RyanGlScott

So it's not that it must be a data type; it can be a saturated type-family application.

Am I missing something? In the original example, the type family instance is:

type instance ExtensionType ListExtension a = [a]

And the instance we're deriving is:

deriving instance Functor (Test ListExtension)

In other words, the field of Extend will have type ExtensionType ListExtension a. This is a fully saturated type family application, right? So surely the rule you've proposed doesn't quite capture the essence of this problem.

comment:6 in reply to:  4 Changed 2 years ago by Iceland_jack

Replying to simonpj:

If you reduce the arity of ExtensionType1 the deriving` clause works fine (as it should)

Ah, nothing to do with injective type families

comment:7 Changed 2 years ago by simonpj

Consider the instance we want:

instance Functor (Test ListExtension) where
  fmap f (Extend x) = Extend (fmap f x)

Am I missing something?

From the inner fmap we get [W] Functor (ExtensionType ListExtension). If ExtensionType has arity 2, that would be an un-saturated type family. But if it has arity 1 it is saturated, and reduces to [], so all is well.

... the field of Extend will have type ExtensionType ListExtension a. This is a fully saturated type family application

Yes, it's saturated in the field, but the use of fmap requires us to decompose the type application, we it must be decomposable. It's only decomposable if ExtensionType has arity 1.

comment:8 in reply to:  7 Changed 2 years ago by RyanGlScott

Replying to simonpj:

Yes, it's saturated in the field, but the use of fmap requires us to decompose the type application, we it must be decomposable. It's only decomposable if ExtensionType has arity 1.

Thank you, this is the part that I wasn't understanding.

So would you be happy with this error message?

    • Can't make a derived instance of ‘Functor (Test ListExtension)’:
        Constructor ‘Extend’ must use the last type variable only as
        the last argument of a data type or a saturated type family

comment:9 Changed 2 years ago by simonpj

You should ask users not me! But looking at

  Extend :: ExtensionType ext a -> Test ext a

a user might say that ExtentionType ext a does use a as the last arg of a saturated type-family application, namely ExtensionType ext a!

An what is "the last type variable"?

Guessing wildly, what about

Illegal use of type variable 'a' in the first argument of `Extend`.
Such uses must be of form `ty a` where `ty` is a data type or
saturated type family application.

I'm not sure if that's better...

comment:10 Changed 2 years ago by RyanGlScott

Keywords: deriving added
Status: newinfoneeded

Requesting feedback from spacekitteh on what is expected here.

Note: See TracTickets for help on using tickets.