Opened 4 years ago

Closed 2 years ago

#10343 closed feature request (wontfix)

Make Typeable track kind information better

Reported by: oerjan Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 7.10.1
Keywords: Typeable Cc: Ptharien's, Flame, oerjan, shachaf, int-e, dterei, RyanGlScott, sweirich
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typeOf :: Typeable (a::k) => Proxy a -> TypeRep
Blocked By: Blocking:
Related Tickets: #9858, #11011 Differential Rev(s):
Wiki Page:

Description (last modified by oerjan)

(EDIT: My long rambling seems to have been confusing, so a summary:

I think that the type inference and runtime representation should support constructing Typeable (T :: k), even when k contains kind variables that are only mentioned in other Typeable constraints not necessarily involving the type constructor T. This will allow simple composition with polymorphic type constructors like Proxy and Typeable to work more naturally, but also more complicated things.)

With all the apparent exploitable bugs now fixed, #9858 seems to be settling down. Simon P.J. asked me to make a new ticket for some quibbles I still have with limitations of the new design. These started with some examples that I discussed there pre-implementation with Richard Eisenberg, and which he concluded could be supported by a "sufficently smart solver".

In the new (current) design, a TypeRep does contain kind information, which as I understand it is a list of KindReps for the explicit kind parameters applied to the type constructor after type inference. This is sufficient to prevent confusing the same type constructor used at different kinds, and also easily supports type application provided the TypeReps of the parts are known. For this, the internal Typeable constraint solver only ever needs to combine TypeReps, never decompose them.

Since no one else complained in #9858, I assume this is enough for what people are currently using Typeable for. However:

I think the current TypeRep representation for Typeable (a :: k) doesn't contain enough information to generally extract the KindRep for k itself, much less to decompose it, even if the internal Typeable solver were to try. This prevents some polykinded code that is intuitively sound, and which "worked" in the old system, although if only because it didn't try to track kinds at all.

For example, the following expression, with PolyKinds enabled:

typeOf :: Typeable a => Proxy a -> TypeRep

In the old system, this worked simply by combining the TypeRep for Proxy with the TypeRep for a. But in the new system, it fails, because the TypeRep for Proxy needs to know the kind of a, which is neither statically known nor available from the TypeRep of a. You would need to have compile-time information about the type constructor of a to even know how to build the KindRep from the kind arguments.

This problem with constructing TypeReps would arise whenever a polykinded type constructor is applied to a type whose kind is not a known monomorphic one. The second similar one I can think of is

typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep

In an ideal system, we can also find use cases that require not just extracting the KindRep for a type, but also decomposing it. Here is my very hypothetical kitchen sink example from 46:ticket:9858 (this example was made up as a test case before I knew what the new solver would support):

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE AutoDeriveTypeable #-}

import Data.Typeable

newtype C a b = C ()

step :: Proxy (a :: [k] -> *) -> Proxy (C a :: [k -> *] -> *)
step Proxy = Proxy

nest :: Typeable (a :: [k] -> *) => Int -> Proxy a -> TypeRep
nest 0 x = typeRep x
nest n x = nest (n-1) (step x)

main = print $ nest 10 (Proxy :: Proxy (C () :: [()] -> *))

Here, to make this compile, the solver would need to derive Typeable (C a :: [k -> *] -> *] from Typeable (a :: [k] -> *), which at runtime requires first extracting the KindRep of k from the TypeRep of a, and then building the TypeRep for the correctly kinded C. At least the former part seems essentially impossible with the current TypeRep representation, even with a more clever solver.

Change History (40)

comment:1 Changed 4 years ago by oerjan

comment:2 Changed 4 years ago by shachaf

Cc: shachaf added

comment:3 Changed 4 years ago by goldfire

I agree that a kindRep :: TypeRep -> TypeRep or perhaps kindRep :: Typeable a => proxy a -> TypeRep is in order. It seems this is useful independent of kind equalities, though it will likely become more useful (and conspicuously missing if unimplemented) with kind equalities.

comment:4 Changed 4 years ago by goldfire

