Opened 6 years ago

Closed 16 months ago

Last modified 14 months ago

#8128 closed bug (fixed)

Standalone deriving fails for GADTs due to inaccessible code

Reported by: adamgundry Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 7.7
Keywords: GADTs, deriving Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: deriving/should_compile/T8128
Blocked By: Blocking:
Related Tickets: #8740, #11066 Differential Rev(s):
Wiki Page:

Description

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).

Change History (16)

comment:1 Changed 6 years ago by jstolarek

Cc: jan.stolarek@… added

comment:2 Changed 6 years ago by goldfire

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.

comment:3 Changed 6 years ago by adamgundry

You're right that it is tricky to decide whether a constructor could match in general (see #3927 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.

comment:4 Changed 6 years ago by simonpj

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

comment:5 Changed 6 years ago by carter

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...

comment:6 Changed 6 years ago by monoidal

@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.

Last edited 6 years ago by monoidal (previous) (diff)

comment:7 Changed 6 years ago by carter

@monoidal, yup. That works out fine. Though see https://ghc.haskell.org/trac/ghc/ticket/8560#comment:3 for a possibly related issue. (though it may just be a spurious artifact of this one, not sure)

comment:8 Changed 5 years ago by thomie

comment:9 Changed 4 years ago by jstolarek

Cc: jstolarek added; jan.stolarek@… removed

comment:10 Changed 4 years ago by adamgundry

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

comment:11 Changed 4 years ago by thomie

Keywords: GADTs added

comment:12 Changed 2 years ago by RyanGlScott

Keywords: deriving added

comment:13 Changed 16 months ago by RyanGlScott

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

comment:14 Changed 16 months ago by Ryan Scott <ryan.gl.scott@…>

In 90e99c4c/ghc:

Add tests for #8128 and #8740

Commit 08073e16cf672d8009309e4e55d4566af1ecaff4 (#11066) ended up
fixing these, fortunately enough.

comment:15 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: deriving/should_compile/T8128

comment:16 Changed 14 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 44a7b9b/ghc:

Suppress -Winaccessible-code in derived code

Summary:
It's rather unfortunate that derived code can produce inaccessible
code warnings (as demonstrated in #8128, #8740, and #15398), since
the programmer has no control over the generated code. This patch
aims to suppress `-Winaccessible-code` in all derived code. It
accomplishes this by doing the following:

* Generalize the `ic_env :: TcLclEnv` field of `Implication` to
  be of type `Env TcGblEnc TcLclEnv` instead. This way, it also
  captures `DynFlags`, which record the flag state at the time
  the `Implication` was created.
* When typechecking derived code, turn off `-Winaccessible-code`.
  This way, any insoluble given `Implication`s that are created when
  typechecking this derived code will remember that
  `-Winaccessible-code` was disabled.
* During error reporting, consult the `DynFlags` of an
  `Implication` before making the decision to report an inaccessible
  code warning.

Test Plan: make test TEST="T8128 T8740 T15398"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: monoidal, rwbarton, thomie, carter

GHC Trac Issues: #8128, #8740, #15398

Differential Revision: https://phabricator.haskell.org/D4993
Note: See TracTickets for help on using tickets.