Opened 2 years ago

Closed 11 months ago

#13809 closed bug (fixed)

TH-reified type family and data family instances have a paucity of kinds

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Template Haskell Version: 8.0.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: #14268 Blocking:
Related Tickets: #8953, #14268 Differential Rev(s):
Wiki Page:

Description

Consider this data family (and instances):

{-# LANGUAGE TypeFamilies #-}
module Foo where

data family Foo a
data instance Foo ((f :: *        -> *) (a ::       *))
data instance Foo ((f :: (* -> *) -> *) (a :: (* -> *)))

These are two data family instances that GHC distinguishes by the kinds of their type parameters. However, Template Haskell does not give me the same insight that GHC has, because if I call Language.Haskell.TH.reify ''Foo, I get this:

FamilyI
  (DataFamilyD
     Foo.Foo [ KindedTV a_6989586621679025989 StarT ] (Just StarT))
  [ DataInstD
      []
      Foo.Foo
      [ AppT (VarT f_6989586621679026001) (VarT a_6989586621679026000) ]
      Nothing
      []
      []
  , DataInstD
      []
      Foo.Foo
      [ AppT (VarT f_6989586621679026007) (VarT a_6989586621679026006) ]
      Nothing
      []
      []
  ]

Note that neither f nor a have a kind signature in either instance! This makes it completely impossible to tell which is which (aside from the order, which is brittle). It would make my life a lot easier if TH were to include kind signatures for each type variable in a data family instance. I can see two ways to accomplish this:

  1. Include a [TyVarBndr] field in DataInstD and NewtypeInstD where each TyVarBndr is a KindedTV.
  2. Walk over the Types in a DataInstD/NewtypeInstD and ensure that every occurrence of a VarT is surrounded with SigT to indicate its kind.

While (1) is arguably the cleaner solution, since it makes the kinds easy to discover, it is a breaking change. Therefore, I'm inclined to implement option (2) instead.

Change History (9)

comment:1 Changed 2 years ago by RyanGlScott

Summary: TH-reified data family instances have a paucity of kindsTH-reified type familly and data family instances have a paucity of kinds

This also affects type family instances:

{-# LANGUAGE TypeFamilies #-}
module Foo where

type family Foo a
type instance Foo ((f :: *        -> *) (a ::       *))  = Int
type instance Foo ((f :: (* -> *) -> *) (a :: (* -> *))) = Char
FamilyI
  (OpenTypeFamilyD
     (TypeFamilyHead
        Foo.Foo
        [ KindedTV a_6989586621679013859 StarT ]
        (KindSig StarT)
        Nothing))
  [ TySynInstD
      Foo.Foo
      (TySynEqn
         [ AppT (VarT f_6989586621679013869) (VarT a_6989586621679013868) ]
         (ConT GHC.Types.Char))
  , TySynInstD
      Foo.Foo
      (TySynEqn
         [ AppT (VarT f_6989586621679013874) (VarT a_6989586621679013873) ]
         (ConT GHC.Types.Int))
  ]

comment:2 Changed 2 years ago by RyanGlScott

Ugh, and it affects class instances too:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

class Foo a
instance {-# OVERLAPPING #-} Foo ((f :: *        -> *) (a ::       *))
instance {-# OVERLAPPING #-} Foo ((f :: (* -> *) -> *) (a :: (* -> *)))
ClassI
  (ClassD [] Foo.Foo [ KindedTV a_6989586621679013875 StarT ] [] [])
  [ InstanceD
      (Just Overlapping)
      []
      (AppT
         (ConT Foo.Foo)
         (AppT (VarT f_6989586621679013885) (VarT a_6989586621679013886)))
      []
  , InstanceD
      (Just Overlapping)
      []
      (AppT
         (ConT Foo.Foo)
         (AppT (VarT f_6989586621679013890) (VarT a_6989586621679013891)))
      []
  ]

Richard went part of the way in fixing these sorts of issues in #8953, but he avoided going too far in annotating every variable with a kind. Personally, I think he didn't go too far enough :)

comment:3 Changed 2 years ago by goldfire

I prefer design (1). Design (1) also jibes with a ghc-proposal I'm about to submit, allowing the user to write an explicit forall attached to any class/type/data instance (including equations of a closed type family).

Others may feel differently, though.

comment:4 Changed 2 years ago by goldfire

That ghc-proposal is discussed here.

comment:5 Changed 2 years ago by RyanGlScott

Ah. I suppose if we're going to be adding foralls to instances anyways, then option (1) is the only sensible one.

comment:6 Changed 2 years ago by RyanGlScott

See #14268 to track the implementation of the aforementioned GHC proposal.

comment:7 Changed 19 months ago by RyanGlScott

Summary: TH-reified type familly and data family instances have a paucity of kindsTH-reified type family and data family instances have a paucity of kinds

comment:8 Changed 17 months ago by RyanGlScott

Blocked By: 14268 added

comment:9 Changed 11 months ago by RyanGlScott

Milestone: 8.8.1
Resolution: fixed
Status: newclosed

Now that #14268 is implemented, I claim that this is fixed. That is because when you reify Foo now, you get the following information:

FamilyI
  (DataFamilyD
    Foo.Foo [KindedTV a_6989586621679015908 StarT] (Just StarT))
  [ DataInstD
      []
      Foo.Foo
      (Just [KindedTV f_6989586621679015938 (AppT (AppT ArrowT (AppT (AppT ArrowT StarT) StarT)) StarT),KindedTV a_6989586621679015939 (AppT (AppT ArrowT StarT) StarT)])
      [AppT (VarT f_6989586621679015938) (VarT a_6989586621679015939)]
      Nothing
      []
      []
  , DataInstD
      []
      Foo.Foo
      (Just [KindedTV f_6989586621679015958 (AppT (AppT ArrowT StarT) StarT),KindedTV a_6989586621679015959 StarT])
      [AppT (VarT f_6989586621679015958) (VarT a_6989586621679015959)]
      Nothing
      []
      []
  ]

In particular, we now have access to the exact kinds of f and a in each instance, which lets us properly distinguish them. Hooray!

Note: See TracTickets for help on using tickets.