Here's a strange thought: once we have * :: *, does Typeable k a imply Typeable * k? It probably should. But then we would have

class Typeable k => Typeable (a :: k) where ...

which has a superclass cycle. The cycle is benign because we know that all kinds have type *, but it still is a curious beast.

Of course, this isn't necessary, but it would be nice.

comment:5 Changed 4 years ago by simonpj

I'm assuming that much of what Oerjan wants will "just work" once we have Richard's kind equalities. Right Richard?

But not, perhaps, kindRep which I do not fully understand. I wonder if we might address kindRep as part of the overhaul sketched in this wiki page about Typeable? The plan there is to move to type-indexed type representations.

  • What would kindRep look in that context?
  • How would you use kindRep?

A new subsection on that page might be useful.

Simon

comment:6 in reply to:  5 Changed 4 years ago by goldfire

Replying to simonpj:

I'm assuming that much of what Oerjan wants will "just work" once we have Richard's kind equalities. Right Richard?

But not, perhaps, kindRep which I do not fully understand.

I'm not sure exactly what "much of what Oerjan wants" refers to, so I can't make a claim one way or the other. I can say that the feature requested in this ticket will not just work in my branch.

The problem is that if we have a TypeRep for some time a of kind k, there is no way, at runtime, to extract a TypeRep for k. TypeReps simply don't store enough information to do this. Fixing this should be straightforward, and I believe is totally orthogonal to anything dealing with my branch. (Well, not totally orthogonal, because in my branch kindRep (kindRep <<anything>>) is a TypeRep for *, and today it would be a TypeRep for BOX. But this matters little.) Coming up with an API design is a touch harder, but I don't think it should be too bad, and it remains independent from the TTypeRep a story.

Oerjan, you're a (the?) client of all this. Propose an API design. :)

comment:7 Changed 4 years ago by oerjan

I am not sure I can be called a client, I don't have actual useful code hinging on this. As a hobbyist, I spend more time thinking about Haskell than actually programming in it.

I think that simply adding kindRep :: TypeRep -> TypeRep as a field of TypeRep would make the necessary information available at runtime. This ought to fit just as well into the current design as into the proposed TTypeRep on the wiki. I also have a hunch this might make the already existing list of KindReps redundant.

The question of how to make the Typeable solver make use of that information for building kind evidence seems to me like the more complicated part of this.

Just to prove it is possible in principle, I'll restate my mock representation from back in 48:ticket:9858:

class (KindableParts a, a ~ Proxy) => Kindable (a :: k -> *) where
    type KindableParts a :: Constraint
    kindRep :: KindRep a

class Kindable (Proxy :: k -> *) => Typeable (a :: k) where
    typeRep :: proxy a -> TypeRep

This worked well enough to be a basis for running my kitchen sink test case in 7.8.3. However, it doesn't support Richard's ideas for avoiding exposing "Kindable" constraints when doing type inference. And of course the representation's made for reusing already existing type features rather than for efficiency.

comment:8 Changed 4 years ago by simonpj

I was using "what Oerjan wants" as shorthand for the Description of this ticket. For exmaple, he wants the expression

typeRep :: Typeable a => Proxy a -> TypeRep

to typecheck. And it think it will when Richard is done. Similarly perhaps other items on his wish list above. Perhaps it would help to edit the description to enumerate "Wish 1", "Wish 2" etc?

In "Wish n" he is asking for kindRep, for reasons I do not understand. Maybe you can give a use-case? And better still, what would it look like in the context of type-indexed type representations described in wiki:Typeable?

Simon

comment:9 Changed 4 years ago by oerjan

I knew I shouldn't have rambled on so much in my post... the mention of extracting KindRep was not a direct wish, more my explanation of why the current design doesn't handle my test cases. As in, it would be needed to implement a solution to them.

So I guess a shorter summary of what I want is in order:

I want that the type inference and runtime representation should support constructing Typeable (T :: k), even when k contains kind variables that are only mentioned in other Typeable constraints not necessarily involving the type constructor T.

