Opened 20 months ago

Last modified 7 months ago

#8560 new feature request

Derive some generic representation for GADTs

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

Description (last modified by goldfire)

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)

EDIT: The request here is really for some generic representation derivable for GADTs. This is a Research Problem, but one that would really help a fair amount of ordinary folk. It won't ever work with Data, as we now know Data, because the types aren't up to the task. But, perhaps some future generic representation will work.

The original description remains unchanged above so that readers can make sense of the comments.

Attachments (2)

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

Download all attachments as: .zip

Change History (11)

Changed 20 months ago by carter

test case

Changed 20 months ago by carter

finger print file

comment:1 Changed 20 months ago by dreixel

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

comment:2 Changed 20 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 20 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 20 months ago by carter (previous) (diff)

comment:4 Changed 19 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 19 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.

comment:6 Changed 8 months ago by thomie

  • Component changed from Compiler to Compiler (Type checker)

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
...

comment:7 Changed 8 months ago by goldfire

  • Description modified (diff)
  • difficulty changed from Unknown to Rocket Science
  • Milestone set to
  • Summary changed from undeducable Typeable error with data kinds when deriving Data for GADT in GHC version 7.7.20131122 to Derive some generic representation for GADTs

comment:8 Changed 8 months ago by goldfire

  • Type changed from bug to feature request

comment:9 Changed 7 months ago by dreixel

I did look into this before (Chapter 10 of my PhD thesis http://dreixel.net/index.php?content=thesis), and there is a reference implementation for the instant-generics package (https://hackage.haskell.org/package/instant-generics). It could be ported to GHC.Generics, but I never found this approach very elegant.

I'm still hoping to be able to look into this again at some point in the future, though.

Note: See TracTickets for help on using tickets.