[GHC] #8128: Standalone deriving fails for GADTs due to inaccessible code
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- 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`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by monoidal): @carter: Regarding `Typeable 'Z`, you just need to write `deriving instance Typeable 'Z` and likewise for 'N. I don't know what's going on with `Data`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code ----------------------------------------------+---------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: #8740 rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by thomie): * related: => #8740 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #8740 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * cc: jan.stolarek@… (removed) * cc: jstolarek (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #8740, #11066 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * related: #8740 => #8740, #11066 Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Keywords: GADTs, Resolution: | deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #8740, #11066 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: GADTs => GADTs, deriving -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.7 checker) | Keywords: GADTs, Resolution: | deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #8740, #11066 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code
-------------------------------------+-------------------------------------
Reporter: adamgundry | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 7.7
checker) | Keywords: GADTs,
Resolution: | deriving
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: #8740, #11066 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#8128: Standalone deriving fails for GADTs due to inaccessible code -------------------------------------+------------------------------------- Reporter: adamgundry | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 7.7 checker) | Keywords: GADTs, Resolution: fixed | deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T8128 Blocked By: | Blocking: Related Tickets: #8740, #11066 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * testcase: => deriving/should_compile/T8128 * resolution: => fixed * milestone: => 8.6.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8128: Standalone deriving fails for GADTs due to inaccessible code
-------------------------------------+-------------------------------------
Reporter: adamgundry | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 7.7
checker) | Keywords: GADTs,
Resolution: fixed | deriving
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | deriving/should_compile/T8128
Blocked By: | Blocking:
Related Tickets: #8740, #11066 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
participants (1)
-
GHC