(This assumes that type application keeps working as well as it does. Type constructors are the base case which now sometimes doesn't work.)

This is, as far as I can see, precisely what is needed to get things like typeOf :: Typeable a => Proxy a -> TypeRep or typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep to work, but it would also enable much more contrived things like my kitchen sink example.

comment:10 Changed 4 years ago by oerjan

Description: modified (diff)

comment:11 Changed 4 years ago by oerjan

Description: modified (diff)

comment:12 Changed 4 years ago by goldfire

Milestone: 7.12.1
Owner: set to goldfire

This all continues to seem straightforward to me, but I maintain (in contrast to Simon's claim in comment:8) that this is separate from kind equalities.

My implementation approach would be, as oerjan suggests, adding a kindRep field in TypeRep. This can be done today.

Then, define

class Typeable k => Typeable (a :: k) where ...  
   -- probably not possible until I merge

This appears to be a superclass cycle, but we know it doesn't induce infinite regress because the kind of a kind is always *. So, we arrange to have this definition accepted.

Then, the solver will just do the right thing. When we have a given Typeable (a :: k) constraint, the solver will spit off a Typeable (k :: *) constraint. We may have to arrange for the solver not to then spit off a (harmless, but potentially confusing) Typeable (* :: *) constraint.

To work with typeOf :: Typeable a => Proxy a -> TypeRep... well it will all just work. Typechecking this expression leads to

[G] Typeable (a :: k)
[W] Typeable (Proxy (a :: k))

After a little work, the solver arrives at

[G] Typeable (a :: k)
[G] Typeable (k :: *)
[W] Typeable (Proxy :: k -> *)  -- the Typeable solver doesn't decompose kind applications
[W] Typeable (a :: k)

The wanteds are easily solved from the givens.

Since I'm the one with the plan, sounds like I should be the one to execute the plan. But probably only after I merge, since this isn't something we need today.

comment:13 Changed 4 years ago by simonpj

Can I make two pleas?

  1. Could we cast this discussion in the language of type-indexed type representations TTypeRep, in Typeable? A TTypeRep a is very like Typeable a, but has the very great merit of being an ordinary data value. Typeable a is just the implicit version of it. You can get from one to the other via tTypeRep:
    class Typeable a where
      tTypeRep :: TTypeRep a
    
    By using an ordinary data value we get away from talking about classes or superclasses or solvers or whatnot. Once we know, with forensic precision, what TTypeable a should do, then we can think about how the solver might generate Typeable a dictionaries, which are simply containers for a TTypeable a value.
  1. Can we keep TTypeRep abstract, so instead of talking about what it "contains" we speak entirely in terms of what functions are available over it? decomposeFun is one such function. Now, for kindRep I think you are asking for a function
    kindRep :: forall (a::k). TTypeRep a -> TTypeRep k
    
    And indeed it seems plausible that we should provide such a function, although I have seen no examples whatsoever of why it might be useful. (Producing a TypeRep only to print it does not count; there are easier ways of producing that sequence of characters.)

I'm afraid I found the summary entirely opaque "The type inference and runtime representation should support constructing Typeable (T :: k), even when k contains kind variables that are only mentioned in other Typeable constraints not necessarily involving the type constructor T. This will allow simple composition with polymorphic type constructors like Proxy and Typeable to work more naturally, but also more complicated things." What do you mean by "simple composition"? What do you mean by "more complicated things"?

Don't answer directly: rather, just give a sequence of examples that you think should work. That will show me what "simple composition" means, rather than telling me!

comment:14 Changed 4 years ago by int-e

Cc: int-e added

comment:15 in reply to:  12 Changed 4 years ago by oerjan

Replying to goldfire:

This all continues to seem straightforward to me, but I maintain (in contrast to Simon's claim in comment:8) that this is separate from kind equalities.

Whew, I was starting to worry.

[G] Typeable (a :: k)
[G] Typeable (k :: *)
[W] Typeable (Proxy :: k -> *)  -- the Typeable solver doesn't decompose kind applications
[W] Typeable (a :: k)

The wanteds are easily solved from the givens.

Looks good, although note that as we discussed in #9858, the kitchen sink example would require actually decomposing Typeable kinds.

In principle so does normal type application, once you include kindRep:

(Typeable (a :: k1 -> k2), Typeable (b :: k1)) => Typeable (a b :: k2)

The only plausible source for the kindRep of a b is to decompose the kind information in Typeable a. Although I guess type application can still be a special case.

Since I'm the one with the plan, sounds like I should be the one to execute the plan. But probably only after I merge, since this isn't something we need today.

:)

comment:16 in reply to:  13 Changed 4 years ago by oerjan

Replying to simonpj:

I made a long reply, forgot to copy to clipboard before submitting, and had trac give me an error message involving TLS, forgetting everything.

comment:17 Changed 4 years ago by goldfire

I've updated Typeable. See the new Proposed API section, and the new Step 3.

comment:18 in reply to:  17 Changed 4 years ago by oerjan

Replying to goldfire:

I've updated Typeable. See the new Proposed API section, and the new Step 3.

I'd like to note that if the proposed API is to help with Step 3 aka this ticket, either trCon or your suggested tyConRep needs to take a TTypeRep k argument.

The "How can we get a TTyCon for a known-at-compile-time tycon?" was something I also stumbled on when trying to think of an API. Curiously if you simplify this a bit by removing TTyCon (>_> <_<), there is a nice end-user way of writing this from what's on the wiki page:

x :: TTypeRep k -> TTypeRep (Proxy :: k -> *)
x tt = withTypeable tt tTypeRep

Of course this just calls back into the entire machinery that's being implemented, so cannot be used as a basis. However, it means that the primitive desugaring of this may not need to be exposed to users.

comment:19 Changed 4 years ago by dterei

Cc: dterei added

comment:20 Changed 4 years ago by Ptharien's Flame

Cc: Ptharien's Flame added

comment:21 Changed 4 years ago by RyanGlScott

Cc: RyanGlScott added

comment:22 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:23 Changed 4 years ago by sweirich

Cc: sweirich added

comment:24 Changed 4 years ago by bgamari

I've been playing around with various ways that we could achieve this. As far as I can tell there are two options,

  • Encode type constructor kinds into TyCon and reconstruct applications from these at runtime. This would require that TyCon get a bit larger, and would need to include a TypeRep, which is unfortunate as this cost is paid by all users, regardless of whether they use Typeable.
  • Construct the kind representation at when we are asked to construct a Typeable dictionary.

At the moment I'm leaning towards the second approach (and have a broken implementation in Phab:D1837).

The trouble is that you need to be very careful when handling recursive kinding relationships. Consider, for instance, these examples:

(->) :: (->) * (* -> *)
TYPE :: Levity -> TYPE 'Lifted 

Here the types we are trying to derive kind representations for appear in their own kinds. This causes trouble in solving for these representations:

Currently we construct Typeable evidence by decomposing type applications until we hit a tycon. One way to account for kind representations would be to require that when generating evidence for Typeable (t :: k) we also generate evidence for Typeable k. However, if we do this naively we end up sending the solver in a loop. Consider the case we are asked to solve for Typeable (Int -> Bool). Evidence construction would roughly proceed as follows,

want (Typeable (Int -> Bool :: *))
    want (Typeable ((->) :: (* -> * -> *))        -- Normally this isn't a problem:
                                                  -- since (->) is a TyCon, we could 
                                                  -- just stop here; but...
                                                  -- now we need a kind representation 
        want (Typeable (* -> * -> *))
            want (Typeable ((->) * (* -> *)))     -- again we decompose
                want (Typeable (->))
                    want (Typeable (* -> * -> *)) -- again solve for kind of (->)
                        ...                       -- now we are in a loop...

Likewise, we can also get non-trivial cycles,

Levity :: TYPE 'Lifted
TYPE :: Levity -> TYPE 'Lifted
'Lifted :: Levity

One way to address this issue would be to manually define these representations (just as we did before my recent solution to #11120), allowing us to tie the knot. This is a bit frustrating, however, as then we end up yet again having to manually define a handful of representations (and now their kind representations as well).

It would be nice if we could convince the solver to consider things like Typeable (->) as solved when it encounters them; then next time it encounters this constraint it can simply use the evidence it generated earlier. Desugaring would then involve generating a recursive binding set containing all of the needed Typeable dictionaries.

It's also possible that I have fundamentally misunderstood something here. If so, please feel free to say so.

Last edited 4 years ago by bgamari (previous) (diff)

comment:25 Changed 4 years ago by simonpj

I'm lost on this thread. Can someone re-state what the specification is? And do so without reference to the preceding 24 comments. Just a free-standing description of the problem we are trying to solve. I can't begin to think about an implementation until I'm clear about specification.

Also, can you do that in the light of the (recently-published) A reflection on types? It describes the story about type representation that I hope to get into HEAD once 8.0 is out of the way.

Thanks!

comment:26 Changed 4 years ago by bgamari

My goal was to augment the existing Typeable interface with a means of extracting the kind of the type represented by a given TypeRep. That is,

-- The current (non-type-indexed) TypeRep machinery
data TypeRep
type KindRep = TypeRep
typeRep :: Typeable a => Proxy a -> TypeRep

-- I wanted this...
typeRepKind :: TypeRep -> KindRep

As far as I can tell, the semantics of typeRepKind should be clear so long as we are only talking about monomorphically kinded types. For instance,

kindRep :: Typeable a => Proxy a -> KindRep
kindRep = typeRepKind . typeRep

kindRep (Proxy :: Proxy Int)          == *
kindRep (Proxy :: Proxy Int#)         == TYPE 'Unlifted
kindRep (Proxy :: Proxy '[4])         == '[Nat]
kindRep (Proxy :: Proxy (4 ':))       == '[Nat] -> '[Nat]
kindRep (Proxy :: Proxy [])           == * -> *
kindRep (Proxy :: Proxy [Int])        == *
kindRep (Proxy :: Proxy ((->) Int))   == * -> *
kindRep (Proxy :: Proxy Eq)           == * -> Constraint

kindRep (Proxy :: Proxy (':))         insoluble
kindRep (Proxy :: Proxy 'Just)        insoluble

Sorry if the above is a bit hand-wavy. I was merely looking for a nice weekend project; my experience in the typechecker is quite limited (although I'd love for that to change).

I have not thought much about this might fit in to the new type-indexed TypeRep.

Last edited 4 years ago by bgamari (previous) (diff)

comment:27 Changed 4 years ago by bgamari

Perhaps something like this?

data Fingerprint = Fingerprint {- Int -}

data TyCon a = TyCon Fingerprint String

data TypeRep (a :: k) where
    TypeCon :: TyCon a -> TypeRep k -> TypeRep (a :: k)
    TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
               TypeRep (a :: k1 -> k2)
            -> TypeRep (b :: k1)
            -> TypeRep (a b)

class Typeable k => Typeable (a :: k) where
    typeRep :: TypeRep a

typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
typeRepKind (TypeCon _ k) = k

typeRepName :: TypeRep a -> String
typeRepName (TypeCon (TyCon _ n) _) = n

Unfortunately this currently doesn't compile due to the overly restrictive kind that we give to (->), * -> * -> *. I would have thought this would be more polymorphic. There is a small note about this in TysPrim,

You might think that (->) should have type ?? -> ? -> *, and you'd be right. But if we do that we get kind errors when saying

instance Control.Arrow (->)

because the expected kind is * -> * -> *. The trouble is that the expected/actual stuff in the unifier does not go contra-variant, whereas the kind sub-typing does. Sigh. It really only matters if you use (->) in a prefix way, thus: (->) Int# Int#. And this is unusual. because they are never in scope in the source

The reference to kind sub-typing makes me suspect that this restriction is no longer true. I've not yet tried lifting it, however.

Last edited 4 years ago by bgamari (previous) (diff)

comment:28 Changed 4 years ago by simonpj

OK, so the payload is that you want

typeRepKind : forall (k::*). forall (a::k). TypeRep a -> TypeRep k

At least I think that's the right type.

That's a nice short specification. I hope that it would not be too hard to implement.

The whole project of moving from the existing to the new TypeRep needs someone to lead it; maybe that can be your weekend project! The key ticket is #11011, and wiki page Typeable.

comment:29 Changed 4 years ago by bgamari

The whole project of moving from the existing to the new TypeRep needs someone to lead it; maybe that can be your weekend project!

Indeed I have been eyeing it. I thought exposing kind representations would be a good warm-up, although at various points over the weekend I've considered going all-in and moving ahead with the new TypeRep.

Last edited 4 years ago by bgamari (previous) (diff)

comment:30 Changed 4 years ago by simonpj

Let's not implement typeRepKind in the existing TypeRep setup. First move to the new one!

comment:31 Changed 4 years ago by simonpj

Keywords: Typeable added

comment:32 Changed 3 years ago by bgamari

Milestone: 8.0.18.2.1

This bug won't be fixed in 8.0.1; bumping to 8.2.

comment:33 Changed 3 years ago by bgamari

For the record, this will be addressed in the solution of #11011 which should be coming in GHC 8.2. See Typeable/BenGamari for details.

comment:34 Changed 3 years ago by bgamari

Resolution: duplicate
Status: newclosed

Given that the type-indexed Typeable rework will provide support for pulling the kind out of a TypeRep I'm going to close this as a duplicate.

comment:35 Changed 3 years ago by bgamari

Owner: goldfire deleted
Resolution: duplicate
Status: closednew

Unfortunately it looks like the initial implementation of type-indexed Typeable won't actually address this issue. We'll see what the future holds in store.

comment:36 Changed 3 years ago by Ben Gamari <ben@…>

In 8fa4bf9a/ghc:

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.

comment:37 Changed 2 years ago by rwbarton

Is this done? comment:35 is a bit cryptic. If not done, could you clarify what remains?

comment:38 Changed 2 years ago by oerjan

From the discussion I've seen, I am purely guessing that all the necessary internal representations are now available, but the solver part is not. I.e. with PolyKinds enabled, the definition

{-# LANGUAGE PolyKinds #-}
import Data.Typeable
f :: Typeable a => Proxy a -> TypeRep
f = typeOf

still won't compile, but you probably can now use the new TypeRep mechanisms do write an equivalent function by hand.

On the other hand, since 8.0 with TypeInType you can write

f :: (Typeable (a::k), Typeable k) => Proxy a -> TypeRep
f = typeOf

which means the actual need for this improvement is less than it was in 7.10.

At the time I wrote this ticket, I was somewhat thinking about preserving backwards compatibility, which got broken in 7.10 anyhow.

(And until recent trouble with the constraints package, I thought no one had been affected in practice - but the last version of that package actually now restricts the kind of the Deferrable (a ~ b) instance to * in just 7.10, because of this, see discussion at end of https://github.com/ekmett/constraints/issues/43.)

Incidentally in GHCi 8.0.1, with PolyKinds but not TypeInType enabled:

Prelude Data.Typeable> let f x@Proxy = typeOf x
Prelude Data.Typeable> :t f
f :: forall k (t :: k).
     (Typeable * k, Typeable k t) =>
     Proxy k t -> TypeRep

which is convenient, but means you get an inferred type you cannot write.

comment:39 Changed 2 years ago by bgamari

Personally, I am satisfied with the status quo of being able to write,

f :: (Typeable (a::k), Typeable k) => Proxy a -> TypeRep
f = typeOf

oerjan, if you also think that this is satisfactory then feel free to close this ticket.

comment:40 Changed 2 years ago by oerjan

Resolution: wontfix
Status: newclosed

Yes, I see that even my "kitchen sink" example can be fixed with a simple Typeable k constraint. And as in my previous comment, such constraints can be inferred too.

So since I don't know any examples that this doesn't suffice for, I'll close this.

Note: See TracTickets for help on using tickets.