Opened 5 months ago

Last modified 5 months ago

#8560 new bug

undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122

Reported by: carter Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

This may be an artifact of issue #8128 (see https://ghc.haskell.org/trac/ghc/ticket/8128#comment:5), but I'm seeing examples involving data kinds where Typeable isn't deducible. This could be an artifact of other problems, BUT since with 7.7 onwards, we have baked in polykinded Typeable, things should always "just work™" right?

the error with current head is as follows (and i'm attaching the code + current finger print too)

Attachments (2)

test.hs (853 bytes) - added by carter 5 months ago.
test case
typeable-funny.fingerprint (2.1 KB) - added by carter 5 months ago.
finger print file

Download all attachments as: .zip

Change History (7)

Changed 5 months ago by carter

test case

Changed 5 months ago by carter

finger print file

comment:1 Changed 5 months ago by dreixel

Thanks for the report, I'll have a look.

comment:2 Changed 5 months ago 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

comment:3 Changed 5 months ago by carter

the key bit is that however I add typeable info for the datakind level variant of Nat, i get

test.hs:33:1:
    No instance for (Typeable n)
      arising from the superclasses of an instance declaration
    In the instance declaration for ‛Data (Shape ('S n) a)’

or

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

which *SHOULD* be ok. Again, this may just be an incidental problem due to the fact that in general, (standalone) deriving for GADTs is currently broken / impossible

Last edited 5 months ago by carter (previous) (diff)

comment:4 Changed 5 months ago 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 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.

comment:5 Changed 5 months ago by carter

totally reasonable, and honestly I don't need a Data instance for my use case (and i'm not sure what i'd use it for!),
I just found this to be quite odd and hence worth reporting, because weird corner cases are worth knowing/documenting.

Note: See TracTickets for help on using tickets.