#15052 closed bug (invalid)

DeriveAnyClass instances may skip TypeError constraints

Reported by: jcpetruzza Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.2.2
Keywords: CustomTypeErrors 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

In the presence of TypeError, one can derive instances with DeriveAnyClass that would be rejected otherwise. A simplistic example would be:

{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T

where

import GHC.TypeLits(TypeError, ErrorMessage(..))


class TypeError ('Text "BOOM") => C a where
    f :: a -> ()
    f _ = ()


data T = T
  deriving(C)

Of course, any attempt to use the instance leads to a type-error. However, the instance is rejected right away using a normal instance declaration or StandaloneDeriving.

While this is a toy example, it can actually happen when using Generics and default-signatures, where one would puts a TypeError in an instance head for one of the Generics constructors to give a better error message.

Change History (14)

comment:1 Changed 17 months ago by RyanGlScott

You say that the equivalent instance is "rejected right away using a normal instance declaration or StandaloneDeriving", but I can't reproduce this behavior. In fact, these three equivalent instances all typecheck:

{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T where

import GHC.TypeLits(TypeError, ErrorMessage(..))

class TypeError ('Text "BOOM") => C a where
    f :: a -> ()
    f _ = ()

data T1 = T1
   deriving C

data T2 = T2
instance TypeError ('Text "BOOM") => C T2

data T3 = T3
deriving instance TypeError ('Text "BOOM") => C T3

Am I missing something here?

comment:2 Changed 17 months ago by jcpetruzza

Sorry that I wasn't clear. I meant, using instance and deriving instance without providing the instance head.

{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T where

import GHC.TypeLits(TypeError, ErrorMessage(..))

class TypeError ('Text "BOOM") => C a where
    f :: a -> ()
    f _ = ()

data T1 = T1
   deriving C

data T2 = T2
instance C T2 -- won't typecheck

data T3 = T3
deriving instance C T3 -- won't typecheck

comment:3 Changed 17 months ago by RyanGlScott

Right—that's because what you've written isn't equivalent to what deriving C will give you. deriving C gives you:

instance TypeError ('Text "BOOM") => C T

So I'm quite unclear on what the "bug" is here.

comment:4 Changed 17 months ago by jcpetruzza

Fair enough. I tried to produce a simplified example of the behaviour I'm seeing and went too far. I will add a more relastic example.

comment:5 Changed 17 months ago by jcpetruzza

Ok, here is a better example. Class C should have a default implementation for every generic type that is not a sum. Instead of omitting the instance for :+:, I use a TypeError in the head of the instance for :+: to provide a more clear error message.

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveGeneric        #-}
{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TypeOperators        #-}
module T where

import GHC.TypeLits(TypeError, ErrorMessage(..))

import qualified GHC.Generics as Gen

class C a where
    f :: a -> ()

    default f :: (Gen.Generic a, GC (Gen.Rep a)) => a -> ()
    f =  gf . Gen.from


class GC b where
    gf :: b x -> ()

instance GC x => GC (Gen.M1 i c x) where
    gf (Gen.M1 x) = gf x

instance GC Gen.V1 where
    gf _ = ()

instance GC Gen.U1 where
    gf _ = ()

instance GC (Gen.K1 i t) where
    gf _ = ()

instance  GC (l Gen.:*: r) where
    gf _ = ()

instance TypeError ('Text "Can't derive C for sums") => GC (l Gen.:+: r) where
    gf _ = error "unreachable"


data TV              deriving (Gen.Generic, C)
data TU = TU         deriving (Gen.Generic, C)
data TK = TK Int     deriving (Gen.Generic, C)
data TP = TP Int Int deriving (Gen.Generic, C)

data TS = TSL | TSR  deriving (Gen.Generic, C) -- should reject right away

This program is accepted, but any attempt to use the instance will fail at compile time. I find this surprising and less useful than rejecting the program right away.

If one instead uses one of:

instance C TS
-- or
deriving instance C TS

the program is rejected (with the intended error message).

comment:6 Changed 17 months ago by RyanGlScott

Keywords: CustomTypeErrors added

Ah. You're arguing something different, then. You're proposing that if you have a type class instance with TypeError in the context (such as the three instances in comment:1), then GHC should reject that instance itself, instead of rejecting uses of that instance.

This would be a pretty big breaking change. There is a lot of code out there which relies on the ability to use TypeError constraints in instance contexts. (For examples see the T14339 test case.) I think if you want to see this behavior be enshrined into GHC, you should first submit a proposal to the GHC proposals repo, and argue why this behavior is more desirable over the status quo.

comment:7 Changed 17 months ago by jcpetruzza

I'm not sure I see why this would be a breaking change. In this last example (which is the important one, the original was an oversimplification, we can disregard it), why would these two be any different:

data TS = TSL | TSR  deriving (Gen.Generic, C)

vs

data TS = TSL | TSR  deriving (Gen.Generic)
instance C TS

The latter fails, IIUC, because we are trying to see if the default signature of f in C applies to TS, and this forces the reduction of GC (Rep TS), that eventually leads to the TypeError. This is the standard behaviour.

Am I mistaken in thinking that these two declarations should be equivalent?

comment:8 Changed 17 months ago by RyanGlScott

Here is the difference between these two programs. In the first one:

data TS = TSL | TSR  deriving (Gen.Generic, C)

You are requesting that GHC come up with the ??? in the following instance:

instance ??? => C TS

Because C has a superclass constraint, TypeError (...), it infers that for ???. If you had picked different superclass constraints for C, such as class (Eq a, Show a) => C a, then GHC would have inferred (Eq a, Show a) for ???.

In the second example, you are putting the task of coming up with the context in your own hands. You have boldly declared that the instance context should be ()! As a result, GHC tries to unify TypeError (...) with (), which causes the type error to trigger. Boom.

comment:9 Changed 17 months ago by jcpetruzza

Let's forget about the program in comment:1, I understand what GHC is doing there and I agree it is the expected behaviour. :)

The issue is only shown in the program of comment:5. In this program C has an empty context, so writing

data TS = TSL | TSR  deriving (Gen.Generic, C)

and writing

data TS = TSL | TSR  deriving (Gen.Generic)
instance C TS

should have the same result, but it doesn't. The first form is accepted, the second one is rejected (as expected).

comment:10 Changed 17 months ago by RyanGlScott

When deriving infers an instance context, it collects some set of constraints, simplifies them as much as possible (discharging constraints when possible), and uses the remaining constraints as the context.

For instance, in data T a = MkT a Int deriving Show, you start with the constraint set (Show a, Show Int). GHC is able to discharge the Show Int constraint, since there's a top-level instance for that, but not the Show a constraint, so the final instance context is Show a.

Returning to your TypeError example, you start with a constraint set that contains many constraints, with TypeError (...) sprinkled among them. There is no way to discharge a TypeError (...) constraint—if you could, you would be able to do lots of things you weren't supposed to be able to do, since TypeError is designed to be the context for unreachable code! Thus, TypeError (...) ends up in the final instance context.

At this point, you might be thinking "well why doesn't the constraint solver immediately error when it encounters any constraint mentioning TypeError"? That might be feasible, but again, it would be a breaking change—it would explicitly go against the convention established by #14339.

comment:11 Changed 17 months ago by jcpetruzza

I don't disagree with anything you are saying.

The issue is that deriving is behaving differently from instance and from deriving instance. Consider this hopefully more clear example:

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}
module T2 where

import Data.Kind(Constraint)
import GHC.TypeLits(TypeError, ErrorMessage(..))

class D a where
  f :: a

  default f :: DeferError a  => a
  f = error "unreachable"


type family DeferError a :: Constraint where
    DeferError a = TypeError ('Text "Boom")


data X
  deriving D             -- < -- ACCEPTED

data Y
instance D Y             -- < -- REJECTED

data Z
deriving instance D Z    -- < -- REJECTED

Do you aggree that either the three instances should be accepted here or the three instances should be rejected?

comment:12 Changed 17 months ago by RyanGlScott

You've only presented me with the options that all three should be accepted, or all three should be rejected. I don't agree with either of those options. I think that, given the current established conventions for how TypeError works, the first option should be accepted, and the latter two options should be rejected. The first option is working in a fundamentally different way than the latter two, so it's foolhardy to try and equate them.

I think there might be a different semantics for TypeError which would reject the first option. But I'd like to put an emphasis on "different".

comment:13 Changed 17 months ago by jcpetruzza

Ok, I think I understand your point: what we see follows from the documented behaviour for DerivingAnyClass so there is really no bug here.

Tbh, I hadn't noticed until right now that deriving would propagate constraints coming from the default signatures! The initial example in the docs says:

 data Foo = Foo deriving (Show, SPretty)

The above code is equivalent to:

data Foo = Foo deriving Show
instance SPretty Foo

and somehow the idea that deriving would declare the instance over an empty context got stuck in my head for a long time. Hence my insistance in expecting the results to be the same! (maybe Foo a would make for a better example there?)

In any case, I agree that deriving is doing the right thing here. It is a bit unfortunate since I'm not sure I want to use TypeError as it is for generic default methods then, but on the other hand, without it error messages can be a screenful!

comment:14 Changed 17 months ago by jcpetruzza

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.