Re: [GHC] #8560: undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122

23 Nov 2013

      #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