Standalone deriving fails for GADTs due to inaccessible code

Consider the following:

{-# LANGUAGE StandaloneDeriving, GADTs, FlexibleInstances #-}

module StandaloneDerivingGADT where

data T a where
  MkT1 :: T Int
  MkT2 :: (Bool -> Bool) -> T Bool

deriving instance Show (T Int)

This gives the error:

StandaloneDerivingGADT.hs:9:1:
    Couldn't match type ‛Int’ with ‛Bool’
    Inaccessible code in
      a pattern with constructor
        MkT2 :: (Bool -> Bool) -> T Bool,
      in an equation for ‛showsPrec’
    In the pattern: MkT2 b1
    In an equation for ‛showsPrec’:
        showsPrec a (MkT2 b1)
          = showParen
              ((a >= 11)) ((.) (showString "MkT2 ") (showsPrec 11 b1))
    When typechecking the code for  ‛showsPrec’
      in a standalone derived instance for ‛Show (T Int)’:
      To see the code I am typechecking, use -ddump-deriv
    In the instance declaration for ‛Show (T Int)’

The derived instance declaration matches on all the constructors, even if they cannot possibly match. It should omit obviously inaccessible constructors so that this example is accepted. For reference, the derived code is:

  instance GHC.Show.Show
             (StandaloneDerivingGADT.T GHC.Types.Int) where
    GHC.Show.showsPrec _ StandaloneDerivingGADT.MkT1
      = GHC.Show.showString "MkT1"
    GHC.Show.showsPrec a_aij (StandaloneDerivingGADT.MkT2 b1_aik)
      = GHC.Show.showParen
          ((a_aij GHC.Classes.>= 11))
          ((GHC.Base..)
             (GHC.Show.showString "MkT2 ") (GHC.Show.showsPrec 11 b1_aik))
    GHC.Show.showList = GHC.Show.showList__ (GHC.Show.showsPrec 0)

The same problem applies to other derivable classes (e.g. Eq).

Trac metadata

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

changed weight to 5

added Tbug Trac import typechecker labels

This seems impossible to do correctly, in the general case. For example:

type family F a

data Bar a where
  B1 :: Bar Int
  B2 :: Bar (F Bool)

deriving instance Eq (Bar Int)

The instance generated by the deriving instance will depend on the instances for F that are in scope, which seems quite fragile. In particular, if the instance for Eq were derived out of scope of any instance for F, then the instance would pattern-match only on B1. If, later (that is, in another module), we know that F Bool is Int, then it seems we could get a pattern-match failure in the Eq instance.

You're right that it is tricky to decide whether a constructor could match in general (see #3927 (closed) and friends). Thus the "inaccessible code" error is necessarily somewhat conservative. But the point of this ticket is to make the standalone deriving machinery line up with the inaccessibility test, not to make the inaccessibility test perfect. In your example, since the match on B2 is not obviously inaccessible, then it should be included; indeed it works in GHC right now.

I had hoped that this would just be a case of testing dataConCannotMatch in the standalone deriving code. But on further investigation, it seems that "inaccessible code" results when the constraint solver deduces an obviously bogus constraint (e.g. Int ~ Bool), which covers more cases than dataConCannotMatch.

Another option presents itself: we could add a flag that means "silently ignore inaccessible code", and check derived instances with the flag set. After all, if a branch in a derived instance is inaccessible, we may as well just throw it away. Such a flag might be useful also in situations where one version of GHC deduces that a match is inaccessible, but another version requires its presence to satisfy the exhaustiveness checker.

As you say, the typechecker takes account of context (ie other in-scope equalities) so it's not a simple, local check. Code generated by deriving is typechecked separately (line 909 of TcRnDriver). So it'd be reasonably easy to suppress "inaccessible code" warnings for generated code.

There is a separate check for overlapping or fully-overlapped patterns at the desugaring stage. This currently does NOT take account of GADTs etc, and there are many open tickets as a result. Re-doing the overlapping-pattern check would be an excellent thing. However, by the time code gets to the the overlap check, we've lost track of which code was generated by deriving. It'd be possible, although a little tiresome, to retain that information.

If someone wants to work on this, I could advise.

Simon

I'm hitting some example GADT code where the "type erasure" of the GADT type would be yield the correct code for the GADT deriving, I'd be interested in helping take a whack at this sometime after december (2013).

I also seem to getting a failure of Typeable on Datakinds! See the end for the Example. That sounds worrisome!

{-# LANGUAGE PolyKinds   #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Numerical.Types.Shape where


data Nat = S !Nat  | Z 
    deriving (Eq,Show,Read,)   

data Shape (rank :: Nat) a where 
    Nil  :: Shape Z a
    (:*) ::  !(a) -> !(Shape r a ) -> Shape  (S r) a
        --deriving (Eq)

--deriving instance Eq a => Eq (Shape Z a)

Interestingly, I can derive a Typeable instance for the Shape data type, but NOT a Data instances

when i do a

data Shape 
  ....
   deriving (Typeable,Data)

I get

Numerical/Types/Shape.hs:57:28:
    Can't make a derived instance of ‛Data (Shape rank a)’:
      Constructor ‛Nil’ must have a Haskell-98 type
      Constructor ‛:*’ must have a Haskell-98 type
      Possible fix: use a standalone deriving declaration instead
    In the data declaration for ‛Shape’
Failed, modules loaded: Numerical.Types.Nat.
*Numerical.Types.Nat> 

when i then follow that suggestion and do a standalone deriving I get

deriving instance  (Data a) =>  Data (Shape n a)

I then get this lovely message

[2 of 2] Compiling Numerical.Types.Shape ( Numerical/Types/Shape.hs, interpreted )

Numerical/Types/Shape.hs:59:1:
    Could not deduce (Typeable n)
      arising from the superclasses of an instance declaration
    from the context (Data a)
      bound by the instance declaration
      at Numerical/Types/Shape.hs:59:1-48
    In the instance declaration for ‛Data (Shape n a)’

Numerical/Types/Shape.hs:59:1:
    Could not deduce (Typeable r) arising from a use of ‛k’
    from the context (Typeable (Shape n a), Data a)
      bound by the instance declaration
      at Numerical/Types/Shape.hs:59:1-48
    or from (n ~ 'S r)
      bound by a pattern with constructor
                 :* :: forall a (r :: Nat). a -> Shape r a -> Shape ('S r) a,
               in an equation for ‛gfoldl’
      at Numerical/Types/Shape.hs:59:1-48
    In the expression: ((z (:*) `k` a1) `k` a2)
    In an equation for ‛gfoldl’:
        gfoldl k z ((:*) a1 a2) = ((z (:*) `k` a1) `k` a2)
    When typechecking the code for  ‛gfoldl’
      in a standalone derived instance for ‛Data (Shape n a)’:
      To see the code I am typechecking, use -ddump-deriv
    In the instance declaration for ‛Data (Shape n a)’

Numerical/Types/Shape.hs:59:1:
    Couldn't match type ‛'Z’ with ‛'S r0’
    Expected type: a -> Shape r0 a -> Shape n a
      Actual type: a -> Shape r0 a -> Shape ('S r0) a
    In the first argument of ‛z’, namely ‛(:*)’
    In the first argument of ‛k’, namely ‛z (:*)’
    When typechecking the code for  ‛gunfold’
      in a standalone derived instance for ‛Data (Shape n a)’:
      To see the code I am typechecking, use -ddump-deriv
Failed, modules loaded: Numerical.Types.Nat.

I then tried the following to keep it simple

deriving instance (Data a)=> Data (Shape Z a) 

and got

2 of 2] Compiling Numerical.Types.Shape ( Numerical/Types/Shape.hs, interpreted )

Numerical/Types/Shape.hs:60:1:
    Could not deduce (Typeable 'Z)
      arising from the superclasses of an instance declaration
    from the context (Data a)
      bound by the instance declaration
      at Numerical/Types/Shape.hs:60:1-45
    In the instance declaration for ‛Data (Shape 'Z a)’

Numerical/Types/Shape.hs:60:1:
    Couldn't match type ‛'Z’ with ‛'S r’
    Inaccessible code in
      a pattern with constructor
        :* :: forall a (r :: Nat). a -> Shape r a -> Shape ('S r) a,
      in an equation for ‛gfoldl’
    In the pattern: (:*) a1 a2
    In an equation for ‛gfoldl’:
        gfoldl k z ((:*) a1 a2) = ((z (:*) `k` a1) `k` a2)
    When typechecking the code for  ‛gfoldl’
      in a standalone derived instance for ‛Data (Shape 'Z a)’:
      To see the code I am typechecking, use -ddump-deriv
    In the instance declaration for ‛Data (Shape 'Z a)’

Numerical/Types/Shape.hs:60:1:
    Couldn't match type ‛'S r0’ with ‛'Z’
    Expected type: a -> Shape r0 a -> Shape 'Z a
      Actual type: a -> Shape r0 a -> Shape ('S r0) a
    In the first argument of ‛z’, namely ‛(:*)’
    In the first argument of ‛k’, namely ‛z (:*)’
    When typechecking the code for  ‛gunfold’
      in a standalone derived instance for ‛Data (Shape 'Z a)’:
      To see the code I am typechecking, use -ddump-deriv

Numerical/Types/Shape.hs:60:1:
    Couldn't match type ‛'Z’ with ‛'S r’
    Inaccessible code in
      a pattern with constructor
        :* :: forall a (r :: Nat). a -> Shape r a -> Shape ('S r) a,
      in an equation for ‛toConstr’
    In the pattern: (:*) _ _
    In an equation for ‛toConstr’:
        toConstr ((:*) _ _) = (Numerical.Types.Shape.$c:*)
    When typechecking the code for  ‛toConstr’
      in a standalone derived instance for ‛Data (Shape 'Z a)’:
      To see the code I am typechecking, use -ddump-deriv
    In the instance declaration for ‛Data (Shape 'Z a)’
Failed, modules loaded: Numerical.Types.Nat.

The Typeable 'Z thing is a bit odd! This is on a recent copy of head, built in the past month...

mentioned in issue #8560

@carter: Regarding Typeable 'Z, you just need to write deriving instance Typeable 'Z and likewise for 'S. I don't know what's going on with Data.

@monoidal, yup. That works out fine. Though see #8560#ticket:8128#comment:73082 for a possibly related issue. (though it may just be a spurious artifact of this one, not sure)

mentioned in issue #8740 (closed)

Trac metadata

Trac field	Value
Related	→ #8740 (closed)

Trac metadata

Trac field	Value
CC	jan.stolarek@p.lodz.pl → jstolarek

mentioned in issue #11066 (closed)

I think the right way to fix this is to make inaccessible code errors into warnings (per #11066 (closed)). We could then optionally suppress them if they arise from generated code.

Trac metadata

Trac field	Value
Related	#8740 (closed) → #8740 (closed), #11066 (closed)

added GADTs label

mentioned in issue #12466 (closed)

added deriving label and removed GADTs label

Now that inaccessible code is a warning instead of an error (see #11066 (closed)), the original program now typechecks. I'll whip up a test case.

mentioned in commit 90e99c4c

closed

changed milestone to %8.6.1

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → deriving/should_compile/T8128

mentioned in issue #15398 (closed)

mentioned in commit 44a7b9ba

added Pnormal label

mentioned in issue #18474 (closed)