#8560: undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122 -------------------------------------+------------------------------------ Reporter: carter | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): the error message itself is the "cannot deduce typeable" piece of the following {{{ [1 of 1] Compiling Test ( test.hs, interpreted ) test.hs:33:1: No instance for (Typeable n) arising from the superclasses of an instance declaration In the instance declaration for ‛Data (Shape n a)’ test.hs:33:1: Could not deduce (Typeable r) arising from a use of ‛k’ from the context (Typeable (Shape n a)) bound by the instance declaration at test.hs:33:1-34 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 test.hs:33:1-34 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)’ test.hs:33:1: Could not deduce (n ~ 'Z) from the context (Typeable (Shape n a)) bound by the instance declaration at test.hs:33:1-34 ‛n’ is a rigid type variable bound by the instance declaration at test.hs:33:19 Expected type: Shape n a Actual type: Shape 'Z a Relevant bindings include gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Shape n a) (bound at test.hs:33:1) In the first argument of ‛z’, namely ‛Nil’ In the expression: z Nil 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 test.hs:33:1: Overlapping instances for Typeable (Shape r0 a) arising from a use of ‛k’ Matching givens (or their superclasses): (Typeable (Shape n a)) bound by the instance declaration at test.hs:33:1-34 Matching instances: instance [overlap ok] (Typeable s, Typeable a) => Typeable (s a) -- Defined in ‛Data.Typeable.Internal’ (The choice depends on the instantiation of ‛a, r0’) In the expression: k (k (z (:*))) In a case alternative: _ -> k (k (z (:*))) In the expression: case constrIndex c of { GHC.Types.I# 1# -> z Nil _ -> k (k (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: none. }}} it may be the case that its a spurious piece of the deriving GADT instances problem -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8560#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8560: undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122 -------------------------------------+------------------------------------ Reporter: carter | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): I have not even begun to think what `deriving( Data )` might do for GADTs. At Lennart's request, we did make "standalone deriving" simply generate code, and if it doesn't typecheck it's your problem. See [http://www.haskell.org/ghc/docs/latest/html/users_guide/deriving.html #stand-alone-deriving the manual] (fourth bullet). See #3102, and #3702 for someone who liked it. I'm not sure that was a good decision, especially for jolly complicated classes like `Data`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8560#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8560: undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122 -------------------------------------+------------------------------------- Reporter: carter | 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: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by thomie): * component: Compiler => Compiler (Type checker) Comment: With HEAD the error is now: {{{ $ ghc-7.9.20141115 test.hs ... Could not deduce (Data a) arising from a use of ‘k’ from the context (Typeable (Shape n a)) bound by the instance declaration at test.hs:33:1-34 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 test.hs:33:1-34 Possible fix: add (Data a) to the context of the data constructor ‘:*’ or the type signature for gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Shape n a -> c (Shape n a) or the instance declaration ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8560#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8560: Derive some generic representation for GADTs -------------------------------------+------------------------------------- Reporter: carter | Owner: Type: feature | Status: new request | Milestone: ⊥ Priority: normal | Version: 7.7 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Rocket Science Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * type: bug => feature request -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8560#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8560: Derive some generic representation for GADTs -------------------------------------+------------------------------------- Reporter: carter | Owner: Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Generics Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Generics -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8560#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler