Standalone deriving for GADTs should avoid impossible cases

changed weight to 5

added Tbug Trac import labels

I suspect this would not be too hard. See DataCon.dataConCannotMatch and its call sites.

added Pnormal label

added GADTs deriving labels

marked #18474 (closed) as a duplicate of this issue

marked this issue as related to #18474 (closed)

mentioned in issue #18474 (closed)

Another example from #18474 (closed):

data SumType (types :: [Type]) where
  Here  :: forall x xs. x          -> SumType (x ': xs)
  There :: forall x xs. SumType xs -> SumType (x ': xs)

deriving instance Eq (SumType '[])

Ideally, this would simply generate:

instance Eq (SumType '[]) where
  _ == _ = True

Currently, however, it generates the following instance with unreachable cases:

instance Eq (SumType '[]) where
  (==) (Here a) (Here b) = a == b
  (==) (There a) (There b) = a == b
  (==) _ _ = False

    • Could not deduce: xs1 ~ xs
      from the context: '[] ~ (x : xs)
        bound by a pattern with constructor:
                   There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
                 in an equation for ‘==’
      or from: '[] ~ (x1 : xs1)
        bound by a pattern with constructor:
                   There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
                 in an equation for ‘==’
      ‘xs1’ is a rigid type variable bound by
        a pattern with constructor:
          There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
        in an equation for ‘==’
      ‘xs’ is a rigid type variable bound by
        a pattern with constructor:
          There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
        in an equation for ‘==’
      Expected type: SumType xs
        Actual type: SumType xs1
    • In the second argument of ‘(==)’, namely ‘b1’
      In the expression: ((a1 == b1))
      In an equation for ‘==’: (==) (There a1) (There b1) = ((a1 == b1))
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (SumType '[])’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        b1 :: SumType xs1
        a1 :: SumType xs
   |
70 | deriving instance Eq (SumType '[])
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

mentioned in commit 4389315e

mentioned in commit 1e9cde15

I added a test here. Is my reasoning correct here? Namely, when deriving instances for Foo Int,

data Foo a where
  X :: Foo Int
  Y :: ... -> Foo Bool

should behave exactly the same as

data Foo a where
  X :: Foo Int

I started a thing in fd5e1083. Is that on the right track? I'm currently getting zipEqual: unequal lists: zipTyEnv errors, where univ_tvs and univ_tys are different lengths in dataConInstSig, but I'm not sure what to do next:

-- Printing out these values in `dataConInstSig`:
-- (con, univ_tvs, ex_tvs, arg_tys, univ_tys)

(UWord, [k, p], [], [Word#], [k, Word, p])

I believe this is happening when compiling GHC.Generics, line 1085

Other miscellaneous questions:

Is it correct in needing inst_tys to be passed to each gen_*_binds function manually, or is there a more high level place we can put the filter?
Is this only applicable for stock-derived instances? Related to the previous point, can we do this filtering more automatically for non-stock derived instances also?
Any tips on implementing this for Ix?

mentioned in commit c8017b36

mentioned in commit 41c5d721

mentioned in commit 130146ce

mentioned in commit d9da1e86

mentioned in commit fd5e1083

Thanks for working on this!

Is it correct in needing inst_tys to be passed to each gen_*_binds function manually, or is there a more high level place we can put the filter?

You'll certainly need to use inst_tys, yes. Luckily, the infrastructure for passing inst_tys to each gen_*_binds is already in place. See the hasStockDeriving function, which currently throws away the inst_tys whenever most gen_*_binds are used. For an example of a place where hasStockDeriving does use inst_tys, see gen_Generic_binds.

I'm currently getting zipEqual: unequal lists: zipTyEnv errors

I don't know off the top of my head why that might happen, but I think the way you're obtaining inst_tys (by way of splitTyConApp_maybe) is slightly wrong. See if the errors persist if you propagate inst_tys from hasStockDeriving.

Is this only applicable for stock-derived instances?

Unless I'm overlooking something, yes. Only stock-derived instance would ever match directly on data constructors, so that would be the only situation in which the bug described in this issue would arise.

Any tips on implementing this for Ix?

To be honest, I haven't through about Ix much. Is there a particular challenge that Ix is imposing on your patch?

Hey Ryan, thanks for taking the time to help out!

See if the errors persist if you propagate inst_tys from hasStockDeriving.

That was the first thing I did, but I was also getting (a slightly different) zipTyEnv errors. I believe the problem is that inst_tys :: [Type] from hasStockDeriving represents the type being derived (it's a list for the case of MultiParamTypeClasses, but should only be a list of one element since these type classes only have one parameter) while the [Type] parameter in dataConCannotMatch represents types to instantiate type variables in the provided DataCon.

This is the dataConInstSig info I get that occurs if I do this

-- Printing out these values in `dataConInstSig`:
-- (con, univ_tvs, ex_tvs, arg_tys, univ_tys)

(L1, [k, f, g, p], [], [f p], [(:+:) f g p])

Is there a particular challenge that Ix is imposing on your patch?

I don't see the derivation for Ix using tyConDataCons, unlike the other ones. Do you know how Ix extracts the data constructors from the TyCon?

That was the first thing I did, but I was also getting (a slightly different) zipTyEnv errors.

Ah, you are right. inst_tys isn't what I meant to say; I was actually thinking of dit_rep_tc_args from DerivInstTys (but double-check me on that). Currently, that isn't an argument to hasStockDeriving or gen_*_binds, but it shouldn't be too difficult to propagate dit_rep_tc_args to these functions.

I don't see the derivation for Ix using tyConDataCons, unlike the other ones.

Good point. One complication that I didn't think about too much is that many derived instances actually do not use or pattern match on constructors directly. Instead, they do this indirectly by way of auxiliary functions. For example, here is the -ddump-deriv output for a simple derived Ix instance:

{-# OPTIONS_GHC -ddump-deriv #-}
module Foo where

import Data.Ix

data A = MkA
  deriving (Eq, Ord, Ix)

==================== Derived instances ====================
Derived class instances:

  [...]

  instance GHC.Ix.Ix Foo.A where
    GHC.Ix.range (a_a1s4, b_a1s5)
      = case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi a_a1s4) of {
          a#_a1s6
            -> case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi b_a1s5) of {
                 b#_a1s7
                   -> GHC.Base.map
                        Foo.$tag2con_F0QIzYDmc392Khs0v1sjJi
                        (GHC.Enum.enumFromTo
                           (GHC.Types.I# a#_a1s6) (GHC.Types.I# b#_a1s7)) } }
    GHC.Ix.unsafeIndex c_a1s8@(a_a1s9, _) d_a1sa
      = case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi a_a1s9) of {
          a#_a1sb
            -> case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi d_a1sa) of {
                 d#_a1sc
                   -> case (d#_a1sc GHC.Prim.-# a#_a1sb) of {
                        c_a1sd -> GHC.Types.I# c_a1sd } } }
    GHC.Ix.inRange (a_a1se, b_a1sf) c_a1sg
      = case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi a_a1se) of {
          a#_a1sh
            -> case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi b_a1sf) of {
                 b#_a1si
                   -> case (Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi c_a1sg) of {
                        c#_a1sj
                          -> (GHC.Classes.&&)
                               (GHC.Prim.tagToEnum# (c#_a1sj GHC.Prim.>=# a#_a1sh))
                               (GHC.Prim.tagToEnum# (c#_a1sj GHC.Prim.<=# b#_a1si)) } } }

  Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi :: Foo.A -> GHC.Prim.Int#
  Foo.$tag2con_F0QIzYDmc392Khs0v1sjJi :: GHC.Types.Int -> Foo.A
  Foo.$maxtag_F0QIzYDmc392Khs0v1sjJi :: GHC.Types.Int
  Foo.$maxtag_F0QIzYDmc392Khs0v1sjJi = GHC.Types.I# 0#
  Foo.$tag2con_F0QIzYDmc392Khs0v1sjJi (GHC.Types.I# a_a1rT)
    = GHC.Prim.tagToEnum# a_a1rT
  Foo.$con2tag_F0QIzYDmc392Khs0v1sjJi Foo.MkA = 0#

In particular, note the use of $con2tag_F0QIzYDmc392Khs0v1sjJi, which returns a zero-indexed tag for each data constructor (0 for the first constructor, 1 for the second, etc.) and $tag2con_F0QIzYDmc392Khs0v1sjJi, which constructs a constructor based on the corresponding tag. For the sake of making the code slightly more efficient at runtime, $tag2con often uses the primitive tagToEnum# function instead of directly pattern matching on Int values. Unfortunately, tagToEnum# does not work at all with GADTs, which poses a challenge for our needs.

My recommendation would be to change the code in GHC.Tc.Deriv.Generate that generates $tag2con implementations and have it check if the data type involved is a GADT. If it is, then rather than using tagToEnum#, pattern match on Ints directly to implement $tag2con. This approach won't work for every GADT, but it should at least work better than the current approach.

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Standalone deriving for GADTs should avoid impossible cases

Child items ...

Activity

Standalone deriving for GADTs should avoid impossible cases

Relates to

Activity