#13261: Consider moving Typeable evidence generation wholly back to solver -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 goldfire): For the record, I've never been totally convinced by the "generate Typeable stuff at declaration time" approach. As noted above, there is a shared cost. Do we have any program that shows a concrete speed boost by the new design? Yes, the new design seems like `Typeable`-heavy code would run faster, but it would be lovely to verify this fact and be able to quantify it. Once there are dependent types, this issue does not really change. Yes, users could effectively use `Typeable` without writing the word `Typeable` in their programs, but they would still need to use runtime type tests to trigger any of this machinery. So I would consider this orthogonal. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13261#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13261: Consider moving Typeable evidence generation wholly back to solver -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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 nomeata): Can we do it like specializations: Create on the fly the first time we need them, but use an existing one if any dependency already created them? (Maybe this is what Simon means by on-the-fly CSE). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13261#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13261: Consider moving Typeable evidence generation wholly back to solver -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12276 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"8fa4bf9ab3f4ea4b208f4a43cc90857987e6d497/ghc" 8fa4bf9a/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8fa4bf9ab3f4ea4b208f4a43cc90857987e6d497" Type-indexed Typeable This at long last realizes the ideas for type-indexed Typeable discussed in A Reflection on Types (#11011). The general sketch of the project is described on the Wiki (Typeable/BenGamari). The general idea is that we are adding a type index to `TypeRep`, data TypeRep (a :: k) This index allows the typechecker to reason about the type represented by the `TypeRep`. This index representation mechanism is exposed as `Type.Reflection`, which also provides a number of patterns for inspecting `TypeRep`s, ```lang=haskell pattern TRFun :: forall k (fun :: k). () => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE r1) (res :: TYPE r2). (k ~ Type, fun ~~ (arg -> res)) => TypeRep arg -> TypeRep res -> TypeRep fun pattern TRApp :: forall k2 (t :: k2). () => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b) => TypeRep a -> TypeRep b -> TypeRep t -- | Pattern match on a type constructor. pattern TRCon :: forall k (a :: k). TyCon -> TypeRep a -- | Pattern match on a type constructor including its instantiated kind -- variables. pattern TRCon' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a ``` In addition, we give the user access to the kind of a `TypeRep` (#10343), typeRepKind :: TypeRep (a :: k) -> TypeRep k Moreover, all of this plays nicely with 8.2's levity polymorphism, including the newly levity polymorphic (->) type constructor. Library changes --------------- The primary change here is the introduction of a Type.Reflection module to base. This module provides access to the new type-indexed TypeRep introduced in this patch. We also continue to provide the unindexed Data.Typeable interface, which is simply a type synonym for the existentially quantified SomeTypeRep, data SomeTypeRep where SomeTypeRep :: TypeRep a -> SomeTypeRep Naturally, this change also touched Data.Dynamic, which can now export the Dynamic data constructor. Moreover, I removed a blanket reexport of Data.Typeable from Data.Dynamic (which itself doesn't even import Data.Typeable now). We also add a kind heterogeneous type equality type, (:~~:), to Data.Type.Equality. Implementation -------------- The implementation strategy is described in Note [Grand plan for Typeable] in TcTypeable. None of it was difficult, but it did exercise a number of parts of the new levity polymorphism story which had not yet been exercised, which took some sorting out. The rough idea is that we augment the TyCon produced for each type constructor with information about the constructor's kind (which we call a KindRep). This allows us to reconstruct the monomorphic result kind of an particular instantiation of a type constructor given its kind arguments. Unfortunately all of this takes a fair amount of work to generate and send through the compilation pipeline. In particular, the KindReps can unfortunately get quite large. Moreover, the simplifier will float out various pieces of them, resulting in numerous top-level bindings. Consequently we mark the KindRep bindings as noinline, ensuring that the float-outs don't make it into the interface file. This is important since there is generally little benefit to inlining KindReps and they would otherwise strongly affect compiler performance. Performance ----------- Initially I was hoping to also clear up the remaining holes in Typeable's coverage by adding support for both unboxed tuples (#12409) and unboxed sums (#13276). While the former was fairly straightforward, the latter ended up being quite difficult: while the implementation can support them easily, enabling this support causes thousands of Typeable bindings to be emitted to the GHC.Types as each arity-N sum tycon brings with it N promoted datacons, each of which has a KindRep whose size which itself scales with N. Doing this was simply too expensive to be practical; consequently I've disabled support for the time being. Even after disabling sums this change regresses compiler performance far more than I would like. In particular there are several testcases in the testsuite which consist mostly of types which regress by over 30% in compiler allocations. These include (considering the "bytes allocated" metric), * T1969: +10% * T10858: +23% * T3294: +19% * T5631: +41% * T6048: +23% * T9675: +20% * T9872a: +5.2% * T9872d: +12% * T9233: +10% * T10370: +34% * T12425: +30% * T12234: +16% * 13035: +17% * T4029: +6.1% I've spent quite some time chasing down the source of this regression and while I was able to make som improvements, I think this approach of generating Typeable bindings at time of type definition is doomed to give us unnecessarily large compile-time overhead. In the future I think we should consider moving some of all of the Typeable binding generation logic back to the solver (where it was prior to 91c6b1f54aea658b0056caec45655475897f1972). I've opened #13261 documenting this proposal. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13261#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13261: Consider moving Typeable evidence generation wholly back to solver -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12276 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by oerjan): * cc: oerjan (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13261#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#13261: Consider moving Typeable evidence generation wholly back to solver -------------------------------------+------------------------------------- Reporter: bgamari | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12276 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => Typeable -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13261#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler