Deriving a class via an instance that has a TypeError constraint using standalone deriving fails during compilation.

This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving. This is the shortest example I was able to come up with:

{-# Language DataKinds, UndecidableInstances, StandaloneDeriving, DerivingVia #-}  

import GHC.TypeLits

newtype NotNum a = NotNum a

instance (TypeError (Text "Not a num")) => Num (NotNum a) where

data Foo = Foo
deriving via (NotNum Foo) instance Num Foo

In this case, it'll fail in compilation with 'Not a Num'.

This only seems to happen when combining deriving via with standalone deriving, because if I derive the class like:

data Foo = Foo deriving Num via (NotNum Foo)

It works as expected (doesn't fail with my custom error until I actually try to use a Foo where I should use a Num)

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

Trac metadata

Trac field	Value
TypeOfFailure	OtherFailure → ValidProgramRejected

data Foo = Foo deriving Num via (NotNum Foo) is generating a slightly different instance than you think it is:

$ /opt/ghc/8.6.3/bin/ghci Bug.hs -ddump-deriv
GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

==================== Derived instances ====================
Derived class instances:
  instance (TypeError ...) => GHC.Num.Num Main.Foo where

GHC treats TypeError constraints as insoluble, so they're inferred to be a part of the instance context. A standalone deriving via (NotNum Foo) instance Num Foo declaration, on the other hand, asserts that there is no instance context, so GHC tries to solve for the residual TypeError constraint that is inferred during typechecking. This leads to the compile-time exception you see in the original program.

Note that if you write this:

deriving via (NotNum Foo) instance TypeError (Text "Not a num") => Num Foo

Or even this:

{-# LANGUAGE PartialTypeSignatures #-}

deriving via (NotNum Foo) instance _ => Num Foo

Then you won't get an exception during compile-time.

Thanks for the prompt response and for the explanation!.

So, is it expected behavior or an unintended consequence of how TypeError is treated?

I don't think I'm qualified to say. I've never been clear on what exactly the semantics of TypeError actually //intended// to be, so it's anyone's guess as to whether this is a bug or a feature.

Adding Iavor who is the key person on TypeError.

See also Proposal/CustomTypeErrors

If I understand what's going on here, the custom type errors work as intended.

I think of using TypeError in the context of an instance declaration as saying "this instance does not exist". I think it would be nicer to have an actual language construct to say that, but for the time being TypeError is convenient "hack" that achieves a similar result.

So, the standalone instance in the original example has to derive and instance for Num Foo by using the non-existing instance for NotNum Foo. As a result GHC reports that it can't do that, using the custom type error provided. I think that this makes sense.

OTOH, if you write the alternative that Ryan wrote:

deriving via (NotNum Foo) instance TypeError (Text "Not a num") => Num Foo

you are really saying that there is no instance for Num Foo and for the exact same reason that there is no instance for NotNum Foo. Deriving a non-existing instance seems like a bit of an odd thing to do though, as there is nothing to derive...

I guess it makes sense if you are trying to report a class of errors in the same way, but you could get the same by just writing the instance without deriving:

instance Num (NotNum Foo) => Num Foo

closed

Alright. Since Iavor seems convinced that this is expected behavior, I'm going to close this.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added custom type errors label

added Pnormal label