#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
Cc: | jan.stolarek@… added |
---|
comment:2 Changed 6 years ago by
comment:3 Changed 6 years ago by
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
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
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
@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
.
comment:7 Changed 6 years ago by
@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
Related Tickets: | → #8740 |
---|
comment:9 Changed 4 years ago by
Cc: | jstolarek added; jan.stolarek@… removed |
---|
comment:10 Changed 4 years ago by
Related Tickets: | #8740 → #8740, #11066 |
---|
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
Keywords: | GADTs added |
---|
comment:12 Changed 2 years ago by
Keywords: | deriving added |
---|
comment:13 Changed 18 months ago by
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:15 Changed 18 months ago by
Milestone: | → 8.6.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Test Case: | → deriving/should_compile/T8128 |
This seems impossible to do correctly, in the general case. For example:
The instance generated by the
deriving instance
will depend on the instances forF
that are in scope, which seems quite fragile. In particular, if the instance forEq
were derived out of scope of any instance forF
, then the instance would pattern-match only onB1
. If, later (that is, in another module), we know thatF Bool
isInt
, then it seems we could get a pattern-match failure in theEq
instance.