Re: [GHC] #8128: Standalone deriving fails for GADTs due to inaccessible code

22 Nov 2013

      #8128: Standalone deriving fails for GADTs due to inaccessible code
----------------------------------------------+----------------------------
        Reporter:  adamgundry                 |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  normal                     |        Milestone:
       Component:  Compiler (Type checker)    |          Version:  7.7
      Resolution:                             |         Keywords:
Operating System:  Unknown/Multiple           |     Architecture:
 Type of failure:  GHC rejects valid program  |  Unknown/Multiple
       Test Case:                             |       Difficulty:  Unknown
        Blocking:                             |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------

Comment (by carter):

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

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8128#comment:5
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler