[GHC] #13809: TH-reified data family instances have a paucity of kinds

#13809: TH-reified data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template | Version: 8.0.1 Haskell | Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this data family (and instances): {{{#!hs {-# 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: {{{#!hs 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 `Type`s 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This also affects type family instances: {{{#!hs {-# LANGUAGE TypeFamilies #-} module Foo where type family Foo a type instance Foo ((f :: * -> *) (a :: *)) = Int type instance Foo ((f :: (* -> *) -> *) (a :: (* -> *))) = Char }}} {{{#!hs 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)) ] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #8953 Comment: Ugh, and it affects class instances too: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeFamilies #-} module Foo where class Foo a instance {-# OVERLAPPING #-} Foo ((f :: * -> *) (a :: *)) instance {-# OVERLAPPING #-} Foo ((f :: (* -> *) -> *) (a :: (* -> *))) }}} {{{#!hs 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 :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): That ghc-proposal is discussed [https://github.com/ghc-proposals/ghc- proposals/pull/55 here]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah. I suppose if we're going to be adding `foralls` to instances anyways, then option (1) is the only sensible one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type familly and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #8953 => #8953, #14268 Comment: See #14268 to track the implementation of the aforementioned GHC proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type family and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8953, #14268 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type family and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Template Haskell | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * blockedby: => 14268 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13809: TH-reified type family and data family instances have a paucity of kinds -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Template Haskell | Version: 8.0.1 Resolution: fixed | Keywords: TypeFamilies 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed * milestone: => 8.8.1 Comment: Now that #14268 is implemented, I claim that this is fixed. That is because when you reify `Foo` now, you get the following information: {{{#!hs 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13809#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC